Steven Hé (Sīchàng)

LLM proof synthesis, search, and learning (authored by agents unless marked 🧑)

what this adds

• evidence checked on October 7, 2026
• this note connects mathematical theorem proving to systems verification
  • the key question is which proof techniques transfer when programs, specifications, and dependencies change
• existing detailed audits remain the starting point
  • AutoVerus and LemmaNet
  • LeetProof
  • StarVerus
  • VeriSkill
  • Vero (local note; not yet published)
  • Proofs Promptly (local note; not yet published)
  • October Verus frontier (local note; not yet published)
• publication status
  • LeanDojo: arXiv comments report NeurIPS 2023 acceptance
  • CoqPilot: arXiv comments report ASE 2024 Tool Demonstrations publication
  • other early sources below were read through their arXiv manuscripts
    • proceedings status was not independently refreshed unless an entry states it
    • an arXiv link alone does not establish whether later peer review occurred
• reported results below are authors’ claims
  • official abstracts and project documentation were checked
  • experiments were not independently rerun
  • different success rates are not directly comparable
    • tasks, model sizes, sample counts, search budgets, and verifier versions differ

three distinct jobs

• selecting an existing fact
  • a premise is a previously proved fact available to the current proof
• choosing the next proof step
  • a tactic is a command that transforms a proof obligation or closes it
• inventing a useful intermediate statement
  • a helper lemma can divide a difficult proof into smaller proofs
• inference: all three occur in systems verification
  • library lemmas handle sequences and maps
  • loop invariants connect one iteration to the next
  • representation lemmas connect concrete memory to an abstract data structure
  • mathematical benchmark performance does not establish performance on these systems tasks

Lean: retrieval, search, and proof decomposition

• LeanDojo / ReProver, Yang et al., 2023
  • authors’ abstract: “augmented with retrieval for selecting premises”
  • contribution: executable interaction with Lean and training data that identifies which premises proofs use
  • important evaluation choice: hold out premises used by test proofs
    • authors’ abstract: “novel premises that are never used in training”
  • inference: a Rust verification counterpart should hold out libraries and projects
    • a random split of similar single-function exercises tests a weaker kind of reuse
• COPRA, Thakur et al., 2023
  • authors’ abstract: “a stateful backtracking search”
  • a general model proposes tactics
  • Lean or Coq executes them
  • failures, search history, and retrieved lemmas inform later attempts
  • evidence includes Lean miniF2F and Coq tasks drawn from CompCert
  • authors’ abstract: “COPRA significantly outperforms few-shot invocations of GPT-4”
  • limitation: this comparison establishes the value of the complete agent configuration on its evaluated tasks
    • it does not isolate every search and retrieval component
• DeepSeek-Prover, Xin et al., 2024
  • authors’ abstract: “8 million formal statements with proofs”
  • pipeline translates mathematical problems, filters statements, generates proofs, and trains on accepted data
  • reported miniF2F result is 46.3% with 64 samples
  • inference: synthetic verified proofs can overcome scarce training data
    • statement quality and task diversity remain separate concerns
• DeepSeek-Prover-V1.5, Xin et al., 2024
  • authors’ abstract: “reinforcement learning from proof assistant feedback”
  • additionally searches a tree of candidate proof continuations
    • Monte Carlo tree search means allocating attempts among branches using results of earlier attempts
  • reported results: 63.5% on miniF2F and 25.3% on ProofNet
  • inference: final checked success can supply training feedback without a human writing every proof
    • a wrong formal statement can still have a valid proof
• DeepSeek-Prover-V2, Ren et al., 2025
  • authors’ abstract: “decompose complex problems into a series of subgoals”
  • recursive proof generation supplies initial training examples before reinforcement learning
  • authors report 88.9% on miniF2F-test and 49 of 658 PutnamBench problems
  • inference: near saturation on one small benchmark can coexist with much lower coverage elsewhere
  • systems opportunity: choose intermediate assertions that make a fixed program easier to prove
    • preserving the original specification must be checked separately

Isabelle: combine model suggestions with established automation

• Thor, Jiang et al., 2022
  • authors’ abstract: “used for premise selection”
  • a hammer searches for proofs using existing automated provers and library facts
  • reported PISA success rises from 39% to 57%
  • authors report 8.2% solved beyond the two components’ separate coverage
    • authors’ abstract: “neither language models nor automated theorem provers are able to solve on their own”
  • inference: a model and conventional prover can cover different failures
    • compare the combined system against both components under equal total resource budgets
• Draft, Sketch, and Prove, Jiang et al., 2022
  • authors’ abstract: “maps informal proofs to formal proof sketches”
  • automated proving fills the smaller gaps in the sketch
  • reported competition-problem coverage rises from 20.9% to 39.3%
  • inference: the useful model output may be a proof plan rather than a complete proof
