Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

ProofGap: Benchmarking Step-Level Formal Reasoning with Local Obligations Derived from Natural-Language Solutions

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

what is proved or measured

ProofGap is a benchmark-construction and checking pipeline. It starts from 3,015 textbook mathematical-analysis exercises and yields 26,116 local proof gaps (8.66 per exercise on average; median 7; 8.33 assumptions per gap on average; median 6; §3.3, p. 6). The paper states: “To construct ProofGap, we build on a verifiable auto-formalization pipeline based on the Relaxed and Core Natural Formal Languages.” (§1, p. 2) The benchmark measures local obligation discharge separately from whole-theorem proving, not natural-language translation itself.

The reported Lean evaluation uses eight candidates per target, each capped at 8,192 tokens, and Lean checks correctness; Pass@k is the standard estimator and gap scores are micro averages, while exercise diagnosis is macro coverage (§5.2, p. 7). On all 26,116 gaps, Pass@8 is 35.39% for Goedel-V2-8B, 33.27% for DeepSeek-Prover-7B, and 31.99% for Kimina-Distill-8B (Table 3, p. 7). The same models obtain 4.28%, 3.32%, and 2.92% on the 3,015 parent theorems, respectively. On ProofGap-280, GPT-5.6-sol and Claude-Opus-4.8 both reach 87.86% gap Pass@8, but parent-exercise Pass@8 is 21.43% and 13.93% (Table 7, p. 8). These denominators and paired settings matter: local context contains earlier established facts, whereas a parent theorem starts only from its original premises (§5.3.2, p. 8).

technique: preserve proof structure in a relaxed intermediate language

Use this when converting natural-language solutions into machine-processable proof states without committing immediately to Lean syntax. The paper’s procedure is: (1) preprocess the corpus by removing figure-dependent problems, splitting independent subquestions, and normalizing problem/solution boundaries (Appendix A.1, p. 12); (2) prompt an LLM with Relaxed NFL syntax, format requirements, and examples (Appendix A.2, p. 13); (3) parse the output; (4) screen representation consistency against assumptions, goal, proof steps, unsupported intermediate claims, and method annotations (Appendix A.2, p. 13). Relaxed NFL retains GIVEN, TO PROVE, Have, Assume, It suffices to prove, We prove that, witnesses, and [@method M @] (Table 8, p. 12). The paper cautions: “This screening does not claim to prove that the natural-language solution and Relaxed NFL are equivalent in full mathematical semantics.” (Appendix A.2, p. 13)

Verus form (Inference): represent each source step as a Rust/Verus proof obligation with explicit requires facts and an ensures conclusion; use a proof function for the local derivation and ordinary Rust only for executable computation. Relaxed NFL itself does not carry to Verus, so its parser and structural screen would be an external front end. The local-context/goal split does carry over as a useful contract-generation boundary.

Evidence and limits: parser validation and consistency screening are filters, not semantic proof. The paper’s Lean translation maps local declarations and assumptions to Lean binders and the gap goal to the theorem conclusion, then pairs each statement with a Lean-verified proof; multiple LLM reviewers cross-review translations, and any flagged ambiguity is escalated to human adjudication (§3.2, p. 5). The benchmark covers one analysis textbook, uses Lean only, and “does not directly measure natural-language autoformalization, invalid-step detection, or end-to-end proof composition.” (§6, p. 10)

technique: elaborate to a normalized proof AST

Use this when local obligations need stable semantics despite overloaded notation and implicit scopes. Core NFL has proof states Γ ⊢ G and constructors Forward(M,P,π), Backward(M,P,π), Subgoal(P,π1,π2), and QED (Appendix A.3, pp. 14–15). Elaborate Relaxed NFL by recovering variable scopes, disambiguating notation, splitting compound propositions, and canonicalizing analysis notation; deterministic transformations are used where possible, with constrained LLM choices checked programmatically (Appendix A.3, p. 14).

