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

点击翻译按钮获取中文摘要

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.