发表机构
Inria , CMAP, CNRS, École polytechnique, Institut Polytechnique de Paris; École Normale Supérieure de Lyon; PQShield（法国国家信息与自动化研究所，CMAP，法国国家科学研究中心，巴黎综合理工学院，巴黎理工学院; 里昂高等师范学校; PQShield公司）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出基于Rocq的形式化验证多面体顶点集的方法，其速度比lrslib的非正式顶点枚举快1.5至5倍以上，可验证顶点列表的完整性或精确性。
AI 中文摘要
由线性不等式系统描述的多面体顶点计算是多面体计算的核心问题，是H-表示（通过线性不等式）与V-表示（通过顶点和极射线）转换的基础步骤，在数学中多面体及其组合学研究，以及软件和系统验证应用中均发挥重要作用。本文提出一种基于证明的方法，用于形式化验证多面体顶点的计算：给定非正式计算得到的顶点列表，该方法可在证明助手Rocq中证明此列表是完整的，甚至是精确的。该方法的核心是一种基于抽象单纯复形的新完整性准则，它推广了多面体法向扇形的三角剖分。与以往方法相比，该方法的显著优势在于，原本昂贵的数值计算基本简化为多面体的成员资格测试，而其他步骤均为廉价的组合测试。我们在证明助手Rocq中实现了该验证方法并证明其正确性，在多种多面体上进行了实验，包括Birkhoff多面体、交叉多面体、立方体、排列多面体、超单纯形，以及用于否定Hirsch猜想的高维多面体。实验表明，通过Rocq到OCaml的提取检查器进行验证，通常比最先进的非正式C实现lrslib（采用反向搜索方法）的顶点枚举快1.5倍至5倍以上。
英文摘要
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.
Comments20 pages, 3 figures, 2 tables
