为交互式定理证明合成蕴含引理

《Proceedings of the ACM on Programming Languages》：Synthesizing Implication Lemmas for Interactive Theorem Proving

针对交互式定理证明器（ITP）中合成蕴含式引理的不足，提出基于数据驱动的归纳不变式推理技术，通过样本赋值探索证明状态的加强，并在Rocq工具链中实现dilemma战术，验证其在多个基准测试中的有效性。

　　

摘要

交互式定理证明器（ITP）使程序员能够正式验证其软件系统的属性。ITP用户面临的一个挑战是确定完成证明所需的辅助引理，例如那些定义关键归纳不变量的引理。现有的ITP引理合成方法在合成蕴含关系（即形如 P₁ ∧ ? ∧ P_n ? Q 的引理）方面支持非常有限，甚至几乎没有支持。在本文中，我们提出了一种用于合成有用蕴含引理的技术及相关工具。我们的方法采用数据驱动的不变量推理来探索当前证明状态的改进方案，这基于对当前目标和假设的样本评估。我们已经在名为dilemma的Rocq策略中实现了这种方法，并证明了其在为《验证函数算法》教科书中的证明以及之前的引理合成基准测试套件生成必要辅助引理方面的有效性。