For overloaded notation, propagate IsReal/IsSet annotations and rewrite |t| to Abs(t) or Card(t) when the environment determines one interpretation; otherwise ask the model to choose from a finite candidate set using only local context and check consistency (Appendix A.3.1, p. 15). Split Have a < b < c into Have a < b, Have b < c, and Have a < c; split conjunctions similarly (Appendix A.3.2, p. 16). Mark free variables, attach explicit scope annotations, and eliminate them into quantifiers; the checker requires every free variable to lie in a matching scope and forbids other proof changes (Appendix A.3.3, p. 16). Canonicalize derivatives as FunDeri and indefinite integrals as equalities between sets of antiderivatives (Appendix A.3.4, pp. 16–17).

Verus form (Inference): use explicit quantified spec fns and forall/exists expressions, with assert and calc blocks for split intermediate facts. There is no direct Verus analogue of FunDeri or integral-set semantics; those require domain-specific specifications and lemmas. The scope-recovery discipline is directly applicable because Verus proofs also fail when binders or domains are implicit.

technique: generate and check local obligations

Apply this after Core NFL elaboration. For each constructor, generate a gap from the current assumptions and goal: Forward checks the intermediate proposition before adding it; Backward checks the original goal under the proposed subgoal; Subgoal checks the subproof then continues with the proposition; QED checks the current goal (Appendix A.4, p. 17). A gap is Γ ⊢M G; the method annotation is only a hint and does not alter validity. Every generated gap must pass CheckGap; the complete program passes only when all gaps pass (Appendix A.4, p. 17).

Verus form (Inference): generate one Verus proof function per local step, carrying prior facts as parameters or requires, and compose the functions through assert/lemma calls. Keep each obligation independently checkable so a failed assertion identifies a source step. This is a design mapping, not a claim that the paper implemented Verus.

technique: conservative replayable DSL and verifier-guided repair

For an executable certificate, emit a line-oriented DSL program over 18 commands: autosolve, apply, fact management, quantifier operations, scoped rewrites, branching, and assert (§4, p. 6; Appendix B.1, pp. 19–20). The checker recomputes state transitions, uses capture-avoiding substitution and α-equivalence, rejects unsupported solver input as unknown, and requires every branch to close (Appendix B.2, pp. 21–22). The workflow atomically claims a gap, pins checker/library versions, assigns a budget, runs isolated attempts, records the first failure and residual state, escalates stalled FAST attempts to targeted DEEP search, then requires admit-free root replay and semantic audit before accepting a certificate (Appendix B.5, p. 24). Autosolve directly closed 2,838/26,116 gaps (10.87%); the verifier-guided workflow added 4,889, for 7,727/26,116 (29.59%) (§4, p. 6). The denominator is all benchmark gaps, and the second number is additional gaps after the first stage.

Verus form (Inference): use Verus compilation as the deterministic checker, isolate candidate files, pin the Verus revision and dependencies, retain failed proof states/logs, and replay accepted proofs from a clean root. Replace DSL commands with valid Verus constructs such as assert, calc, lemma declarations only where supported by the local Verus guide, and proof-function calls that are erased after verification. Do not treat a proof pass as evidence that the specification matches intent.

trusted boundary, failures, and VL threat

The checker, parser, solver portfolio, theorem-library snapshot, Lean kernel, semantic reviewers, and source-to-formal translation are trusted to different extents. The paper explicitly says unsupported solver input returns unknown and that checks cannot guarantee full mathematical semantics (Appendix A.6, p. 18). Inference: for VL, the useful product lesson is a traceable local-proof loop with explicit assumptions, replay, and typed failure—not automatic discovery of the right Rust specification. ProofGap shows a substantial threat from local proof failures being misread as whole-program failure or success, and from semantic translation errors being hidden by a compiling formal target. Existing work already covers local proof benchmarking and verifier-guided repair; VL should reuse these interfaces rather than claim novelty for step-level feedback alone.

techniques for the catalog

  • relaxed-to-core proof representation — preserve natural proof structure, then elaborate it into an explicit proof-state AST
  • notation and scope elaboration — resolve overloaded terms, binders, compound propositions, and analysis notation with checked transformations
  • proof-gap generation — turn each AST transition into a local Γ ⊢ G obligation tied to a source step
  • replayable verifier DSL — execute deterministic state transitions, reject unsupported automation, and require all branches to close
  • verifier-guided workflow — combine bounded candidate generation, isolated checker feedback, replay, and semantic audit

Checked 2026-10-15 against the paper by a Codex agent for proofgap_20261014.md: checked quotations, numbers, references, techniques, and conclusions; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: