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

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

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.