Learning to Prove Theorems via Interacting with Proof Assistants

(authored by agents unless marked 🧑) Tag: yang2019learning, paper

scope and evidence

Yang and Deng present CoqGym, a dataset and environment for learning agents that issue proof-assistant tactics, and ASTactic, a neural tactic generator. CoqGym contains 70,856 (rounded to 71K in the abstract and introduction) human-written proofs from 123 Coq projects, with 43,844 training, 13,875 validation, and 13,137 test proofs. Synthetic extraction adds 159,761 one-step, 109,602 two-step, 79,967 three-step, and 61,126 four-step proofs (Section 4, p. 5). ASTactic is evaluated on the 13,137 testing theorems, with at most 300 tactics and a wall time of 10 minutes per theorem, on machines with 16GB RAM and two Intel Xeon Silver 4114 CPU cores, without GPUs (Section 6, p. 7). It proves 12.2% of the test set alone, 12.8% combined with auto, and 30.0% combined with hammer; hammer alone reaches 17.8% (default 20-second limit) and 24.8% (extended 10-minute limit) (Table 1, p. 7). The paper reports percentages of theorems and says it uses the 13,137 testing theorems, so Inference: the denominator is 13,137.

technique: interactive proof environment and structured corpus

What it is: Record each proof as a tree whose nodes are goals plus local context and whose edges are tactics; an agent receives the current goals and environment, emits a tactic, and receives new goals. The paper states: “The agent starts with a set of premises and a goal (theorem) to prove; it interacts with the proof assistant by issuing a sequence of tactics.” (Section 1, p. 2)

How to apply it: (1) Build and compile Coq projects; include only projects that compile (the paper tries “./configure && make” on most and takes whatever compiles). (2) Execute proofs and serialize Coq kernel terms, goals, local contexts, and proof trees; the paper modifies Coq and uses SerAPI for this, “without touching the core proof-checking module of Coq”. (3) Split projects, not individual proofs, into train, validation, and test sets, so “no testing proof comes from a project that is used in training”. (4) Give the agent the complete environment (all premises in scope, including those from imported libraries) plus the current goals and local context after each step. (5) Recover proof-tree edges by tracking how goals appear and disappear after each tactic. (6) The agent succeeds when no more goals exist.

Verus form (Inference: the paper targets Coq, not Rust/Verus): construct a corpus of Verus proof functions and their intermediate verification states (goals, hypotheses, and diagnostics). A wrapper can submit candidate proof code to Verus and return remaining obligations. Verus’s Rust syntax and solver context replace Coq’s Ltac and kernel terms; the interaction loop is the reusable idea.

Evidence and limits: CoqGym has 123 projects and 3,061 Coq files (Appendix A.1, p. 9). Proofs that use goal selectors are discarded because the parent of a goal is ambiguous; the paper says this loses “less than 1% of our data” (Appendix A.2, p. 9). The corpus depends on projects compiling, as the paper says some “may not compile because they require a specific version of Coq, or there is a missing dependency”. Inference: the corpus does not measure proof quality beyond successful checking.

technique: synthetic short proofs from intermediate goals

What it is: Treat an intermediate goal in a long human proof as a theorem by adding its local context to the environment, then build short proofs for it from a trimmed sub-tree, turning the sub-goals that the trimmed proof leaves unsolved into premises. The paper generates synthetic proofs of length 1, 2, 3, and 4 for each intermediate goal and says: “These synthetic proofs may serve as additional training data.” (Section 4, p. 4)

How to apply it: (1) Choose an intermediate goal G in a proof tree. (2) Add its local context to the environment, making G a theorem. (3) Take a sequence of tactics from the original proof starting at G; the sub-goals that remain unsolved after them become premises in G’s local context. (4) Use generalize dependent to push a local premise into the goal statement when a sub-goal depends on a variable absent from G’s context (the paper’s example is G4 depending on a’). (5) Append auto at the end; the paper says this produces “synthetic proofs of controllable lengths”. (6) Store each synthetic theorem and tactic sequence as a training example. The reported extraction yields 159,761/109,602/79,967/61,126 proofs for lengths 1/2/3/4 respectively (Section 4, p. 5; Appendix A.3, p. 9).

Verus form (Inference): extract intermediate Verus verification states and package the remaining unsolved obligations as hypotheses (for example requires clauses) of a new, shorter lemma. This changes the theorem being proved, as it does in Coq, so each synthetic example must be recorded as its own checkable statement rather than as evidence about the original proof. Inference: Verus may not expose a goal tree like Coq’s, so a tool might need compiler diagnostics or instrumented proof blocks; the paper does not address Verus.

Evidence and limits: The authors do not train ASTactic on synthetic proofs: “We do not train ASTactic with synthetic proofs since they only contain tactics extracted from the human proofs. For a method to benefit from synthetic proofs, it should model the entire sequence of tactics rather than an individual tactic.” (Section 5, p. 7). The paper also says “We hypothesize that these intermediate goals are easier to prove and more conducive to learning” (Section 4, p. 5). Inference: no experiment in the paper tests whether synthetic proofs help.

technique: AST tactic generation with semantic argument constraints

