计算混合整数线性规划（MILP）被广泛认为是算法改进与硬件和编译器进步的成功结合（Bixby, 2012），当前的先进MILP求解器能够解决具有数百万变量和约束的问题（Koch等人，2022）。
MILP求解器的需求主要来自工业应用，因此底层的数值计算通常依赖于浮点运算以提高效率。对于大多数此类应用，为了实现高程度的数值稳定性，浮点计算会结合数值误差容忍度。然而，MILP求解器也被用于实验数学中寻找反例（Lancia等人，2020；Pulaj，2020）或提供数值证据（Kenter和Skipper，2018；Pulaj和Wood，2024；Stolee，2013）。在这些定理证明应用中，正确性至关重要，需要额外的保障措施来防止使用不精确的浮点运算和/或编程或算法错误。最著名的例子是在Isabelle/HOL中验证了数千个线性程序在开普勒猜想证明中的不可行性（Nipkow等人，2002）。
另一组在自动定理证明任务中成功应用的工具是布尔可满足性（SAT）求解器和可满足性模理论（SMT）求解器（De Moura和Bj?rner，2009）。例如，SAT求解器在解决一些长期存在的数学问题方面取得了成功，包括埃尔德什差异猜想（Konev和Lisitsa，2015）、布尔毕达哥拉斯三元组猜想（Heule等人，2016）以及第五Schur数的确定（Heule，2018）。另一方面，SMT求解器越来越多地被用作证明助手的子程序（B?hme和Nipkow，2010；Ekici等人，2017），以自动解决证明目标。在这些应用中，SAT/SMT求解器通常需要生成证明，这些证明可以由证明检查器独立检查以确保求解器输出的正确性。与MILP特别相关的一个理论是线性整数实数算术理论，先进的SMT求解器如Z3（De Moura和Bj?rner，2008）、cvc5（Barbosa等人，2022）和MathSAT5（Cimatti等人，2013）支持证明生成。
尽管MILP求解器返回的答案的验证尚未像SAT/SMT社区中的类似求解器那样成熟，1，但已经取得了重要进展。最初的努力是对一个大型TSP问题的最优性进行认证（Applegate等人，2009），随后使用次加性生成函数来认证最优性（Cheung和Moazzez，2016）（但不包括不可行性）。一个重要的里程碑是提出了VIPR 1.0（验证整数规划结果），这是第一个用于MILP实例的通用分支定界证书格式，可以处理最优性、不可行性和放宽的最优性界限（详见定理1）。VIPR 1.0的设计考虑到了简洁性，由一系列可以使用有限数量的推理规则依次验证的声明组成（Cheung等人，2017；Eifler和Gleixner，2024）。这种带有额外保障措施的证书格式被用于Chvátal猜想的特殊情况的证明（Eifler等人，2022）以及3-sets猜想的证明（Pulaj，2023）。VIPR 1.0格式目前实现在最新版本的exact SCIP（Cook等人，2011）中，并附带一个用于相应证书的检查器（viprchk，用C++实现）。为了简洁起见，在本文的其余部分我们将VIPR 1.0称为VIPR；本文中提到的VIPR格式的数学形式化会省略类型字体（例如，我们正式讨论VIPR证书，但我们的实现使用的是VIPR文件格式）。
虽然viprchk作为一个参考工具仍然很有用，并且注重性能，但它明显缺乏与其算法正确性相关的形式推理。更复杂的是，一些VIPR规范表述不正式，或者如我们在3.1小节中指出的那样没有明确说明。此外，viprchk的实现并非完全独立于MILP求解器：根据它检查的证书，viprchk可能依赖于预期的MILP求解器行为来进行算法检查，而不仅仅是依赖规范。为了说明这一点，在3.2小节和附录C中，我们展示了viprchk返回错误或模糊答案的简单VIPR证书。尽管不太可能有成熟的MILP求解器产生这样的证书或类似的证书，但根据规范这是可能的。最后在3.1小节中，我们指出了viprchk对VIPR证书的index属性的非批判性使用，这种属性旨在实现内存管理和快速性能，但这从根本上要求信任相关的MILP求解器，可能会影响验证的正确性。
我们进行这项工作的动机是解决上述问题，以便提供可行的viprchk替代方案。我们的主要贡献如下。首先，由于一些VIPR规范是用非正式语言描述的，我们引入了更正式的定义来消除可能的歧义，从而得到了一个精确的有效性概念（第3节），特别是不再使用index属性。其次，我们将VIPR证书的有效性与线性整数实数算术理论中的无变量无量词谓词（基础公式）等价起来（定理2）。第三，我们使用Why3的演绎逻辑框架（Bobot等人，2011）正式验证了我们谓词构造的正确性，表明VIPR证书有效当且仅当相应的谓词评估为真。最后，我们通过使用可满足性模理论库（SMT-LIB）实现了一个检查器框架，并使用cvc5验证其有效性。在第5节中，我们使用文献中的相关基准实例评估了我们的检查器。
我们的方法不仅在验证方面有优势，因为我们的形式化有助于阐明规范本身的期望结构。例如，在3.3小节中，我们看到一些VIPR规范在允许空洞有效推导方面是宽容的，这种推导是MILP求解器首先不会考虑的。虽然这种宽容的有效性概念在某些情况下可能是可取的，但它可能会因冗余或无用的信息而影响验证时间。我们的形式化可以根据应用目标适应更强或更弱的有效性概念，对规范和等价谓词进行最小的修改。最后，由于其灵活性，可以轻松地将额外的推理规则集成到我们的现有框架中。
我们在验证方面的贡献有两个方面。首先，我们使用Why3的自动演绎逻辑框架在逻辑层面正式验证了我们转换的正确性（Bobot等人，2011）。这样做的主要优势是我们的转换是与实现无关的。根据对运行时计算的信任程度，可以使用任何选择的工具轻松评估我们的谓词，因为谓词是完全明确地编写的，并且经过了形式验证。
其次，我们使用cvc5（一个先进的SMT求解器）实现了我们的构造，确保了运行时和逻辑层面的稳健验证。然而，我们强调我们实现的检查器是SMT求解器不可知的，因为任何符合SMT-LIB的求解器都可以用来评估等价谓词，只需对实现进行少量修改。此外，由于我们评估的是一个基础公式，我们在第5节中使用SMT求解器cvc5也可以用模型验证工具（如Dolmen（Bury和Bobot，2023）代替。重要的是，我们的合取公式的布尔表达式在其检查中很容易实现并行性，这是我们在分析框架中探索的一个特点。最后，随着像SMT Lean（Mohamed，2025）这样的正在进行的项目的支持，这些项目支持线性整数实数算术理论，进一步与交互式定理证明器的集成也是可行的。有关向更安全的VIPR证书检查器以及潜在集成或扩展的进一步讨论，请参阅第4.2节。与该项目相关的所有代码都可以在GitHub上免费获取。
本文的其余部分组织如下。第3节提供了MILP和VIPR证书的概述，我们为了简洁起见进行了抽象描述，但仍然不失一般性；第3节还描述了给定VIPR证书的有效性。第4节仔细定义了VIPR证书中的基础公式，并进一步证明了该公式的等价性。第5节介绍了在已知基准上进行的设计评估。最后，我们的结论性意见在第6节中。
