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.

交互式定理证明器使程序员能够证明其软件的正确性和安全性。然而，如今所需的手动证明工作量非常大，这严重限制了这些强大工具在实践中的使用。该项目开发自动化来解决证明程序属性的关键挑战：需要识别完成证明所需的辅助引理。该项目的新颖之处在于一种自动合成引理的新方法，以及对候选引理进行过滤和排序以供用户检查的技术。软件系统是当今社会各个方面的关键基础设施。该项目的影响是降低获得软件强有力保证所需的成本，并降低使用交互式定理证明器的准入门槛。该项目开发了一种自动引理合成的新方法，该方法结合了现有方法的优点，目标是：具有指导性和表现力。关键思想是将引理综合问题简化为数据驱动程序综合的形式，其目标是综合满足给定的一组输入输出示例的表达式。从当前证明状态生成合成示例可确保生成的引理针对用户的目标。同时，该方法可以利用现成的数据驱动程序合成器，以任意用户提供的语法生成表达式。该项目探索了引理合成的多种表述作为数据驱动的问题，在表达性和易处理性之间做出了不同的权衡；开发过滤和排名的形式，以帮助用户识别最有用的候选引理；将该方法实例化为 Coq 证明助手的策略；并进行自动化实验和用户研究，以告知并迭代改进最终的工具。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Data-driven lemma synthesis for interactive proofs

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

• 发表时间: 2022-10
• 期刊: Proceedings of the ACM on programming languages
• 作者: Sivaraman, Aishwarya;Sanchez;Chen, Bretton;Lerner, Sorin;Millstein, Todd.
• 通讯作者: Millstein, Todd.