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

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

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.