Source-linked AI summary
Learning to Prove Theorems via Interacting with Proof Assistants
Kaiyu Yang, Jia Deng
TL;DR
The paper asks how machine learning can automate interaction with proof assistants, whose tactic construction remains labor-intensive and constrained by limited prior datasets and inflexible models. It constructs CoqGym and develops ASTactic, which generates tactics as AST programs; experiments show 12.2% standalone success and 30.0% when combined with ATP systems.
Problem
Automating interactive theorem proving is difficult because human tactic construction is labor-intensive, while prior approaches used small datasets and could not generate out-of-vocabulary tactics.
Method
The paper constructs CoqGym from 71K human-written proofs across 123 Coq projects and develops ASTactic to generate tactics as abstract syntax tree programs.
Results
ASTactic proves 12.2% of test-set theorems, compared with 4.9% for Coq’s built-in automated tactics, and reaches 30.0% combined with ATP systems.
Takeaways & Limitations
ASTactic can generate effective tactics and prove theorems not previously provable by automatic methods.
Takeaways & Limitations
Prior auto-ITP approaches were constrained by datasets of no more than a few thousand theorems and fixed tactic vocabularies.
Abstract
from arXiv · showhide
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 https://github.com/princeton-vl/CoqGym.
1. Introduction
Automating interactive theorem proving requires learning from human-written tactics while addressing limited data and inflexible tactic generation. The paper introduces CoqGym and ASTactic to tackle these challenges.
- Motivation: Automated theorem provers remain behind human experts at efficiently constructing proofs in large formal systems.The gap matters for formal mathematics, software verification, and hardware design.
- Motivation: Interactive theorem proving uses human-entered tactics to express high-level proof techniques while proof assistants handle lower-level details.A successful tactic sequence is executed by the proof assistant as a proof program.
- Motivation: Human involvement makes interactive theorem proving labor-intensive, but existing proofs provide supervision for machine-learning systems.Recent efforts have learned tactic generation from human-written proofs.
- Challenges: Prior auto-ITP work was limited by datasets containing only a few thousand theorems and models unable to generate out-of-vocabulary tactics.Fixed-set copying constrained tactic flexibility because possible tactics can contain functions, arguments, and compound expressions.
- Contributions: CoqGym contains 71K human-written proofs from 123 Coq projects spanning mathematics, hardware, programming languages, and other domains.Its scale and diversity support machine-learning training and cross-domain evaluation.
- Contributions: ASTactic generates tactics as abstract syntax tree programs by composing grammar productions with tokens available at runtime.The model takes Coq goals and premises as input and outputs a tactic in a subset of Coq’s tactic language.
- Results: ASTactic generates effective tactics and can prove new theorems beyond the reach of previous automatic provers.The reported test-set success rate is 12.2%, compared with 4.9% for built-in automated tactics; combining the model with ATP systems raises success to 30.0%.
2. Related Work
Prior theorem-proving systems automate proof search but remain limited by large search spaces, small and narrow datasets, and inflexible tactic generation. CoqGym addresses these gaps with broader higher-order-logic data and AST-based tactic generation.
- Automated theorem proving: Modern automated theorem provers use resolution-based first-order proof search, but large search spaces remain challenging.Some proof assistants instead connect to external ATP systems through translation and proof reconstruction.
- Learning to interact with proof assistants: Learning-based proof-assistant systems include finite-state tactic sampling, retrieval-based tactic selection, and SMT-oriented tactic generation.SEPIA samples paths from a finite automaton, while TacticToe retrieves candidates and evaluates them with learned search.
- Learning to interact with proof assistants: Prior auto-ITP models cannot generate tactics outside fixed, predetermined tactic sets, limiting out-of-vocabulary generalization.Coq tactics may contain functions, arguments, and compound expressions, unlike the simpler argument spaces handled by FastSMT.
- Datasets for theorem proving: CoqGym targets higher-order logic and high-level tactics, whereas many prior datasets focus on first-order logic and low-level proofs.HOList provides a related proof-assistant dataset, but its method does not generate tactics as ASTs.
- Datasets for theorem proving: CoqGym contains 71K theorems from 123 diverse Coq projects, compared with 1,602 theorems from the Feit–Thompson development in GamePad.It also augments human proofs with synthetic proofs extracted from intermediate steps.
3. Background on Coq
Coq combines a language for mathematical objects, theorems, and proofs with machine-checked semi-automatic proof construction. Users interact backward from a goal by applying tactics, producing a proof tree that can be modeled as an agent dialogue.
- Coq as a proof assistant: Coq supports certified software and hardware development and mathematical proofs through a functional language and machine-checked proof construction.Its applications include the Feit–Thompson theorem.
- Proof construction: A Coq proof starts with a theorem as the initial goal and repeatedly applies tactics to create sub-goals until none remain.Users may inspect feedback and backtrack during this trial-and-error process.
- Proof trees and tactics: The proof tree has the original theorem as its root, goals as nodes, and tactics as edges connecting goals to resulting sub-goals.Each goal has a local context, while goals share the same environment.
- Proof trees and tactics: Tactics range from simple commands to argument-bearing and compound expressions defined by Coq’s Ltac language.For example, “simpl; apply H” performs two operations sequentially.
- Learning interaction: From a machine-learning perspective, Coq theorem proving resembles task-oriented dialogue: an agent observes goals and contexts, then generates an Ltac tactic.The proof assistant returns new goals after executing each tactic.
4. Constructing CoqGym
CoqGym is constructed by extracting structured runtime information from compiling Coq projects and augmenting human proofs with shorter synthetic proofs. Its project-level splits support cross-domain generalization evaluation.
- Dataset and representation: CoqGym provides 71K human-written proofs from 123 Coq projects, together with ASTs, environments, goals, and proof trees.The structured representation exposes syntactic and semantic information beyond raw source code.
- Project processing: The dataset includes only projects that compile, excluding projects requiring unavailable Coq versions or missing dependencies.Projects are organized around inter-related proofs in particular domains.
- Project processing: The training, validation, and test sets contain 43,844, 13,875, and 13,137 proofs, respectively, with test proofs held out by project.This split is designed to measure generalization across domains.
- Dataset and representation: CoqGym serializes interpreter-extracted OCaml ASTs into Lisp-style S-expressions and supplies Python tools for using them.The environments are represented as Coq kernel terms obtained by executing proofs and serializing Coq internals.
- Dataset and representation: Unlike prior work, CoqGym supplies each proof’s complete environment, including premises from the same source file and imported libraries.This gives models access to relevant information in structured form.
- Dataset and representation: Each proof is represented as a tree whose nodes contain goals and local contexts, while edges are tactics that decompose goals into sub-goals.Edges are identified by tracking goals as they emerge and disappear during proof execution.
- Synthetic proofs: Synthetic proofs of lengths 1 through 4 are extracted from intermediate goals in human-written proofs to add shorter training examples.The authors hypothesize that intermediate goals are easier to prove and more conducive to learning.
- Dataset statistics: CoqGym records 70,856 human-written proofs, averaging 8.7 intermediate goals and 9.1 steps per proof.Its synthetic collection contains 159,761 one-step, 109,602 two-step, 79,967 three-step, and 61,126 four-step proofs.
5. ASTactic: generating tactics as programs
ASTactic generates Coq tactics dynamically as grammar-constrained AST programs, using encoded goals and premises to synthesize context-specific arguments. At test time, sampled tactics guide depth-first search for complete proofs.
- Unlike fixed-set approaches, ASTactic dynamically generates tactics in a simplified context-free grammar and synthesizes arguments from available premises at runtime.The grammar excludes compound and user-defined tactics and restricts term arguments to identifiers.
- ASTactic encodes Coq goals and premises as trees, then decodes a program-structured tactic by sequentially growing an AST.The encoder uses TreeLSTM representations, while the decoder generates the tactic AST.
- The model encodes the local context and up to 10 environment premises, leaving selection from the entire environment for future research.Input terms are encoded with a child-sum TreeLSTM, whose root state represents each complete tree.
- The decoder grows tactic ASTs depth-first, selecting grammar production rules at non-terminals and emitting argument tokens at terminals.A GRU updates its state from input embeddings and partial-tree information to control each expansion.
- Runtime argument synthesis uses semantic categories, including premise scoring, four-way integer classification, and random selection of quantified goal variables.These constraints narrow the large identifier and argument search space.
- Training uses extracted CoqGym proof steps, cross-entropy for production rules, and teacher forcing so generated arguments align with ground-truth tree expansions.At inference, beam-sampled tactics are explored with depth-first search, with duplicate proof states pruned by backtracking.
6. Experiments
The experiments evaluate ASTactic for automated Coq theorem proving, including standalone and combined use with existing automated tactics. Results examine success rates, efficiency, and generated-proof lengths.
- Experimental setup: 13,137 testing theorems are evaluated under a limit of 300 tactics and 10 minutes per theorem.The agent observes goals, local context, and environment, and can execute tactics, Undo, and other valid Coq commands.
- Success rates: 30.0% of theorems are proved by combining ASTactic with hammer, compared with 24.8% for hammer alone.The combined system improves the success rate by 5.2 percentage points over hammer alone.
- Success rates: 12.2% of theorems are proved by ASTactic, compared with 4.9% by Coq’s built-in automated tactics.Hammer with its extended time limit proves 24.8% of theorems, providing a stronger standalone baseline.
- Efficiency: Increasing beam width expands the explored tactic search space and raises runtime, but success rate drops above 20.Beam width controls the number of candidate tactics explored at each proof step, trading speed for accuracy.
- Efficiency: ASTactic combined with hammer takes less than 100 seconds per theorem while proving over 3,000 theorems.Built-in automated tactics are faster but prove only a few hundred theorems.
- Efficiency: ASTactic typically finds a proof within 10 tactics when combined with hammer, compared with 10,000 tactics for SEPIA.Standalone ASTactic requires only a few hundred tactics in the reported comparison.
- Generated proofs: Generated proofs are usually shorter than 10 steps, with average lengths of 6.0 steps for generated proofs and 12.5 for the testing set.The comparison uses proof length measured by the number of steps.
- Generated proofs: A generated proof can be shorter than the ground truth because the ring decision procedure solves the goal with fewer tactics.The example reflects the reported difficulty of finding longer proofs.
7. Conclusion
The paper presents CoqGym and ASTactic for learning to prove Coq theorems automatically. Experiments confirm ASTactic’s effectiveness for synthesizing complete proofs.
- Conclusion: CoqGym provides human-written proofs from diverse Coq projects, while ASTactic generates Coq tactics as abstract syntax trees.The paper frames both as contributions to learning theorem proving in Coq.
- Conclusion: Experimental results on CoqGym confirm ASTactic’s effectiveness for automatically synthesizing complete proofs.The conclusion states the result without limiting it to a particular baseline or configuration.
A.1. Building the Coq projects
The authors construct the Coq project collection by compiling required libraries and projects, then automatically building the remaining projects when possible. The resulting collection contains 123 projects and 3,061 Coq files with proofs.
- Building the Coq projects: The standard library and frequently required projects are manually compiled and installed before other projects are built automatically.The automatic process uses simple commands such as “./configure && make” and keeps whatever compiles.
- Building the Coq projects: 123 projects and 3,061 Coq files are retained after excluding files that contain no proof.The file count describes the resulting compiled project collection.
A.2. Reconstructing the Proof Tree
Proof trees are reconstructed by tracking how goals change after tactics are applied. Ambiguous multi-goal cases caused by goal selectors are discarded, leaving an unambiguous tree for the remaining proofs.
- Reconstructing the Proof Tree: When a goal disappears and new goals emerge, the new goals become its children in the proof tree.For example, changing [2, 7] to [8, 9, 7] identifies 8 and 9 as children of 2.
- Reconstructing the Proof Tree: Proofs using goal selectors that affect multiple goals are discarded because their parent-child relationships are unclear.Goal selectors are rarely used, and discarding these proofs loses less than 1% of the data.
A.3. Extracting Synthetic Proofs from Intermediate Goals
The paper converts intermediate goals into premises to extract synthetic proofs, while handling dependencies that are absent from the original goal’s context.
- An intermediate goal can be treated as a theorem by adding its local context to the environment.
- A direct synthetic proof follows the tactics after the intermediate goal in the original human-written proof.For G2, the extracted sequence is “induction a as [|a’]. trivial. simpl; rewrite IHa’. trivial.”
- Trimming the proof subtree can produce shorter proofs by turning unsolved sub-goals into premises and applying those premises.For G2, the remaining proof can use “apply H3. apply H4.” or auto.
- Synthetic proofs can be generated at controllable lengths by selecting tactics from the original proof and appending a completion step.
- Dependent sub-goals require generalize dependent to move missing local premises into the goal statement before forming a well-formed premise.G4 depends on a’, which is absent from G2’s context; generalize dependent produces H4 for the local context.
B. The Space of Tactics for ASTactic
ASTactic’s tactic space is defined by a context-free grammar whose productions describe the tactic programs the model can generate.
- The tactic space is specified by a context-free grammar with tactic expr as its start symbol.
- The grammar includes tactics such as intro, apply, auto, rewrite, simpl, unfold, induction, elim, split, assumption, trivial, and reflexivity.
- Tactic expressions can contain comma-separated terms or rewrite terms, and several tactics accept local identifiers or integer arguments.The grammar defines lists for terms, qualified identifiers, local identifiers, and rewrite terms; integer arguments are restricted to 1, 2, 3, or 4.
- The grammar represents optional clauses for locations, using terms, hint databases, and rewrite directions.Its productions include in, at, using, with, and directional rewrite forms.
- The grammar also includes specialized forms such as destruct, discriminate, inversion, simple induction, constructor, inversion clear, and contradiction.