AIMing: Automated Theorem Proving for Advancing Mathematics

With the ever-widening use of software in safety-critical applications such as autonomous vehicles, design defects are becoming increasingly catastrophic in their consequences. Formal, mathematical techniques to prove the correctness of software provide a promising approach to ensure the safety of such systems. However, formal verification of complex systems often requires an impractical level of human effort: automated theorem provers (ATPs) typically do not scale to real-world applications, forcing correctness proofs to be written largely by hand in interactive theorem provers (ITPs). A similar challenge has arisen in mathematics, where there is growing use of ITPs to formalize (and sometimes find mistakes in) proofs: the lack of scalable automation puts formalization beyond the reach of most working mathematicians. This project aims to address these challenges by developing new techniques allowing ATPs to scale to complex theorems, as well as tools usable by mathematicians for proof formalization. Enhancing the scalability and usability of ATPs will reduce the barrier to entry for safety-critical system designers and mathematicians to verify their systems and proofs, helping to make these safer and more trustworthy. The project has three primary research thrusts. The first two thrusts tackle several obstacles to using Large Language Models (LLMs) to automate proof construction, turning an ITP into an ATP: data scarcity, sparse rewards, and lack of self-play. Thrust 1 will address the data scarcity problem by generating synthetic theorems and proofs: the project will develop LLM-based techniques to generate human-like theorem statements and proofs, as well as techniques for translating between formal theorems/proofs and informal, more easily-interpretable versions. Thrust 2 will address the self-play and sparse reward problems by exploiting high-level structure in proof search: the project will develop techniques to synthesize lemmas providing easier-to-prove intermediate steps on the way to a desired theorem, as well as techniques to guide proof search using human feedback. Finally, the last thrust seeks to ensure that the project's advancements in ATPs transfer to advances in mathematics, and that the developed tools will be useful for working mathematicians. Towards this end, Thrust 3 will apply the project's tools to study important conjectures in the theory of linear groups. 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.