Collaborative Research: SHF: Small: Data-Driven Lemma Synthesis for Interactive Proofs

协作研究：SHF：小型：交互式证明的数据驱动引理合成

• 批准号: 2220892
• 负责人: Sorin Lerner
• 金额: $ 25万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2220892&HistoricalAwards=false
• 关键词: Collaborative; Research; SHF; Small; Data

Interactive theorem provers enable programmers to prove correctness and security properties about their software. However, today the manual proof effort required is very high, which severely limits the usage of these powerful tools in practice. This project develops automation to address a key challenge for proving properties of programs: the need to identify the auxiliary lemmas that are required in order to complete a proof. The project's novelties are a new approach to automated synthesis of lemmas, along with techniques to filter and rank candidate lemmas for user inspection. Software systems are critical infrastructure in all aspects of society today. The project's impacts are to reduce the cost required to obtain strong guarantees about software and to lower the barriers to entry for using interactive theorem provers.The project develops a new approach to automated lemma synthesis that combines the strengths of existing approaches, being both goal-directed and expressive. The key idea is to reduce the lemma synthesis problem to a form of data-driven program synthesis, where the objective is to synthesize an expression that meets a given set of input-output examples. Generating examples for synthesis from the current proof state ensures that the resulting lemmas are targeted at the user's goal. At the same time, the approach can leverage off-the-shelf data-driven program synthesizers that produce expressions in an arbitrary user-provided grammar. The project explores multiple formulations of lemma synthesis as a data-driven problem, which make different tradeoffs between expressiveness and tractability; develops forms of filtering and ranking to help users identify the most useful candidate lemmas; instantiates the approach as a tactic for the Coq proof assistant; and performs both automated experiments and user studies to inform and iteratively improve the resulting tool.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

Interactive Theorem侵略使程序员能够证明其软件的正确性和安全性。但是，今天所需的手动证明工作非常高，这严重限制了这些强大的工具在实践中的使用。该项目开发自动化以应对证明程序属性的关键挑战：需要确定为完成证明所需的辅助引理。该项目的新颖性是一种自动合成引理合成的新方法，以及用于过滤和排名候选诱饵进行用户检查的技术。软件系统是当今社会各个方面的关键基础设施。该项目的影响是降低获得有关软件的强大保证所需的成本，并降低使用交互式定理掠夺的进入的障碍。该项目开发了一种新的方法来自动诱使合成，从而结合了现有方法的优势，既是目标又是表现力的。关键思想是将引理综合问题减少到数据驱动程序合成的形式，其中目的是合成一个符合给定的输入输出示例的表达式。从当前证明状态生成综合示例可确保所产生的引理针对用户的目标。同时，该方法可以利用现成的数据驱动程序合成器，这些程序合成器在任意用户提供的语法中产生表达式。该项目探讨了引理合成作为数据驱动问题的多种表述，这些问题在表现力和障碍性之间做出了不同的权衡。开发过滤和排名的形式，以帮助用户识别最有用的候选引理；实例化该方法是COQ证明助手的策略；并执行自动化实验和用户研究以告知和迭代地改善所得工具。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子优点和更广泛的影响评估标准通过评估来提供支持的。

项目成果

Data-driven lemma synthesis for interactive proofs

用于交互式证明的数据驱动引理合成

• DOI: 10.1145/3563306
• 发表时间: 2022
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Sivaraman, Aishwarya;Sanchez-Stern, Alex;Chen, Bretton;Lerner, Sorin;Millstein, Todd
• 通讯作者: Millstein, Todd