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 in the abstract to 71K) 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. ASTactic is evaluated on 13,137 test theorems with at most 300 tactics and a 10-minute wall limit, on two Xeon Silver 4114 cores and 16 GB RAM. It proves 12.2% of the test set alone, 12.8% with auto, and 30.0% with hammer; hammer alone reaches 17.8% at 20 seconds and 24.8% at 10 minutes (Table 1). These fractions use the 13,137-theorem test denominator.

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 2, p. 2)

How to apply it: (1) Build and compile Coq projects; retain only compilable projects. (2) Execute proofs and serialize Coq kernel terms, goals, local contexts, and proof trees. (3) Split projects—not individual proofs—into train, validation, and test sets to measure cross-domain generalization. (4) At runtime, expose the current goals, local context, and environment after every tactic. (5) Declare success only when Coq reports no subgoals.

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; less than 1% of proofs using goal selectors are discarded because their proof-tree parent is ambiguous (Appendix A.2, p. 17). The corpus depends on projects compiling under the chosen Coq version and does not measure proof quality beyond successful checking.

technique: synthetic short proofs from intermediate goals

What it is: Turn intermediate goals in long human proofs into standalone theorems by adding earlier subgoals as premises, then extract proofs of lengths one through four. The paper explains: “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. (3) Convert solved sibling or earlier subgoals into premises; use generalize dependent when a premise mentions a variable absent from G’s context. (4) Take a short sequence of original tactics and append auto, producing a proof of controlled length. (5) Store each synthetic theorem and tactic sequence as a training example. The reported extraction yields 159,761/109,602/79,967/61,126 examples for lengths 1/2/3/4 respectively.

Verus form (Inference): extract intermediate Verus verification states and package discharged subgoals as lemmas or assumptions only when their proof terms are retained. Unlike Coq’s tactic state, Verus does not expose a stable public goal tree, so a tool would need compiler diagnostics or instrumented proof blocks. Treating an unproved subgoal as an assumption would invalidate training evidence; the extracted lemma must remain checkable.

Evidence and limits: The authors do not train ASTactic on synthetic proofs because those contain tactics extracted from human proofs and not full sequences. Synthetic data therefore enlarges the dataset but is not evidence that the model learned from it.

technique: AST tactic generation with semantic argument constraints

What it is: ASTactic encodes goal and premise ASTs with a TreeLSTM, then a GRU decoder expands a tactic AST under a context-free grammar (CFG). Attention selects relevant premises. Arguments are generated by category: premises are scored, integers use a four-way classifier, and quantified variables are sampled from the goal. 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 4, p. 5)

How to apply it: (1) Define a tactic CFG and restrict it to common atomic tactics; exclude compound tactics and user-defined tactics. (2) Encode the goal, all local premises, and up to ten environment premises as AST vectors. (3) Grow an output AST depth-first; at each nonterminal choose the highest-probability applicable production. (4) For apply H-style arguments, score premises with attention; for integers choose 1–4; for induction variables choose a universally quantified goal variable. (5) Train with cross-entropy and teacher forcing so argument losses align with ground-truth trees. (6) At test time, sample a beam of tactics and search complete proofs with depth-first search, backtracking duplicate states.

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 13,137 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). Average runtime rises from 0.2 to 3.9 seconds per theorem. Width 20 is best in this setting, while width 25 declines, showing search saturation rather than monotonic improvement.

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

What it is: Treat generated tactics as actions, execute them in Coq, and use backtracking search; combine ASTactic with automated tactics such as hammer before decomposing a goal. The test protocol permits 300 tactics and 10 minutes.

How to apply it: (1) At each proof state, invoke a portfolio tactic (for example hammer). (2) If it leaves the goal, sample ASTactic candidates with beam search. (3) Execute one candidate, record resulting subgoals, and recurse depth-first. (4) Undo on failure or duplicate proof state. (5) Stop at an empty goal list or resource limit. (6) Keep the proof artifact and replay it through the assistant.

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: Combining ASTactic with hammer proves 30.0% of 13,137 test theorems, versus 24.8% for hammer with a 10-minute limit, a 5.2 percentage-point increase (Table 1). The paper reports that this combination typically finds a proof within ten tactics, while ASTactic alone may need a few hundred; the figure is descriptive and has no separate denominator.

trusted boundary and product threat

Coq’s kernel checks the final proof, but the learned model, dataset extraction, tactic grammar, search policy, and Coq environment remain outside the proof’s logical trust base. The experiments show success on 13,137 held-out Coq theorems, not Rust or Verus. Inference: for VeruLaw, this is a high opportunity and moderate threat. An agent can learn proof-search patterns from a large corpus, but Verus-specific contracts, ownership, solver instability, and unsafe boundaries require a separate dataset and replay checker. The product should retain verifier checking as the acceptance gate and record complete proof source, not only generated tokens.

what VL should not redo

CoqGym already establishes project-level splits, proof-tree extraction, synthetic intermediate-goal data, AST-structured tactic decoding, and verifier-in-the-loop depth-first search. A VL project should not claim these as new ideas. A useful contribution would be a public Verus corpus, diagnostics-to-state representation, and measurements of cross-project generalization and proof repair under dependency changes.

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. Success percentages in Table 1 use the 13,137-test denominator, but the paper does not report confidence intervals or per-project 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 an untested hypothesis.

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 earlier 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 Checked 2026-10-14: audit record yang2019learning; paper-study comparison complete; gate executed; experiments not rerun

Last edited: 2026-10-14