Learning to Prove Theorems via Interacting with Proof Assistants

By Kaiyu Yang, Jia Deng. 2019

190 citations recorded by the source corpus.

Humans prove theorems by relying on substantial high-level reasoning and problem-specific insights. Proof assistants offer a formalism that resembles human mathematical reasoning, representing theorems in higher-order logic and proofs as high-level tactics. However, human experts have to construct proofs manually by entering tactics into the proof assistant. In this paper, we study the problem of using machine learning to automate the interaction with proof assistants. We construct CoqGym, a large-scale dataset and learning environment containing 71K human-written proofs from 123 projects developed with the Coq proof assistant. We develop ASTactic, a deep learning-based model that generates tactics as programs in the form of abstract syntax trees (ASTs). Experiments show that ASTactic trained on CoqGym can generate effective tactics and can be used to prove new theorems not previously provable by automated methods. Code is available at this https URL.

Subfields: Artificial Intelligence, Information Systems, Software, Reinforcement Learning

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Information Systems

In Software

In Reinforcement Learning

Citations in the corpus

Generative Language Modeling for Automated Theorem Proving (2020, methodology): “GamePad [33] and CoqGymn/ASTactic [34] introduce environments based on the Coq theorem prover.”
Formal Mathematics Statement Curriculum Learning (2022, background): “…and lem-mas but very few exercises), we hypothesized that if the difﬁculty of this set of statements was made varied enough, expert iteration could potentially leverage it to effectively shift our models’ distribution closer to miniF2F ’s, and in turn, improve their eventual performance on it.”
Language Modeling for Formal Mathematics (2020, methodology): “There are other datasets which might be suitable for our approach as well, including proofs extracted from HOL4 [Gauthier et al., 2017], and from Coq [Huang et al., 2019, Yang and Deng, 2019, Sanchez-Stern et al., 2019].”
Can Transformers Learn to Solve Problems Recursively? (2023, background): “Once confined to the realm of symbolic methods, some of the most performant tools for synthesizing [3, 4, 21, 5], repairing [16, 35, 41], and even formally verifying [1, 42, 12, 37, 36, 13] programs now rest in part or in whole upon neural foundations.”
Mathematical Reasoning via Self-supervised Skip-tree Training (2020, methodology): “There are other datasets which might be suitable for our approach as well, including proofs extracted from HOL4 [Gauthier et al., 2017], and from Coq [Huang et al., 2019, Yang and Deng, 2019, Sanchez-Stern et al., 2019].”
Large Language Models for Mathematical Reasoning: Progresses and Challenges (2024, background): “Additionally, the C OQ G YM dataset (Yang and Deng, 2019) provides a broad ATP environment, showcasing a rich collection of more than 71,000 proofs penned by humans, all within the framework of the Coq proof assistant.”
NaturalProofs: Mathematical Theorem Proving in Natural Language (2021, methodology): “others use the Coq [19, 48], Metamath [44, 42, 30], Isabelle [24], or Lean [14, 49] environments.”
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving (2020, background): “But due to the difﬁculty of formal mathematics (for humans), such datasets are necessarily small, e.g. containing thousands [11] to tens-of-thousands [37] of theorems — orders of magnitude smaller than the datasets that enabled breakthroughs in areas such as vision and natural language processing.”
Baldur: Whole-Proof Generation and Repair with Large Language Models (2023, methodology): “By contrast with PISA, CoqGym [95], the neural theorem prover benchmark suite for the Coq proof assistant, uses a project-wise split, where training and testing data come from entirely different projects.”
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning (2021, methodology): “Compared to other ITPs, MetaMath is a low-level proving system: each proof step makes only a small step towards the goal.”
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics (2021, background): “Yang & Deng (2019) built CoqGym, a large-scale dataset, which comes also with a learning environment, of 71k human-written proofs in Coq proof assistant.”
A Survey of Deep Learning for Mathematical Reasoning (2022, unknown): “For example, ASTactic (Yang and Deng, 2019) applies TreeLSTM (Tai et al.”
Learning Compositional Rules via Neural Program Synthesis (2020, methodology): “…approaches, including enumerative approaches (Balog et al., 2016), execution guided work (Chen et al., 2018; Zohar & Wolf, 2018; Ellis et al., 2019; Yang & Deng, 2019), and hybrid models (Murali et al., 2017; Nye et al., 2019) However, a key difference in our work is the number of input-output…”
Learning to Reason in Large Theories without Imitation (2019, methodology): “o the unbounded repository of premises. We use the HOList environment [Bansal et al., 2019] in our experiments. Similar to HOList for HOL Light [Harrison, 1996], GamePad [Huang et al., 2019], CoqGym [Yang and Deng, 2019], TacticToe [Gauthier et al., 2017], and Proverbot9001 [Sanchez-Stern et al., 20”