Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Linear Programming in Isabelle/HOL

Julian Parsert

TL;DR

The paper presents a formally verified linear programming solver implemented in Isabelle/HOL, building on a prior simplex formalisation and leveraging duality to convert optimisation into a constraint-satisfaction task. By combining two representations of linear polynomials and constructing a robust constraint-generation pipeline, it proves soundness and enables code generation of a verified external solver. The approach is demonstrated through examples, including a production-planning LP and a zero-sum game (Rock–Paper–Scissors) yielding optimal strategies, with generated code available in multiple functional languages. The work advances formal verification for optimization algorithms and lays groundwork for verified solvers in game-theoretic contexts, with planned extensions to completeness proofs and broader integrations.

Abstract

Linear programming describes the problem of optimising a linear objective function over a set of constraints on its variables. In this paper we present a solver for linear programs implemented in the proof assistant Isabelle/HOL. This allows formally proving its soundness, termination, and other properties. We base these results on a previous formalisation of the simplex algorithm which does not take optimisation problems into account. Using the weak duality theorem of linear programming we obtain an algorithm for solving linear programs. Using Isabelle's code generation mechanism we can generate an external solver for linear programs.

Linear Programming in Isabelle/HOL

TL;DR

The paper presents a formally verified linear programming solver implemented in Isabelle/HOL, building on a prior simplex formalisation and leveraging duality to convert optimisation into a constraint-satisfaction task. By combining two representations of linear polynomials and constructing a robust constraint-generation pipeline, it proves soundness and enables code generation of a verified external solver. The approach is demonstrated through examples, including a production-planning LP and a zero-sum game (Rock–Paper–Scissors) yielding optimal strategies, with generated code available in multiple functional languages. The work advances formal verification for optimization algorithms and lays groundwork for verified solvers in game-theoretic contexts, with planned extensions to completeness proofs and broader integrations.

Abstract

Linear programming describes the problem of optimising a linear objective function over a set of constraints on its variables. In this paper we present a solver for linear programs implemented in the proof assistant Isabelle/HOL. This allows formally proving its soundness, termination, and other properties. We base these results on a previous formalisation of the simplex algorithm which does not take optimisation problems into account. Using the weak duality theorem of linear programming we obtain an algorithm for solving linear programs. Using Isabelle's code generation mechanism we can generate an external solver for linear programs.
Paper Structure (13 sections, 5 theorems, 29 equations, 1 figure)

This paper contains 13 sections, 5 theorems, 29 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Isabelle/HOL and Notation
  3. Linear Programming
  4. Linear Optimisation
  5. Duality
  6. Solving Linear Programs
  7. Formalisation
  8. Combining Representations
  9. Creating Systems of Constraints
  10. Abstract Linear Programming
  11. Final Algorithm
  12. Code Generation and Examples
  13. Conclusion and Future Work

Key Result

Theorem 2

Given linear constraints $A$, $b$, and the objective function $c$, we obtain $x$ and $y$ as the solutions to the primal and dual linear program, respectively. We can derive the following equality:

Figures (1)

  • Figure 1: A plot describing the optimisation problem presented in ex:LP.

Theorems & Definitions (8)

  • Example 1: Linear Program
  • Theorem 2: Strong Duality Theorem
  • Theorem 3: vec_to_lpoly and lpoly_to_vec are (almost) inverses
  • Definition 4: Two block non interference
  • Theorem 5
  • Lemma 6
  • Theorem 7: Weak Duality Theorem
  • Example 8: Solving Rock Paper Scissors