一句话：基于数据驱动的不变式推断，在 Rocq 中自动合成蕴含形式的辅助引理以减轻交互式证明负担。
交互式定理证明器（ITP）让程序员能形式化验证软件性质，但用户常需手工找出完成证明所需的辅助引理，尤其是定义关键归纳不变式的引理。现有引理合成方法对蕴含形式引理 P1 ∧ … ∧ Pn ⇒ Q 的支持十分有限。本文提出一种合成有用蕴含引理的技术与工具：基于当前目标与假设的样本赋值，采用数据驱动的不变式推断来探索当前证明状态的强化。作者将该方法实现为 Rocq 中的策略 dilemma。在来自《Verified Functional Algorithms》教材以及已有引理合成基准集的证明上，该工具能有效合成必要的辅助引理，验证了方法的实用性。
Interactive theorem provers (ITP) enable programmers to formally verify properties of their software systems. One burden for users of ITPs is identifying the necessary helper lemmas to complete a proof, for example those that define key inductive invariants. Existing approaches to lemma synthesis for ITPs have limited, if any, support for synthesizing implications: lemmas of the form P 1 ∧ ⋅⋅⋅ ∧ P n ⇒ Q . In this paper, we propose a technique and associated tool for synthesizing useful implication lemmas. Our approach employs a form of data-driven invariant inference to explore strengthenings of the current proof state, based on sample valuations of the current goal and assumptions. We have implemented our approach in a Rocq tactic called dilemma . We demonstrate its effectiveness in synthesizing necessary helper lemmas for proofs from the Verified Functional Algorithms textbook as well as from prior benchmark suites for lemma synthesis.
@article{paperbot2915,
title = {Synthesizing Implication Lemmas for Interactive Theorem Proving},
author = {Ana Brendel and Aishwarya Sivaraman and Todd Millstein},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763131}
}