Faster formal checking of polyhedron vertices than informal methods
Formally Certifying the Vertex Set of a Polyhedron Faster than Informal Enumeration
Logic in Computer Science
Summary
Finding all the corner points of shapes defined by linear inequalities is important in math and computer science but can be slow and error-prone. The authors developed a way to formally certify that a given list of these corners is complete and correct using a proof assistant, ensuring high reliability. Their method reduces complex calculations to simpler checks and has been proven faster than existing informal tools. They tested it on various complex shapes, showing both efficiency and rigor.
What this means in practice
- •For software verification engineers: Use the certified vertex checker to improve the reliability of polyhedral computations in system and software verification pipelines.
- •For computational geometry developers: Integrate the certification method to verify vertex computations faster and more reliably than traditional enumeration tools.
Authors
Xavier Allamigeon, Yazid Id-Sahra, Pierre-Yves Strub
Abstract
The computation of the vertices of a polyhedron described by a system of linear inequalities is a central problem in polyhedral computation. It is a fundamental step in the conversion between H-representations, by linear inequalities, and V-representations, by vertices and extreme rays. This operation plays an important role both in the study of polyhedra and their combinatorics in mathematics and in applications to software and system verification. We present a certificate-based approach for formally verifying the computation of the vertices of a polyhedron. Given an informally computed list of vertices, our method allows to certify in the proof assistant Rocq that the list is complete, or even exact. The cornerstone of the method is a new completeness criterion based on an abstract simplicial complex that generalizes a triangulation of the normal fan of the polyhedron. A significant advantage over previous approaches is that the usually expensive numerical computations are essentially reduced to membership tests to the polyhedron, while the other steps are cheap combinatorial tests. We implement the certification method and prove its correctness in the proof assistant Rocq. We experiment with it on a variety of polyhedra, including Birkhoff polytopes, cross-polytopes, cubes, permutahedra, hypersimplices, and high-dimensional polytopes involved in the disproof of the Hirsch conjecture. Our experiments show that certification with the Rocq-to-OCaml extracted checker is typically 1.5x to over 5x faster than vertex enumeration by the state-of-the-art informal C implementation lrslib of the reverse search method.