• LEGO-Prover, Wang et al., 2023
  • authors’ abstract: “a growing skill library containing verified lemmas as skills”
  • generated lemmas are checked, stored, retrieved, and further generalized
  • authors report more than 20,000 generated skills
  • reported miniF2F-test success is 47.1%
  • inference: a verified lemma library is a more directly checkable memory than prose advice
    • usefulness still needs held-out evaluation
    • a valid lemma may be irrelevant or expensive to retrieve

Rocq / Coq: local proof completion and program-derived obligations

• CoqPilot, Kozyrev et al., 2024
  • authors’ abstract: “checks if each proof candidate solves the given subgoal”
  • replaces a proof hole only after checking a candidate
  • combines model candidates and conventional proof methods
  • official project documentation
    • authors: “compiler message could be automatically sent to the LLM with a request to repair it”
  • inference: editor integration is useful evidence for a practical workflow
    • it does not establish autonomous specification generation
• RocqStar, Solovev et al., 2025 / AAMAS 2026
  • authors’ abstract: “retrieval-based premise selection”
  • reported retrieval gain is up to 28% relative
  • authors’ abstract reports multi-agent debate during planning
    • “increases the proof success rate by 20% overall”
  • limitation: “relative” and percentage-point improvements differ
    • the abstract’s planning figure should not be silently read as a percentage-point gain
  • inference: compare additional agents with additional independent attempts at the same cost
• LemmaNet is especially relevant to systems verification
  • the existing AutoVerus citation audit records annotated C, Frama-C obligations, and Rocq helper-lemma generation
  • that note’s scope statement: “assumes an already annotated C/ACSL program”
  • inference: this studies difficult proof completion after intent has been formalized
    • it does not remove the need to determine what the program should promise

Dafny: generate annotations while keeping the target fixed

• dafny-annotator, Poesia, Loughridge, and Amin, 2024
  • authors’ abstract: “adds logical annotations to a Dafny method until the verifier can prove it correct”
  • greedy annotation search uses Dafny feedback
  • synthetic program generation creates additional checked training examples
  • reported Llama 3.1 8B success rises from 15.7% to 50.6% after training on DafnyBench and DafnySynth
  • official README
    • authors: “The methods are assumed to be correctly implemented and formally specified”
  • inference: this is proof support for supplied code and specifications
• DafnyPro, Banerjee, Bouissou, and Zetzsche, 2026
  • authors’ abstract: “a diff-checker that prevents modifications to base program logic”
  • also removes unnecessary invariants and retrieves predefined proof strategies
  • authors report 86% correct proofs on DafnyBench with Claude Sonnet 3.5
  • claimed improvement is 16 percentage points over their base model
  • inference: preventing changes to the target is part of the evaluation method
    • otherwise a proof-generation agent can make the exercise easier by changing the code

F* / Pulse: substantial programs with expert guidance

• Proofs Promptly, Ioannidis et al., ICFP 2026
  • use the existing full-paper and artifact audit (local note; not yet published)
  • authors’ stated human roles include “reading and evaluating the auto-generated specification”
  • authors also report “occasionally supplying a key invariant or proof idea”
  • inference: the interesting next experiment measures expert intervention rather than claiming its absence
    • separate specification corrections, architectural decisions, invariant hints, and routine tool repair
  • existing audit identifies conflicting elapsed-time descriptions
    • use completed checked artifacts as evidence
    • avoid treating estimated manual effort as a controlled productivity measurement

2025–26 frontier: the proof plan itself is a search object

• source status checked on October 7, 2026
  • all five official abstracts and PDFs opened
  • selected method, evaluation, and limitation sections read
  • this is selective full-paper reading, not abstract-only evidence
• Goedel-Architect, Chung, Cai, Li, et al., June 4, 2026
  • status: arXiv preprint
    • peer-reviewed venue not established by this check
  • authors’ §2: “keeps the signature of the original formal statement”
  • method: generate a graph of definitions and lemmas, prove its nodes, and revise the graph after failures
  • authors’ §3.2: “measured at the pipeline level rather than at the prover level”
  • reported 75.6% PutnamBench coverage uses one initial graph and up to 16 refinement rounds
  • reported 88.8% additionally uses natural-language proof guidance and more attempts
  • inference: these are different operating settings
    • one pipeline attempt can contain many model calls
    • the quoted pass@1 distinction is essential when comparing costs
  • systems relevance: a module’s proof dependencies can be revised globally instead of repeatedly repairing one failing assertion
    • this paper evaluates competition mathematics, not maintained Rust projects
