Satisfiability Modulo Theories for Verifying MILP Certificates
Kenan Wood, Runtian Zhou, Haoze Wu, Hammurabi Mendes, Jonad Pulaj
TL;DR
This paper addresses the critical need for trustworthy verification of MILP solver results by formalizing VIPR 1.0 certificates and proving their correctness via a ground formula in the theory of Linear Integer Real Arithmetic. The authors formalize a predicate that captures certificate validity, verify it in Why3, and implement an SMT-LIB based checker that is solver-agnostic and capable of detecting forged certificates. Through experiments on benchmark instances, they show their method can outperform prior tooling in both correctness and safety, while enabling parallel checking and potential integration with interactive theorem provers. The work lays groundwork for a safer, modular checking ecosystem for MILP certificates, with future directions including code extraction and deeper SMT/interactive prover integration.
Abstract
Correctness of results from mixed-integer linear programming (MILP) solvers is critical, particularly in the context of applications such as hardware verification, compiler optimization, or machine-assisted theorem proving. To this end, VIPR 1.0 is the first recently proposed general certificate format for answers produced by MILP solvers. We design a schema to encode VIPR's inference rules as a ground formula that completely characterizes the validity of the algorithmic check, removing any ambiguities and imprecisions present in the specification. We formally verify the correctness of our schema at the logical level using Why3's automated deductive logic framework. Furthermore, we implement a checker for VIPR certificates by expressing our formally verified ground formula with the Satisfiability Modulo Theory Library (SMT-LIB) and check its validity. Our approach is solver-agnostic, and we test its viability using benchmark instances found in the literature.