一句话：提出数据驱动的引理合成方法，将交互式证明中的辅助引理生成归约为程序合成，并实现为 Coq 策略 lfind。
交互式定理证明常需辅助引理，但现有自动合成方法难以兼顾目标导向与表达力：目标导向方法生成引理受限，基于文法的方法虽表达力强却缺乏方向性，不适合交互使用。本文提出兼具目标导向与表达力的引理合成方法，核心是将引理合成归约为数据驱动的程序合成问题，从当前证明状态生成合成样例；同时给出系统化引入新变量的技术，以及对候选引理进行过滤和排序以便呈现给用户。作者实现 Coq 策略 lfind，在四个基准套件上评估：在人类证明者使用引理取得进展的案例中，68% 能生成有用引理，这些引理或使原目标可全自动证明，或与人工引理匹配。
Interactive proofs of theorems often require auxiliary helper lemmas to prove the desired theorem. Existing approaches for automatically synthesizing helper lemmas fall into two broad categories. Some approaches are goal-directed, producing lemmas specifically to help a user make progress from a given proof state, but they have limited expressiveness in terms of the lemmas that can be produced. Other approaches are highly expressive, able to generate arbitrary lemmas from a given grammar, but they are completely undirected and hence not amenable to interactive usage. In this paper, we develop an approach to lemma synthesis that is both goal-directed and expressive. The key novelty is a technique for reducing lemma synthesis to a data-driven program synthesis problem, whereby examples for synthesis are generated from the current proof state. We also describe a technique to systematically introduce new variables for lemma synthesis, as well as techniques for filtering and ranking candidate lemmas for presentation to the user. We implement these ideas in a tool called lfind, which can be run as a Coq tactic. In an evaluation on four benchmark suites, lfind produces useful lemmas in 68% of the cases where a human prover used a lemma to make progress. In these cases lfind synthesizes a lemma that either enables a fully automated proof of the original goal or that matches the human-provided lemma.
@article{paperbot1454,
title = {Data-driven lemma synthesis for interactive proofs},
author = {Aishwarya Sivaraman and Alex Sanchez-Stern and Bretton Chen and Sorin Lerner and Todd Millstein},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563306}
}