• Planning to Hammer / Quarry, Zhang, Di, Li, Yao, and Ma, July 24, 2026 revision
  • first submitted June 16, 2026
  • status: arXiv preprint
    • the PDF has an unfilled ACM article template
    • that alone does not establish peer-reviewed publication
  • authors’ abstract: “type-checks them in Rocq under temporarily admitted sublemmas”
  • method: rank alternative decompositions by estimated difficulty for CoqHammer
  • authors’ Algorithm 1: “solved with a kernel-checked Rocq proof”
  • temporary admissions help check candidate plans
    • final acceptance requires the sublemmas to be proved
  • authors’ §6.4 reports 55%, 52%, and 16% on CoqGym100, Wigderson100, and TransBench58
    • uniform ten-minute wall-clock budget
    • reported gains over the strongest baseline are 7–13 percentage points
  • removing difficulty ranking reduces these rates to 51%, 49%, and 12%
  • inference: selecting an easy decomposition contributes beyond generating several plans
    • the low TransBench58 rate cautions against assuming easy transfer to translated Rust obligations
• Goedel-Code-Prover, Li, Yang, He, et al., August 10, 2026 revision
  • first submitted March 18, 2026
  • PDF states: “Published as a conference paper at COLM 2026”
  • status: conference publication reported by the authors’ PDF
  • method: train one model to decompose obligations and complete proofs
    • the decomposition score is also used to rank plans during search
  • authors’ introduction: “three Lean 4 code verification benchmarks”
  • reported 62.0% aggregate success with an 8B model across 427 tasks
    • Verina: 68.8%
    • CLEVER: 54.0%
    • AlgoVeri: 62.3%
  • inference: this is more directly relevant than competition theorem proving
    • these are Lean verification exercises
    • the result does not establish native Verus support or autonomous specification correctness
  • research consequence: decomposition plus learning is already a strong existing contribution
    • our proposed contribution must target a different failure, such as maintained dependencies or specification changes
• Seed-Prover, Chen, Gu, Huang, et al., August 1, 2025 revision
  • first submitted July 31, 2025
  • status: arXiv preprint
    • peer-reviewed venue not established by this check
  • authors’ abstract: “Lean feedback, proved lemmas, and self-summarization”
  • method: retain proved intermediate lemmas while revising a whole proof
  • authors’ §2.2.4: “This setting completes in 1–2 hours”
    • their light setting already includes 8–16 attempts and 8–16 refinements per attempt
  • reported 81.8% on MiniCTX-v2 uses context from recent formalization projects
  • reported IMO 2025 result combines Seed-Prover with a separate geometry engine
    • it must not be read as six ordinary Lean tasks handled by one prover
  • inference: context-rich evaluation and explicit compute budgets matter more than the word “light”
• Agentic Verification of Software Systems / AutoRocq, Tu, Zhao, Song, et al., April 11, 2026 revision
  • first submitted November 21, 2025
  • PDF publication line: “Proc. ACM Softw. Eng., Vol. 3, No. FSE, Article FSE157”
  • status: FSE 2026 journal publication reported by the authors’ PDF
  • method: query Rocq context on demand and track the branching proof structure
  • program obligations come from annotated C through Frama-C
    • this pipeline supplies the program semantics and verification conditions
  • authors’ §7: “12/60 (20%) lemmas”
  • kernel-utility case study reports 12 of 60 lemmas proved
    • AutoRocq with CoqHammer proves 18
    • PALM proves 10
  • inference: this establishes partial proof automation on program-derived obligations
    • it does not establish complete Linux-module verification
    • local refinement during one proof is distinct from changing model weights across tasks

self-improvement has several meanings

• expert iteration, Polu et al., 2022
  • authors define it as “proof search interleaved with learning”
  • authors’ abstract: “at same compute budget”
  • checked successes become new training examples
• DeepSeek-Prover changes model weights using generated proofs and verifier feedback
• LEGO-Prover changes a library of checked lemmas
• VeriSkill changes reusable prose guidance
  • existing VeriSkill audit quotes the authors’ claim: “first self-evolution framework”
  • inference: claims of a new self-improving verification assistant must account for that work
• inference: these mechanisms should be compared separately
  • training can be expensive but amortized across later jobs
  • libraries need retrieval and dependency management
  • prose guidance can become stale or accidentally contain benchmark solutions
  • report both improvement cost and held-out benefit

research implications

• combined research designs specify the experiments and closest baselines
• retrieval and learned lemmas motivate candidate 3’s dependency-change evaluation
• checked decomposition must compare against Goedel-Architect, Quarry, Goedel-Code-Prover, and P3
  • preserving the original target is an evaluation requirement, not by itself a new method
• recommendation: measure expert hints separately
  • compare no hint, invariant-only hint, and full proof-plan hint
  • include expert preparation time
  • builds on Proofs Promptly and sketch-guided proving
  • hypothesis: a small expert intervention may beat many additional model calls
  • novelty unconfirmed

remaining limits

• this is a cross-language mechanism review
  • it is not a complete ranking of October 2026 proving models
• official source pages were fetched directly when the browser search endpoint failed
• five frontier PDFs and extracted text were added to /hdd1/sichanghe/paper_collection
  • folder names contain the linked title, first three authors, arXiv, and year
  • source versions are recorded in the entries above
• the research proposals above are agent recommendations
  • no novelty claim or performance gain has been established

Last edited: 2026-10-08