Data-driven lemma synthesis for interactive proofs
Data-driven lemma synthesis for interactive proofs
复制标题
用于交互式证明的数据驱动引理合成
DOI：
10.1145/3563306
复制
发表时间：
2022
影响因子：
--
通讯作者：
Millstein, Todd
中科院分区：
文献类型：
--
作者：
Sivaraman, Aishwarya;Sanchez-Stern, Alex;Chen, Bretton;Lerner, Sorin;Millstein, Todd
定理的交互式证明通常需要辅助引理来证明所需的定理。现有的自动合成辅助引理的方法分为两大类。一些方法是目标导向的，产生引理专门帮助用户从给定的证明状态取得进展，但它们在可以产生的引理方面的表现力有限。其他方法具有很强的表现力，能够从给定的语法生成任意引理，但它们是完全无向的，因此不适合交互使用。关键的新颖性是一种技术，用于将引理综合归结为数据驱动的程序综合问题，从而从当前证明状态生成综合示例。我们还描述了一种系统地为引理合成引入新变量的技术，以及用于过滤和排序候选引理以呈现给用户的技术。我们在一个名为lfind的工具中实现了这些想法，该工具可以作为Coq策略运行。在对四个基准测试套件的评估中，lfind在68%的人类证明者使用引理取得进展的情况下生成了有用的引理。在这些情况下，lfind会合成一个引理，该引理要么支持对原始目标的全自动证明，要么与人类提供的引理匹配。
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.
登录
查看更多内容
使用天使执行的递归函数程序的自下而上综合
DOI：
--
发表时间：
2021
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
Anders Miltner;A. Nunez;Ana Brendel;Swarat Chaudhuri;Işıl Dillig
通讯作者：
Işıl Dillig
SMT 求解器的归纳
DOI：
--
发表时间：
2015
期刊：
International Conference on Verification, Model Checking and Abstract Interpretation
影响因子：
--
作者：
Andrew Reynolds;Viktor Kunčak
通讯作者：
Viktor Kunčak
DOI：
10.1007/bf00244460
发表时间：
1996-03-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Ireland, A;Bundy, A
通讯作者：
Bundy, A
DOI：
10.1007/978-3-540-45085-6_22
发表时间：
2003-07
期刊：
--
影响因子：
--
作者：
L. Dixon;Jacques D. Fleuriot
通讯作者：
L. Dixon;Jacques D. Fleuriot
通过与证明助手交互学习证明定理
DOI：
--
发表时间：
2019
期刊：
International Conference on Machine Learning
影响因子：
--
作者：
Yang, Kaiyu;Deng, Jia
通讯作者：
Deng, Jia