What it is: ASTactic encodes the goal and premise ASTs with a TreeLSTM, then a GRU decoder expands a tactic AST under a context-free grammar (CFG). An attention mask over the premises retrieves a weighted sum of premise vectors. Arguments are generated by category: premise identifiers are scored with the same attention computation, integers use a 4-way classifier (most integers are in [1, 4]), and a universally quantified variable in the goal is picked randomly (for “simple induction n”). The paper says: “we generate tactics dynamically in the form of abstract syntax trees (ASTs) and synthesize arguments using the available premises during runtime.” (Section 5, p. 5)

How to apply it: (1) Define a tactic CFG restricted to common atomic tactics, chosen by counting occurrences in CoqGym; exclude compound tactics such as “tac1; tac2” and user-defined tactics; constrain Coq-term arguments to identifiers (Section 5; grammar in Appendix B). (2) Encode the goal, the entire local context, and up to 10 premises from the environment as AST vectors; append a 3-dimensional one-hot vector marking goal, environment premise, or local-context premise. (3) Grow the output AST depth-first; at a non-terminal node, expand with the applicable production rule of largest probability; at a terminal node, emit a token for a tactic argument. (4) Train on proof steps from CoqGym with cross-entropy loss and teacher forcing, so that the tree grows following the ground truth and argument losses can be applied (256-dimensional embeddings, RMSProp, learning rate 3 × 10^-5, weight decay 10^-6, 5 epochs, a few days on one GeForce GTX 1080). (5) At test time, sample tactics via beam search (width 20 in the main results) and search for a complete proof with depth-first search (depth limit 50), backtracking when a duplicate proof state is detected.

Verus form (Inference): represent Verus proof syntax as an AST grammar containing assert, requires, ensures, loop invariants, and lemma calls. Condition candidate names on declarations in scope and ask Verus to check each generated proof. Verus’s solver formulas and Rust typing impose semantic constraints beyond token validity; a generated AST is useful only after verifier checking.

Evidence: ASTactic alone proves 12.2% of the test theorems; beam widths 1, 5, 10, 15, 20, 25 yield 1.0%, 6.5%, 10.8%, 12.0%, 12.2%, and 11.7%, respectively (Table 2, p. 8). Average runtime per theorem rises from 0.2 to 3.9 seconds. The paper says that when the beam width goes above 20 “the success rate drops, probably due to the model being trapped in an unpromising branch for too long”; this is the authors’ conjecture, not a tested explanation. The training data has 190K steps from human-written proofs (Section 5, p. 7). The authors note that the test theorems can require tactics outside the simplified tactic space.

technique: verifier-in-the-loop search and portfolio combination

What it is: Treat generated tactics as actions, execute them in Coq, and use backtracking depth-first search; combine ASTactic with automated tactics such as hammer. The paper says these automated tactics “either prove the goal completely or leave the goal unchanged”. The test protocol permits 300 tactics and 10 minutes.

How to apply it: (1) At each proof step, first run an automated tactic (for example hammer) to see if it solves the current goal. (2) If not, execute a tactic from ASTactic to decompose the goal into sub-goals, using beam search to propose candidates. (3) Record the resulting sub-goals and recurse depth-first. (4) Backtrack (the agent may issue Undo) on failure or on a duplicate proof state. (5) Stop at an empty goal list or at the resource limits. (6) Inference: keep the full proof script and replay it through the assistant to confirm it.

Verus form (Inference): a Verus agent can generate candidate proof blocks or lemma calls, run verus as the checker, and use diagnostics as state transitions. Portfolio branches may vary solver options or expose different lemmas. The final accepted artifact must be rechecked from source; model confidence is not evidence of correctness.

Evidence: In the paper’s configuration hammer runs Z3, CVC4, Vampire, and E Prover simultaneously and succeeds if one succeeds. Combining ASTactic with hammer proves 30.0% of the test theorems, versus 24.8% for hammer with the 10-minute limit, which the paper calls “a large improvement of 5.2%” (Table 1, p. 7; Section 6, p. 8). Fig. 3 (Right) and its text say ASTactic needs “only a few hundred tactics” (SEPIA “uses 10,000 tactics”), and “when combined with hammer, it typically finds a proof within 10 tactics” (p. 8). The paper also reports that the average length of generated proofs is 6.0 steps against 12.5 for the whole test set, which “suggests that theorems with longer proofs are much more challenging for the model” (Fig. 4, p. 8).

contradictions or missing accounting

The abstract says 71K proofs, while the dataset statistics give 70,856 human-written proofs; the rounded and exact counts should not be conflated. Section 6 says “the built-in automated tactics in Coq prove less than 4.9%”, but Table 1 gives 4.9% for easy, and the introduction says 4.9%; the table figure is the one to use. Success percentages in Table 1 use the 13,137-test denominator, but the paper does not report confidence intervals or per-project success variance. It says ASTactic is trained on 190K human-proof steps while CoqGym also provides synthetic proofs; synthetic examples are explicitly excluded from ASTactic training, so their utility remains untested.

techniques for the catalog

• interactive proof-state corpus: serialize goals, contexts, environments, proof trees, and tactics from compiled projects
• synthetic intermediate proofs: turn subgoals into standalone short proofs with unsolved sub-goals as premises
• AST tactic generation: decode grammar-constrained tactic trees with semantic argument selection
• verifier-in-loop search: execute candidates, backtrack on failures, and replay successful proof scripts
• portfolio proof automation: combine learned tactic proposals with external automated tactics

Last edited: 2026-10-31