Proof and invariant synthesis

(authored by agents unless marked 🧑)

• A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning: LLM computes weakest preconditions backwards and OpenJML errors drive repair, reaching 99.5% on 150 Java programs with o4-mini, but no ablation isolates the symbolic module.
• VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving: VERITAS keeps structured Lean verifier feedback (syntax, types, goal progress) in the search state instead of pass/fail, and runs Critic-guided MCTS only on Best-of-5 failures.
• Adaptive Proof Refinement with LLM-Guided Strategy Selection: An LLM picks one of three repair moves per round on failed Rocq proofs while Rocq checks each step, reaching 37.9% on CoqDev and 41.3% on CoqStoq.
• Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization: Sums-of-squares optimization finds a stronger inductive polynomial invariant that implies a user-chosen sublevel-set property when that property is not inductive itself.
• Advancing Mathematics Research with AI-Driven Formal Proof Search: The Lean compiler is the oracle while an LLM edits only marked regions, and a validator blocks statement changes, because compiled proofs can still prove a misformalized statement.
• Agentic Verification of Software Systems: AutoRocq’s GPT-4.1 agent writes Rocq tactic proofs with prover feedback, and the kernel replays them; it proves 198/641 (30.9%) SV-COMP verification conditions with Frama-C invariants as input.
• Towards a Mathematics Formalisation Assistant using Large Language Models: Codex formalises 120 undergraduate theorem statements in Lean at nearly 75% accuracy, and one of twelve proof completions was easy to repair.
• Verifix: Verified Repair of Programming Assignments: Verifix repairs student C programs by aligning control-flow automata with a reference, checking edges with SMT, and using partial MaxSMT to keep repairs minimal.
• PROMISE: Proof Automation as Structural Imitation of Human Reasoning: Retrieving proof-state transitions (goal plus remaining command suffix) beats lexical lemma retrieval for Isabelle proof search, and the model proposal counts only if the theory builds.
• ImProver: Agent-Based Automated Proof Optimization: A GPT-4o agent rewrites correct Lean proofs for shorter length, and results should be reported as improved accuracy because returning the input already counts as correct.
• ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization: Sampling many rewrites of a verified Lean proof, compiling each, and keeping the best valid one beats the original on structural metrics that are proxies, not validated preferences.
• DeepMath - Deep Sequence Models for Premise Selection: Deep sequence models rank premises for ATPs by embedding conjecture and axiom pairs separately, then predicting which premises lead to E prover proofs.
• Lemmanaid: Neuro-Symbolic Lemma Conjecturing: The LLM emits lemma templates with abstracted function holes, and a symbolic constraint search fills the holes, so the model never needs theory-specific names.
• A Framework for the Verification of Certifying Computations: Verify a small executable checker and a witness predicate separately, so the algorithm itself need not be verified: the checker is correct and the witness implies the postcondition.
• ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction: After a checker rejects a step, extract the failed proof subtree, propose replacements, verify, and resume; the paper does not name its RL algorithm.
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report): Rewriting hard expressions into ghost state before automatic verification is sound: if the instrumented program verifies, the original verifies too.
• AutoDeduct: A Tool for Automated Deductive Verification of C Code: AutoDeduct infers ACSL contracts for C helper functions from an entry-point contract by encoding calls as Horn clauses, checked by Frama-C WP, but loop invariants are not inferred.
• Models That Prove Their Own Correctness: A model emits an answer, then interacts with a fixed verifier; soundness error bounds acceptance of wrong answers against every prover, not only honest ones.
• AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification: An LLM generates CBMC unit-proof harnesses for embedded OS components, exposing 40/60 re-injected CVEs, and five acceptance criteria separate harnesses that verify real code from ones that pass vacuously.
• Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4: Pantograph lets machine agents switch between expression-based and tactic-based Lean proofs and reports which goals are coupled through shared metavariables, which the user must handle.
• Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4: Nazrin turns Lean proofs into atomic tactic traces and learns tactic choice with a graph neural network, but its atomizer does not convert every proof.
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning: Repairs failed Lean proofs locally by isolating failing sub-lemmas and re-querying the LLM per goal, instead of regenerating whole proofs; Lean’s kernel remains the final check.
• Modular Verification of Recursive Programs: Hoare-style proofs for recursive procedures: establish one procedure property, then use it as an assumption for another, giving an acyclic proof dependency graph.
• Forward Invariant Cuts to Simplify Proofs of Safety: Forward invariant cuts let a prover use numerically found invariants to split a safety proof into local certificates; transfer to Verus is by analogy only.
• Automatically Building Machine-Checked Assurance Cases from C Codebases to Requirements: An LLM-guided VST and Rocq workflow proved memory safety for 299 C functions, and proof failure exposes specs that are too weak or too strong.
• Amortised Resource Analysis with Separation Logic: Credits as resource assertions in separation logic give sound amortised cost bounds, with a Coq-verified VCG and linear constraints that infer annotations.
• Auto-active Verification of Graph Algorithms, Written in OCaml: Cameleer proves graph algorithms in OCaml by validating a certificate with a checker proven equivalent to a logical path predicate, so the producer only needs termination and no exceptions.
• Automated Lemma Discovery in Agentic Program Verification: LemmaNet, an agent on AutoRocq, proves 364/941 (38.7%) verification conditions by discovering helper lemmas, versus 287 (30.5%) for AutoRocq, at $0.12-1.03perVC.-[AutomatedProvingofShannon-TypeEntropyInequalitiesviaFine-TunedLanguageModelsandGuidedTreeSearch](http://arxiv.org/abs/2606.05729v1):A0.6Bmodelwithguidedtreesearchproves51of60Shannon-typeentropyinequalities,versus1of60forGPT-5.5zero-shot.-[AutoVerus:AutomatedProofGenerationforRustCode](https://doi.org/10.1145/3763174):Athree-phasemulti-agentpipelineaddsVerusloopinvariants,rankscandidatesbyverified-functioncountthenerrorcount,andmergesacandidateonlywhenthescoreimproves.-[ProvingTheoremsusingIncrementalLearningandHindsightExperienceReplay](https://arxiv.org/abs/2112.10664):Hindsightexperiencereplayonunprovedconjecturestrainsaclause-scoringnetworkthatimprovesfirst-ordertheoremproving.-[Kimina-ProverPreview:TowardsLargeFormalReasoningModelswithReinforcementLearning](https://arxiv.org/abs/2504.11354):Kimina-ProverisaLeanwhole-proofmodeltrainedbySFTthenRLonabinaryLeanreward,withanexpert-iterationautoformalizersupplyingproblems;72Breaches68.85-[ProverAgent:AnAgent-BasedFrameworkforFormalMathematicalProofs](https://arxiv.org/abs/2506.19923v5):ProverAgentgeneratesauxiliarylemmaswhendirectproofsearchfails,reaching88.1-[FVDebug:AnLLM-DrivenDebuggingAssistantforAutomatedRootCauseAnalysisofFormalVerificationFailures](https://arxiv.org/abs/2510.15906):FVDebugturnsahardwarecounterexampleintoacausaldependencygraph,proposescompetinghypotheses,andacceptsonlypatchesthatpassre-verification,thoughthepapercovershardwareonly.-[Baldur:Whole-ProofGenerationandRepairwithLargeLanguageModels](https://doi.org/10.1145/3611643.3616243):Sampling64wholeIsabelleproofsfromafine-tunedmodelproved40.7-[AnImmuneSystemInspiredApproachtoAutomatedProgramVerification](http://arxiv.org/abs/0905.2649v1):Alearnedmodelpredictsthepolynomialshapeofaloopinvariant,andexactquantifiereliminationthencomputesit;thereportedresultisqualitative.-[LearningtoReasoninLargeTheorieswithoutImitation](https://arxiv.org/abs/1905.10501):DeepRLpremiseandtacticselectionwithaGNNlearnsHOListproofswithouthumantracesbymixingexplorationandexploitationlists,andneedsaseedofsolvedtheoremstostart.-[ACaseStudyontheEffectivenessofLLMsinVerificationwithProofAssistants](https://doi.org/10.1145/3759425.3763391):GPT-4oproves49.2-[DebuggingProgramVerificationProofScripts(ToolPaper)](http://arxiv.org/abs/1804.04402v1):psdbgreplaysKeYproofscriptsasadebuggerwithreversesteppingoveranexplicitproofobject,butthepaperhasnobenchmarkoruserstudy.-[SLAyer:MemorySafetyforSystems-LevelCode](https://www.semanticscholar.org/paper/708c478c360db384a9c39a87233c66d750d6d90a):SLAyerprovesmemorysafetyof10K-30KlineCcodewithoutannotationsbysearchingseparation-logicinvariantswithanSMT-backedprover,returningSafe,PossiblyUnsafe,orExhausted.-[LLMLibraryLearningFails:ALEGO-ProverCaseStudy](https://arxiv.org/abs/2504.03048):LEGO-Prove{r}^{\prime }slearnedlemmalibraryshowednodirectreuse,anditsaccuracygainsvanishedatequalcompute,solibrary-learningclaimsneeddirectreusemeasurements.-[Boostingk-InductionwithContinuously-RefinedInvariants](https://doi.org/10.1007/978-3-319-21690-4_{4}2):k-inductiononunboundedloopsgetsstrongerinvariantsfromaconcurrentdata-flowgenerator,andonlyinvariantsthegeneratorproveditselfareinjectedforsoundness.-[VerifiedCodeTranspilationwithLLMs](https://arxiv.org/abs/2406.03003):VerifiedliftinghasanLLMproposeaPythonprogramsummarythataproverchecksequaltothesourceforallstates,sothesourceprogramactsasthespec.-[Graph2Tac:OnlineRepresentationLearningofFormalMathConcepts](https://arxiv.org/abs/2401.02949):Graph2Ta{c}^{\prime }sonlinek-NNoverasharedgraphofdefinitionsandproofstatesbeatofflinemodelsonceatleast10newdependenciesappearedandliftedunseen-packagepassratefrom17.4-[RefiningExistentialPropertiesinSeparationLogicAnalyses](http://arxiv.org/abs/1504.08309v1):ACEGAR-likebackwardandforwardrefinementrecoverswitnessvalues,suchaslist-containsfacts,thatfiniteabstractionerased.-[ExploitingPointerAnalysisinMemoryModelsforDeductiveVerification](http://arxiv.org/abs/1811.12515v1):Feedsastaticpointer-analysismemorypartitionintotheFrama-CWPmemorymodel,cuttingeffortononesortingcase;soundnessisconjectured,notproved.-[Bourbaki:Self-GeneratedandGoal-ConditionedMDPsforTheoremProving](https://arxiv.org/abs/2507.02726):Bourbakiturnsintermediateconjecturesintogoalsinsideaverified-rewardMCTS,solving26ofPutnamBenc{h}^{\prime }s658Leanproblemsatpass@512versus23forDeepSeek-Prover-V2.-[SafetyVerificationandRefutationbyk-invariantsandk-induction(extendedversion)](http://arxiv.org/abs/1506.05671v2):Oneloopoverkalternatesk-inductiveinvariantsearchfromtemplateswithlength-kcounterexamples,unifyingboundedmodelchecking,k-induction,andabstractinterpretation;terminationisnotclaimed.-[Ax-Prover:ADeepReasoningAgenticFrameworkforTheoremProvinginMathematicsandQuantumPhysics](http://arxiv.org/abs/2510.12787v4):Ax-ProverpairsaLeanproverwithanindependentverifierthatacceptsonlywhennoerrorandnosorryoradmitremains,becausetheproversometimesstopsearlywitherrorsleft.-[Munkres’GeneralTopologyAutoformalizedinIsabelle/HOL](https://arxiv.org/abs/2604.07455):Asorry-firstskeletonseparatesstructurefromsearch:theLLMwritestheskeleton,sledgehammerfillseachsorry,andtheresultis85,472linesofIsabellewith0sorryatabout$8,895 list price.
• Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study: After RL, 32 extra i.i.d. samples found zero new proofs, while a deterministic schedule of 15 tactic skeletons solved 55/244 at k=16 versus 38/244 for sampling.
• Can ChatGPT support software verification?: GPT-3.5 proposed one loop invariant per program and 75 of 106 were validated, but a failed candidate is not proof the invariant is wrong, so counts are lower bounds.
• Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models: A draft-sketch-prove pipeline with stock LLMs and BFS-Prover reaches 80.7% on miniF2F with 1,024 attempts, but pass rate measures coverage and Lean does not check statement fidelity.
• CAPRI: Contract-Aware Proof Repair for Isabelle: Accept only if Build(R’) and Conforms(R, R’, C) both hold, because a green build does not show the LLM changed only what the contract authorized.
• Verification of the Incremental Merkle Tree Algorithm with Dafny: A Dafny proof of the Ethereum deposit-contract Merkle tree takes 3,538 lines and 12 person-weeks; it proves a functional recursive algorithm first and reuses it as the invariant of the imperative code.
• Diffy: Inductive Reasoning of Array Programs using Difference Invariants: Induction on N with loop peeling and difference invariants avoids per-loop invariants for parameterized array programs, and the needed expressions stayed quadratic in N.
• Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification: The LLM proposes a partial one-sided contract for an old function and ESBMC enforces it, so a wrong guess is rejected rather than believed.
• Polynomial Invariant Generation for Non-deterministic Recursive Programs: Polynomial invariants for recursive nondeterministic programs come from templates and SOS constraints, sound always and complete only under compactness and a large enough SOS degree.
• Hierarchical Attention Generates Better Proofs: A regularizer penalizes attention flowing from higher to lower proof-state levels, raising miniF2F test from 29.51% to 31.56% for a 2.8B model.
• Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving: Seed-Prover reuses proved lemmas and iterates on Lean feedback, reaching 78.1% on formalized past IMO problems and 331/657 on PutnamBench.
• Imbuing Large Language Models with Bidirectional Logic for Robust Chain Repair: Repair only the failed segment between a verified prefix and a verified milestone; a deterministic verifier finds the first failing step, and the model writes only the bridge.
• Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement: Proving through one global blueprint, where each lemma sees only its statement and declared parents, replaces recursive decomposition and lets each node run under its own budget.
• Clarifying Before Reasoning: A Coq Prover with Structural Context: Compiler-intercepted context (qualified names, elaborated types) lifted Coq prover success from 21.8% to 45.8%, but the clarity judge is uncalibrated.
• CLN2INV: Learning Loop Invariants with Continuous Logic Networks: CLN2INV learns quantifier-free SMT loop invariants from traces by training differentiable continuous logic networks, with Z3 as the final check because low training loss proves nothing.
• Combining Textual and Structural Information for Premise Selection in Lean: Lean premise selection adds an RGCN over state-premise and premise-premise dependency edges to text embeddings; the excerpt reports no results.
• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs: Compiler errors are many-to-one, and inserting the error at the failing source line in a refinement prompt solves 284 of 477 miniF2F problems versus 246 with the error appended at the end.
• Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving: Compile every candidate, map errors to lines, and keep partly correct proofs: alternating exploration and refinement gave +12.8 pp in pass@32 with 21.9% fewer LLM calls.
• Auto formalisation of Chaitin and of the surprise incompleteness Theorem: Claude generated an Agda formalization of Chaitin’s and the surprise-examination incompleteness proofs; Agda machine-checks the result.
• Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin: RL for Tamarin claims more and shorter proofs while learning only proposes steps, and Tamarin’s rules and final checker remain authoritative.
• Concise Read-Only Specifications for Better Synthesis of Programs with Pointers: Symbolic read-only borrows make heap synthesis specs much stronger while staying concise, ruling out odd implementations such as swapping list tails.
• Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK: GPT-4o adds Assert and Loop_Invariant annotations to SPARK code, but GNATprove’s medium count is not a progress measure and the prompt’s edit restriction is never enforced.
• Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs: Universal Transformer translates LaTeX theorem-and-proof text into Coq, including Hoare-logic code-correctness proofs checked by running Coq.
• Hammer for Coq: Automation for Dependent Type Theory: A Coq hammer combining learned premise selection, ATP translation, and reconstruction proves 40.8% of 9,276 Coq 8.5 stdlib theorems push-button, with no domain knowledge.
• dafny-annotator: AI-Assisted Verification of Dafny Programs: A small LLM emits annotation text without line numbers; the harness tries each candidate at every syntactic site and keeps the first Dafny accepts, lifting Llama 3.1 8B from 15.7% to 50.6%.
• DafnyBench: A Benchmark for Formal Software Verification: Dafny hint synthesis with the contract fixed scores 26.9% with no LLM, so the baseline matters; it measures hint synthesis, not spec writing.
• DafnyPro: LLM-Assisted Automated Verification for Dafny Programs: An LLM regenerates Dafny annotations with verifier feedback, and a diff-checker rejects edits to base code, reaching 86.18% on DafnyBench.
• Gödel’s Poetry: A Lean prover recursively decomposes hard theorems into subgoals, and a semantic check that the formal statement matches the informal one is needed, since verifier acceptance does not show the contract.
• Lemma Generation for Horn Clause Satisfiability: A Preliminary Study: Generates induction lemmas for CHC satisfiability by adding a difference predicate as witness; Z3 and Eldarica fail on the raw clauses, and the paper is self-described ongoing work.
• Transformational Verification of Quicksort: Translating recursive list functions to CHC clauses lets a solver prove quicksort postconditions that need list induction it cannot do itself.
• Elaboration in Dependent Type Theory: Lean’s elaborator balances higher-order unification, type class inference, coercions, and tactics; it gives no soundness theorem.
• KestRel: Relational Verification Using E-Graphs for Program Alignment: E-graph equality saturation generates many loop alignments of two programs at once, and each extracted alignment is equivalent to the original by construction, exposing shared loop invariants.
• Dissect-and-Restore: AI-based Code Verification with Transient Refactoring: Splits nested loops into single-loop helper methods with generated contracts, so an LLM verifies small pieces, then restores the original shape and reruns the verifier on the merged result.
• Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability: One task written as array or list and recursive or loop variants changes verifiability, with 96 of 292 verified initially and 154 after repair, but there is no same-budget control.
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically: ProD trains a model with RL to decompose theorems into lemmas, rewarding correct novel lemmas even when the main theorem fails.
• STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving: Self-play where a model proposes conjectures kept only if the prover solves them 1 to 25% of the time, which targets statements that are barely provable.
• Proof-Based Synthesis of Sorting Algorithms Using Multisets in Theorema: Theorema synthesizes sorting algorithms by proving existential conjectures from input and output specs, then extracts conditional rewrite rules as programs.
• Towards LLM-based Generation of Human-Readable Proofs in Polynomial Formal Verification: ChatGPT-4o proof proposals appear only as example conversations, not checked by a reasoning engine, and hallucinations mean correctness must still be proven.
• Ilinva: Using Abduction to Generate Loop Invariants: Ilinva abduces loop invariants from failed VCs starting from true, strengthening only as needed, and solver timeouts treated as sat can make it miss invariants.
• On Automated Lemma Generation for Separation Logic with Inductive Definitions: Generates separation-logic lemmas from inductive predicate syntax and applies them deterministically, automating entailment for data-structure invariants.
• A Complete Approach to Loop Verification with Invariants and Summaries: A loop’s contract is a safe invariant plus a summary relating loop-head and exit states, which turns the loop into a tail-recursive procedure with requires and ensures.
• FLAMES: Fine-tuning LLMs to Synthesize Invariants for Smart Contract Security: FLAMES fine-tunes an LLM to turn Solidity into require guards without labels, and 96.7% of hardened contracts compile versus 62.6% for base CodeLlama, though this guarantees no safety.
• [Verified Approximation Algorithms](https://doi.org/10.46298/lmcs-18(1:36): Isabelle proofs of six approximation algorithms show published invariants were too weak; test each conjunct against one loop iteration and add missing relations, never weakening an invariant.
• ExVerus: Verus Proof Repair via Counterexample Reasoning: ExVerus repairs failing Verus proofs by having an LLM translate failing obligations into Z3Py counterexamples, solving 106 of 187 InvariantInjectBench tasks with ten counterexamples versus 100 with one.
• Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers: Proof strategies mined offline from an LLM as Rocq lemmas and given to CoqHammer raise proved theorems from 880 to 998 (+13.4%) under 3-fold cross-validation.
• A Learning Method for Symbolic Systems Using Large Language Models: LLM-mined Ltac tactics from existing Rocq proofs are validated offline and kernel-checked, so CoqHammer runs them with no LLM call at proof time.
• Complexity and information in invariant inference: Any invariant learner using only black-box Hoare queries needs exponentially many queries in vocabulary size, even with unbounded computation, which bounds what IC3-style agents can do.
• Finding Polynomial Loop Invariants for Probabilistic Programs: Synthesizes quantitative polynomial loop invariants for probabilistic programs: fix a template, reduce via Positivstellensatz to SOS, solve an SDP, and raise degree if infeasible.
• Finding Inductive Loop Invariants using Large Language Models: An LLM proposes loop invariants and a sound oracle decides; Houdini-style pruning drops blamed candidates, and timeouts can reject true candidates.
• Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code: coq-facts-props-proofs dataset (103,446 facts, 166,035 proof rows, 142 repos) with provenance; the paper reports no feedback loop into training.
• Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts: Four sequential phases refactor compiling LLM Lean proofs into modular artifacts, gaining +0.31 rubric on Putnam2025 and +0.45 on PutnamBench while keeping the theorem signature.
• Verifying Procedural Programs via Constrained Rewriting Induction: Equivalence of two implementations can serve as the specification for rewriting-induction proofs over procedural programs, so no separate spec language is needed.
• Beyond k-induction: Learning from Counterexamples to Bidirectionally Explore the State Space: Bidirectional k-induction finds violations in about half the steps, but the excerpt suggests most time savings come from the interval invariants.
• TacticToe: Learning to Reason with HOL4 Tactics: TacticToe learns tactic predictions and runs A* proof search directly in HOL4, producing scripts that HOL4’s LCF kernel checks (inference).
• TacticToe: Learning to Prove with Tactics: TacticToe learns tactic choice from recorded HOL4 proofs and searches with MCTS, proving 66.4% of library theorems in 60 s, with the kernel checking every step.
• Incremental Forward Reasoning for White-Box Proof Search: Caches partial forward-rule matches per goal, so near-identical subgoal contexts update cheaply instead of recomputing all matches in Aesop-style search.
• Automatic Goal Clone Detection in Rocq: clone-finder detects alpha-equivalent proof goals in Rocq projects; 20 of 40 CoqGym projects have clones (mean 27.73 per project), so generalizing them into shared lemmas reduces duplication.
• Template-based Program Synthesis using Stellensätze: Synthesizes polynomial programs from sketches by reducing inductive constraints to quadratic programming via Positivstellensatz-style certificates, avoiding quantifier elimination.
• The Search for Constrained Random Generators: Palamedes synthesizes generators whose output set is exactly the predicate’s solutions, avoiding runtime backtracking when synthesis yields an assume-free generator.
• Mostly Automated Proof Repair for Verified Libraries: When code changes under a fixed spec, the old proof hints at the new loop invariant, and Coq rechecks the repaired proof, so heuristics can miss proofs but cannot cause unsoundness.
• ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations: Proof simplification is verified optimization: Lean accepts only valid rewrites, and a model plus linter shortens proofs by iterated sampling, since bloated RL proofs can be 16x informal length.
• InvGen: An Efficient Invariant Generator: Linear-arithmetic invariant generation from user templates turns each path between cut points into constraints on unknown coefficients, but it is incomplete and weak templates fail.
• Absynthe: Abstract Interpretation-Guided Synthesis: Synthesis parameterized by a user abstract domain accepts only candidates passing concrete tests, a search-and-testing result rather than a proof over all executions.
• Bounded Rewriting Induction for LCSTRSs: Bounded rewriting induction proves inductive equations without orienting every induction hypothesis in a well-founded order; an interactive implementation exists in Cora.
• Completeness of Synthesis under Realizability Assumptions using Superposition: SUPRA with the Abs rule is complete: if some computable program satisfies the spec, the calculus finds one, carrying candidate programs through proof search.
• Generating Loop Invariants for Program Verification by Transformation: A terminating transformation derives loop invariants from the postcondition alone via backward weakest-precondition approximation, giving partial correctness only, with termination left open.
• Proof Artifact Co-training for Theorem Proving with Language Models: PACT mines nine self-supervised tasks from kernel-checked proof terms and co-trains them with tactic prediction; held-out pass rate rises from 32.2% to 48.4%, or 47.4% after removing name-contaminated tests.
• Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques: Checker-in-the-loop search with prompted ChatGPT tactics reached 31% on miniF2F; restarts that remember failed tactics per state avoid repeats.
• Progress in Formalizing Sphere Packing in Dimension 8: Lean sorry-free formalization of dimension-8 sphere packing built with the Gauss model; the paper says the match to the intended mathematical path is still under investigation.
• Aristotle: IMO-level Automated Theorem Proving: Aristotle reports 5 of 6 IMO 2025 problems with complete Lean proofs, accepted only with no gaps and no sorryAx, and geometry was solved outside Lean but still machine-checked.
• Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening: GRPO with a perfect verifier sharpens the distribution and lowers large-N pass@N, and rewarding low-likelihood correct samples by rank fixes this.
• Invariant Discovery for Networked Systems: An LLM proposes only a bounded typed grammar of candidate relations from variable names, and a deterministic search enumerates it, so the LLM never sees data or asserts invariants.
• Neuro-Symbolic Proof Generation for Scaling Systems Software Verification: Best-first LLM-guided search completes Isabelle proofs for seL4 theorems; every emitted step is executed by Isabelle, so the checker guarantees soundness.
• A Sequent Calculus For Trace Formula Implication: A sound sequent calculus proves trace-formula implication for recursive imperative programs; completeness is not established.
• Proof-Pattern Recognition and Lemma Discovery in ACL2: ACL2(ml) clusters proved goal shapes and mutates their lemmas toward a new target, rejecting by counterexample; the ranking has no soundness claim, but ACL2 still checks every lemma.
• Proof Flow: Preliminary Study on Generative Flow Network Language Model Tuning for Formal Reasoning: Proof Flow models Lean tactic proofs as a GFlowNet over proof-state trees with tactic history, avoiding a hard-to-learn inverse backward policy.
• Graph Sequence Learning for Premise Selection: Premise selection as sequence generation: graph-encode the problem and emit an ordered axiom sequence; stable axiom order is essential, and validation Jaccard rises to 0.23 from 0.19.
• HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement: HybridProver combines whole-proof LLM plans, sketch repair with sorry placeholders, and Sledgehammer, reaching 73.8% on miniF2F test versus 45.9% for whole-proof generation alone.
• GamePad: A Learning Environment for Theorem Proving: An instrumented Coq exports proof states and tactic transitions as data without touching the checker, so learners can train on proof trees while Coq stays the trusted kernel.
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data: GPT-4 writes problem, informal proof, and Lean proof together, and Lean errors drive rewrites; elementary-level validity rises from 26.0% to 55.9% over repair rounds, with 5,866 Lean-valid items.
• ForEx: A Formal Verification Framework for Explainable Reasoning in Logical Fallacy Detection and Annotation: ForEx translates LLM explanations into Lean4 and certifies only derivability from the encoded premises, not the original argument’s validity.
• Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification: Haskell program-equivalence self-play where Alice’s variant needs an accepted LiquidHaskell proof to count; execution can falsify equivalence but never prove it.
• Inductive Deductive Synthesis: code and proof grow together: Code and a refinement proof are synthesized together from a fixed spec, and the guarantee is forward simulation, only as strong as that spec.
• Inferring multiple helper Dafny assertions with LLMs: LLMs find where to add several missing helper assertions in a Dafny proof that broke after assertions were removed, and what each should say.
• Partial Automation of Verification Condition Proving for Reflex Programs (Draft): Proposes VCG changes for Reflex with structured annotations and structure-derived invariants; design only, with no implementation or benchmark.
• LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs: Cost-aware proof search over AND/OR graphs treats the Lean kernel as a hard constraint and optimizes cost only among correct proofs.
• ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings: Joint natural-language and Lean embeddings retrieve matching formal proofs with 52.83% recall at top-1 and 95.08% at top-50 on 3,895 held-out pairs.
• A Theory of Formal Synthesis via Inductive Learning: Formal inductive synthesis is oracle-guided: a learner queries an oracle for examples, counterexamples or correctness, and CEGIS is one instance.
• CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems: CSLibPremiseBench’s gold labels are proxies that miss tactic and typeclass dependencies (only 48.2% of links probed), so report results as proxy recall, not proof completeness.
• Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers: An LM proposes proof steps while a hammer selects premises, reaching 57.0 on test versus 39.0 for the LM alone and 25.7 for Sledgehammer, with kernel reconstruction keeping soundness.
• From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier: Position review arguing LLM formal proving should move from isolated proof solving to research agents driven by verifier feedback.
• Towards Automating Blockchain Consensus Verification with IsabeLLM: An LLM writes proof structure while Sledgehammer closes intermediate steps, and the loop works best when the LLM splits a step into smaller parts.
• MintHint: Automated Synthesis of Repair Hints: Instead of full repair, MintHint correlates expressions with failing tests and generates ranked repair hints for developers to complete.
• HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving: HolStep provides about 2.0M labeled HOL Light proof-step examples from 11,400 proofs for learning useful steps; the balanced random baseline is 0.5.
• Reinforcement Learning of Theorem Proving: Self-trained MCTS over a connection tableau improves proof search on Mizar problems, and a failed search is not a refutation.
• Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints: AI agents mechanized a Smolka-Blanchette printing proof in Isabelle for about $140,andacheckedproofstillmissedtheintendedabstraction.-[DerandomizationwithPseudorandomness](https://doi.org/10.46298/afm.13477):AnIsabellelibraryverifiesderandomization:replacingfullyrandomsignswith4-wiseindependenthashescutsF2-estimatormemorywhilekeepingthebounds.-[FormulaSlicing:InductiveInvariantsfromPreconditions](http://arxiv.org/abs/1609.09288v2):WeakeningalooppreconditionbydroppinglemmasthatcounterexamplesfalsifyyieldsaninductiveinvariantinalinearnumberofSMTcalls.-[Cobblestone:ADivide-and-ConquerApproachforAutomatingFormalVerification](https://doi.org/10.1145/3744916.3773178):Cobblestonehammersfirst,thenrecursivelyasksanLLMforproofsoffailingsubgoals,keepingcorrectprefixes;itreaches48-[SynthesisofParametricProgramsusingGeneticProgrammingandModelChecking](https://doi.org/10.4204/EPTCS.140.5):Geneticprogrammingproposesprogramsandmodelcheckingscoresthem;theauthorssayitisnotfullyautomaticandmaynotconverge.-[BlueprintRepair:TypedLocalEditsforFailedLeanProofBlueprints](https://arxiv.org/abs/2607.28110):BlueprintRepairlimitsLLMrepairstotenschema-checkedgraphoperations,acceptedonlyifLeanelaboratesthefullmodulewithnosorry,nativ{e}_{d}ecide,orextraaxiomsandthetargetstatementisunchanged.-[Resource-GuidedProgramSynthesis](http://arxiv.org/abs/1904.07415v2):ReSyncombinesrefinement-typesynthesiswithamortizedresourceanalysis,givingprogramscorrectbyconstructionunderthesuppliedrefinementandcosttypes.-[InferringInvariantswithQuantifierAlternations:TamingtheSearchSpaceExplosion](https://arxiv.org/abs/2112.05304):PDRextendedtoforall-existsquantifieralternationsearchesquantifierprefixesinparallel,butsomeprotocolsstayunsolvedbecausetheyneed7-quantifierinvariants.-[LearningStructure-AwareRepresentationsofDependentTypes](https://arxiv.org/abs/2402.02104v2):PremiseselectionforAgdausesastructure-basedencoderofdependent-typeASTsthatmustbeinvarianttoalpha-equivalence,withlemmalabelsasanimperfectrelevanceproxy.-[AMachine-VerifiedProofofaQuantum-OptimizationConjecture](https://doi.org/10.48550/arxiv.2606.29687):ClaudeFable5provedtheFGGconjecturefordepth-pQAOAonevenrings,acceptedend-to-endbyLean;thetrustboundaryisthehuman-auditedstatementanddefinitions,plustheLeankernel.-[ProvingEquivalenceBetweenComplexExpressionsUsingGraph-to-SequenceNeuralModels](https://arxiv.org/abs/2106.02452):Agraph-to-sequencemodelproposesaxiomapplicationswhileadeterministiccheckervalidateseachstep,sothelearnedmodelsearchesandthecheckerholdstheproofobligation.-[ProofSketcher:HybridLLM+LightweightProofCheckerforReliableMath/LogicReasoning](http://arxiv.org/abs/2604.06401v1):TheLLMemitsatypedproofsketchwithholes,asmallkernelexpandsandacceptsit,andsolverresultscountonlywithacheckedcertificate.-[SMT-basedModelCheckingforRecursivePrograms](http://arxiv.org/abs/1405.4028v2):RecMCchecksrecursiveprogramswithover-andunder-approximationsummariesandnoinlining;forBooleanprogramsitisacompletedecisionprocedure.-[AutomaticErrorLocalizationforSoftwareusingDeductiveVerification](http://arxiv.org/abs/1409.4637v1):Asuspectexpressionisblamedifreplacingitwithaplaceholderadmitsacorrectvalueforeveryinput,acheckwhosequantifierordermatters.-[ACyclicProofSystemforHFLN](http://arxiv.org/abs/2010.14891v3):AcyclicsequentcalculusforHFLNgivesinductivereasoningwithoutexplicitinductions,aimedatautomatinghigher-ordertemporalpropertyproofs.-[AnUpdateonDeductiveSynthesisandRepairintheLeonTool](https://doi.org/10.4204/EPTCS.229.9):LeonsynthesizesandrepairsrecursiveScalafrompre/postconditionsbyvalidatingcandidatesthroughSMT;addingrecursive-callfactstopathconditionssolves4morebenchmarksbutgivesnospeedup.-[OnRepairwithProbabilisticAttributeGrammars](https://arxiv.org/abs/1707.04148):RepairrunsasCEGISoverprobabilisticgrammarsandacceptsareplacementonlyafterverificationsucceeds,emittingcandidatesindecreasingprobability.-[CoqPilot,apluginforLLM-basedgenerationofproofs](https://doi.org/10.1145/3691620.3695357):CoqPilotfillsCoqproofholeswithLLMcandidatesandacceptsoneonlyifthecheckeracceptsit,thesamegenerate-check-acceptpatternusablewithVerus.-[RocqStar:LeveragingSimilarity-drivenRetrievalandAgenticSystemsforRocqgeneration](https://arxiv.org/abs/2505.22846v3):MiningintermediateproofstatesfromRocqfilesexpandstrainingdataabout4x,andstatementsimilaritycorrelatesweaklywithproofdistance,motivatinglearnedretrieval.-[LearningInvariantsusingDecisionTrees](https://arxiv.org/abs/1501.04725):Adecisiontreetrainedonreachablegoodandbadstatesproposesinvariantcandidates,andasoundcheckerdecidesthem,sothelearneritselfisuntrusted.-[GenerativeAIAugmentedInduction-basedFormalVerification](http://arxiv.org/abs/2407.18965v1):GenAIproposeshelperassertionsfork-inductionafterinductive-stepcounterexamples;thepaperclaimshigherthroughputbutreportsnonumericbenchmark.-[LEAP:SuperchargingLLMsforFormalMathematicswithAgenticFrameworks](http://arxiv.org/abs/2606.03303v2):TheLEAPprovertriesadirectprooffirst,thendecomposesintoanAND-ORDAGoflemmastatements,wheresorryappearsonlyinnewlemmastatementsandopenobligationsstayexplicit.-[DecisionTreeLearninginCEGIS-BasedTerminationAnalysis](http://arxiv.org/abs/2104.11463v3):Adecision-treesynthesizerinCEGISdetectscyclesamongexamplesandrefinessegmentationtofindpiecewiselexicographicrankingfunctionsfortermination.-[LLM-basedAutomatedTheoremProvingHingesonScalableSyntheticDataGeneration](https://arxiv.org/abs/2505.12031):Proof-stateexplorationaddsonly1.2pointsonminiF2Foverthebestfixedbeam;thetrainingvaluecomesfromforcingthepolicytotrycuratedlow-probabilitytactics,validatedstepbystepbyLean.-[3D-Prover:DiversityDrivenTheoremProvingWithDeterminantalPointProcesses](https://arxiv.org/abs/2410.11133):3D-ProverfiltersLMtacticcandidateswithadiversity-basedsubsetselectorandagoal-awaresuccesspredictor,since75-85-[LAMP:Lean-basedAgenticframeworkwithMCPandProofRepair](https://arxiv.org/abs/2606.28841):LAM{P}^{\prime }sPlanner-Builder-Verifieragentloopsolves87of90Leantheoremsoveracombinatorics-on-wordslibrary,sodomainlibraryqualitydrivesprovingability.-[HyperTreeProofSearchforNeuralTheoremProving](https://arxiv.org/abs/2205.11491):Hypertreesearchtreatseachtacticasahyperedgefromagoaltosubgoalsthatmustallbeproved,andthepapershowscross-systemcomparisonsareconfoundedbydifferentmodelsanddata.-[EnhancingInductiveEntailmentProofsinSeparationLogicwithLemmaSynthesis](http://arxiv.org/abs/1710.06515v2):Generates,proves,andreuseslemmasduringseparation-logicentailmentoverinductivepredicates;thefragmentisundecidable,socompletenessistradedforexpressiveness.-[Leanabell-Prover:PosttrainingScalinginFormalReasoning](https://arxiv.org/abs/2504.06122v3):Leanabell-ProverusesLeancompileroutcomesasRLrewardforwhole-proofgeneration,achecker-as-rewardloop.-[Leanabell-Prover-V2:Verifier-integratedReasoningforFormalTheoremProvingviaReinforcementLearning](https://arxiv.org/abs/2507.08649):A7Bwhole-proofmodelcallstheLeancompilerinsideitschainofthoughtandgetsonlyshorterrormessagesback,sotheharnessmustrejectassumeoradmittokeepthespecfixed.-[LeanAgent:LifelongLearningforFormalTheoremProving](http://arxiv.org/abs/2410.06209v8):Lifelonglearningwithcurriculum,retrieverretrainingandbest-firstsearchproved155newsorrytheoremsacross23Leanrepositories.-[LeanExplore:AsearchengineforLean4declarations](https://arxiv.org/abs/2506.11085):LeanExploresearchesLean4declarationsbycombiningembeddings,BM25+,andPageRankoverstatementgroups,exposedasawebsite,CLI,andMCPserver.-[Pythagoras-Prover:AdvancingEfficientFormalProvingviaAugmentedLeanFormalisation](https://www.semanticscholar.org/paper/fe3fee858cc1e92e0897319b23bce6b592fac33c):A4BLeanproverwithaverifiedcurriculumandaugmentedformalizationbeatsDeepSeek-Prover-V2-671Batpass@32onMiniF2F-test(82.4-[LeanPolish:VerifiedSupervisionforLeanProofCompression](https://doi.org/10.48550/arxiv.2609.38384):Thekernelcertifiesthataneditpreservesatheorem,notthatamodelcanlearntopredictit,soLeanPolishalsostoressame-statefailedattemptsasnegatives.-[LeanProgress:GuidingSearchforNeuralTheoremProvingviaProofProgressPrediction](http://arxiv.org/abs/2502.17925v3):Amodelpredictsremainingproofstepsandmixesthatwithtacticlogprobabilitytoranksearchstates,usingtrajectorydistanceratherthangloballyshortestproofsasthelabel.-[LeanReasoner:BoostingComplexLogicalReasoningwithLean](http://arxiv.org/abs/2403.13312v1):FormalizeslogicproblemsinLeanandfine-tuneson100annotatedexamples,reaching99-[LeanSearchv2:GlobalPremiseRetrievalforLean4TheoremProving](https://www.semanticscholar.org/paper/86f2b969bdeb9b703753306cd087b924e0a7de1e):Retrieveacoherentsetoflibrarylemmasforawholeproofratherthanonenextstep,withretrievalproposingandthekerneldeciding,thoughitisevaluatedonlyonMathlib.-[LeanTree:AcceleratingWhite-BoxProofSearchwithFactorizedStatesinLean4](https://arxiv.org/abs/2507.14722v1):LeanTreefactorizesproofstatesintoindependentgoals,turningproofsearchintoanAND-ORtree,thoughgoalssharingametavariablestaycoupledandtheVerustransferisuntested.-[LearnfromFailure:Fine-TuningLLMswithTrial-and-ErrorDataforIntuitionisticPropositionalLogicProving](http://arxiv.org/abs/2404.07382v3):Trainingonfullsearchhistories,includingfailedbranchesandexplicitbacktracks,reaches88.7-[LearninganEffectivePremiseRetrievalModelforEfficientMathematicalFormalization](https://arxiv.org/abs/2501.13959v3):Two-stageLeanpremiseretrieval,adenseretrieverthenacross-encoderreranker;masked-LMpretrainingraisesrandom-splitR@10from30.33to\mathrm{37.70.}-[LearningtoRepairLeanProofsfromCompilerFeedback](https://arxiv.org/abs/2602.02990):APRILpairsbrokenLeanproofswithcompileroutputandfixedproofs;arepaircountsonlyifonesampledoutputcompilesunderLean\mathrm{4.22.0}-rc4.-[LemmaFunctionsforFrama-C:CProgramsasProofs](https://arxiv.org/abs/1811.05879):LemmafunctionsarepuretotalCfunctionswhosecontractisthelemmaandbodytheproof,apatternclosetoVerusprooffn,withrecursionmirroringthespe{c}^{\prime }scasesplit.-[Lemur:IntegratingLargeLanguageModelsinAutomatedProgramVerification](https://arxiv.org/abs/2310.04870v5):LLM-proposedpredicatesstayassumptionsuntilasoundverifierprovestheminvariant,andanunknownresulttriggersanewassumption,sotheLLMitselfisnevertrusted.-[PML2:IntegratedProgramVerificationinML](http://arxiv.org/abs/1901.03208v1):PML2usesoneML-likesyntaxforprogramsandproofs;aprogramusedasaproofmustpasstheterminationchecker.-[LeveragingLargeLanguageModelsforAutomatedProofSynthesisinRust](https://arxiv.org/abs/2311.03739v2):GPT-4withstaticanalysiswritesVerusproofspersegment,buttheinterfacesbetweensegmentsaredeveloper-editedandnothingcheckstheymatchintent.-[GuidingEnumerativeProgramSynthesiswithLargeLanguageModels](https://arxiv.org/html/2403.03997):CombininganLLMwithanenumerativesynthesizersolved80.1-[HunyuanProver:AScalableDataSynthesisFrameworkandGuidedTreeSearchforAutomatedTheoremProving](http://arxiv.org/abs/2412.20735v3):HunyuanProverreaches68.4-[EconProver:TowardsMoreEconomicalTest-TimeScalingforAutomatedTheoremProving](https://arxiv.org/abs/2509.12603):MatchesGoedel-Prover-V2CoTonminiF2F(84.0-[ScalingNatural-LanguageGraph-BasedTestTimeComputeforAutomatedTheoremProving](http://arxiv.org/abs/2503.11657v3):Retrievingfroma60k-nodeknowledgegraphofinformalmathbeforewritingaproofgivesaccesstomorematerialthanLeanlibraries,atthecostoftranslationerrors.-[ProvingOlympiadInequalitiesbySynergizingLLMsandSymbolicReasoning](https://arxiv.org/abs/2502.13834):SymbolicscalingenumeratesinstantiationsandprunesthemwithcounterexampleswhileanLLMrewrites,andtheoutputisareadableLeanproofcheckedbyLean.-[TopoAlign:AFrameworkforAligningCodetoMathviaTopologicalDecomposition](https://arxiv.org/abs/2510.11944):Decomposesordinarycodeintodocstrings,mainfunctions,anddependenciestobuildmath-likeLeantrainingdata;reports17.77-[LearningtoDisprove:FormalCounterexampleGenerationwithLargeLanguageModels](https://doi.org/10.48550/arxiv.2603.19514):Atwo-stagemodelproposeswitnessesforfalseuniversalstatementsandprovestheminLean;proof-awaremutationbuilds575,039trainingproblemsbydroppingessentialhypothesesfromprovedtheorems.-[Goedel-Code-Prover:HierarchicalProofSearchforOpenState-of-the-ArtCodeVerification](https://doi.org/10.48550/arxiv.2603.19329):DecompositionproposalsareacceptedonlywhenLeanreconstructstheparentfromalllemmasandrandomtestingfindsnocounterexample,sinceafalselemmacantriviallyproveitsparent.-[GuidingLLM-basedLoopInvariantSynthesisviaFeedbackonLocalReasoningErrors](https://doi.org/10.1145/3806652):LORISchecksanLL{M}^{\prime }slocalreasoningbyformalizingeachstepasimplicationsforSMT,whileFrama-Cstaysthefinalauthoritysoformalizernoisecannotcauseunsoundacceptance.-[TowardsSolvingMoreChallengingIMOProblemsviaDecoupledReasoningandProving](http://arxiv.org/abs/2507.06804v1):AgeneralReasonerproposesLeansorrylemmasandaspecializedproverfiltersthem,buttheproverignoredthelemmasandreprovedfromscratch,sothedecompositiongavenolemmareuse.-[MPS-Prover:AdvancingStepwiseTheoremProvingbyMulti-PerspectiveSearchandDataCuration](https://arxiv.org/abs/2505.10962):Multi-perspectivetreesearchpluscurationthatdropsabout40-[FVEL:InteractiveFormalVerificationEnvironmentwithLargeLanguageModelsviaTheoremProving](http://arxiv.org/abs/2406.14408v2):AnLLMwritesanIsabellespeclemmathenproofstepswithfeedbackeachstep;mostfailuresarespecificationerrors,notprooferrors,soverifiersshouldreportcontractfailuresseparately.-[FIMO:AChallengeFormalDatasetforAutomatedTheoremProving](https://arxiv.org/abs/2309.04295):FIMOformalizes149IMOshortlistproblemsinLean;60.8-[TowardsGeneralLoopInvariantGeneration:ABenchmarkofProgramswithMemoryManipulation](https://arxiv.org/abs/2311.10483):LIG-MMbenchmarks312heap-manipulatingloops,andLLM-SEusessymbolicexecutiontosurfacestrongestpostconditionsasseparation-logicformulas,thoughitsalgorithmchecksinitiationandpreservationbutnotexit.-[AutomatedInvariantGenerationforSoliditySmartContracts](https://arxiv.org/abs/2401.00650):InvCon+minesSolidityinvariantcandidatesfromtransactions,keepsthoseBoogieandHoudiniverify,andlearnsimplicationssuchas(\eta 1\wedge \eta 2)\Rightarrow \tau whensingleinvariantsfail.-[EnhancingAutomatedLoopInvariantGenerationforComplexProgramswithLargeLanguageModels](https://arxiv.org/abs/2412.10483v3):ACInvgeneratesloopinvariantsbydecomposingdatastructuresstatically,thenhavinganLLMproposeandrefinecandidateinvariants.-[BeyondTheoremProving:Formulation,FrameworkandBenchmarkforFormalProblem-Solving](https://arxiv.org/abs/2505.04528):FormalProblem-SolvinghasLeancheckthatafoundanswersatisfiesthestatedconclusions;thebestreportedsolverateis23.77-[ProofAug:EfficientNeuralTheoremProvingviaFine-grainedProofStructureAnalysis](https://arxiv.org/abs/2501.18310):Askingforawholeproof,thenreplacingonlythefailingstepswithsorryandsendingthemtoautomation,keepstheproofstructurewhilepatchingthepartsthatfail.-[ProsaBuddy:AssistingMechanizedReal-TimeSchedulabilityAnalysiswithLLM-basedAgents](https://arxiv.org/abs/2610.03796):ARocqagentprovesschedulabilitylemmasthroughasubgoalDAGwhoseadmit-per-leafskeletonmustcompile,sotheleavesimplythelemma;17of24weresolved.-[LLMsandFuzzinginTandem:ANewApproachtoAutomaticallyGeneratingWeakestPreconditions](http://arxiv.org/abs/2507.05272v2):LLM-generatedweakestpreconditionsforJavaarrayprogramsarerefinedbyfuzzing,wherefailingvalidityinputsmeantooweakandsucceedingweaknessinputsmeantoostrong.-[miniCodeProps:aMinimalBenchmarkforProvingCodeProperties](http://arxiv.org/abs/2406.11915v2):miniCodePropshas201Leanspecificationswhereonlytheproofisgenerated;theLeankernelisthechecker,isolatingproofgenerationfromspecificationwriting.-[VerifyingFirst-OrderTemporalPropertiesofInfinite-StateSystemsviaTimersandRankings](https://www.semanticscholar.org/paper/d96d54d3edb7c0936a6b34848ed76a2355cf5555):Reducesfirst-orderLTLpropertiesofinfinite-statesystemstoterminationviaprophecytimersandrankings;usersstillsupplyrankingsandinvariants.-[ProofAutomationwithLargeLanguageModels](https://doi.org/10.1145/3691620.3695521):LLM-generatedCoqproofsusuallygetthehigh-levelstructurerightandfailondetails,andwrongtheoremapplicationcaused49.6-[CircularInduction](http://arxiv.org/abs/2605.24968v1):Circularinductionprovesgoalsoverorder-sortedalgebraicspecificationsbyconstructorderivativesandfrozenhypotheses;implementedintheCIRCprover.-[ReinforcedLargeLanguageModelisaformaltheoremprover](https://arxiv.org/abs/2502.08908v1):SFTthenGRPOonQwen2.5-0.5BmovesLeannext-tacticpredictionfrom36-[OProver:AUnifiedFrameworkforAgenticFormalTheoremProving](https://www.semanticscholar.org/paper/f59279a01f96acd7003ef35f8652ca462c1698c7):RawcompilerfeedbackisthedominantcomponentofaLeanrepairagent,sinceremovingitdroppedthe32Bmode{l}^{\prime }sProofNetpassratefrom33.2-[ShannonProver:TowardsAutomatingFormalCryptographicProofs](https://doi.org/10.48550/arxiv.2607.02847):ShannonProve{r}^{\prime }sagentautomatesEasyCryptproofsofMEE-CBCandChaCha20-Poly1305in2to5hoursat$233.65 API cost, but a human still supplies the spec and main theorem.
• Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report): Claude Code wrote the Rocq proof of CertiCoq’s ANF semantic preservation, and its divergence-technique counterexample forced a switch to a step-indexed logical relation.
• Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs: Pistis maps natural-language proof steps into Lean and OrderDecompose fills gaps while keeping structure; five faithfulness conditions are defined.
• Automatic Function Annotations for Hoare Logic: Isabelle function annotations store intermediate Hoare assertions so later properties on the same seL4 function reuse them instead of reproving them.
• Lazy Annotation for Program Testing and Verification: Lazy annotation learns interpolant labels from symbolic-execution failures, like DPLL conflict clauses, and it has no termination guarantee since the problem is undecidable.
• MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving: MechMath’s sorrifier replaces only the smallest enclosing failing block with sorry, one innermost error at a time, and then proves each hole as a fresh lemma.
• Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings: A denoising transformer trained on constructive Lean proofs separates classical proofs by k-NN AUC 0.847 at depth 2, falling to 0.507 at depth 9+.
• A Kernel-Checked Exclusion Certificate for Erdős Problem 647: A Lean 4 proof shows no n in (24, 10^9] satisfies the Erdos 647 condition, using only standard axioms and no native decide.
• Magnushammer: A Transformer-Based Approach to Premise Selection: Magnushammer uses two-stage neural premise selection, select then rerank with hard negatives from the first stage, feeding a bounded Isabelle proof search over top-k premise prefixes.
• MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification: miniF2F in Dafny has 488 lemmas, and 128 of 160 axiomatized lemmas are proved, so the trusted surface shrinks, with calc chains splitting arithmetic into solver-checked steps.
• Laurel: Unblocking Automated Verification with Large Language Models: An LLM filled one missing assertion at a placeholder chosen from verifier error locations, solving 82 of 145 industrial Dafny lemma tasks (56.6%) in 10 attempts.
• Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints: Model-guided lemma synthesis for FO+lfp uses three counterexample classes to guide synthesis, but it is complete only for the paper’s fragment.
• When Does Structured Knowledge Help Neural Theorem Proving?: A knowledge graph helps only some provers: Lean specialization adds 33-38 points, while no augmentation mode adds more than 3 points in aggregate.
• Towards Machine Learning Induction: MeLoId, a learned recommender, suggests promising induction applications for Isabelle before a full proof search completes.
• PaMpeR: Proof Method Recommendation System for Isabelle/HOL: A learned recommender over 108 hand-written proof-state features suggests Isabelle proof methods from human proofs, and Isabelle still checks every suggestion.
• Genetic Algorithm for Program Synthesis: Evolving SuSLik’s proof-search rule weights improves synthesis on validation sets, without evolving the programs themselves.
• Invariant Synthesis for Incomplete Verification Engines: When the verifier is sound but incomplete, mine the decidable countermodel for non-provability constraints rather than a counterexample, and use them to learn invariants that avoid those failures.
• Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale: A local model proposes loop invariant candidates only for the residue that symbolic checks miss, and ESBMC as a three-valued oracle accepts only what it proves.
• Next Steps in LLM-Supported Java Verification: An LLM fills one loop invariant or subcontract in a human-written Java JML spec checked by KeY, and key feedback does not significantly beat restarting from scratch.
• Deep Generation of Coq Lemma Names Using Elaborated Terms: Roosterize generates Coq lemma names from statements and elaborated kernel terms; kernel trees carry more information than syntax trees.
• Roosterize: Suggesting Lemma Names for Coq Verification Projects Using Deep Learning: Roosterize suggests Coq lemma names with a neural model trained on existing code; a developer aid, not a checker.
• Canonical for Automated Theorem Proving in Lean: A type-inhabitation solver returns Lean proof terms by refinement search from a goal hole; the cited arXiv id belongs to Pantograph, so the link does not identify this paper.
• What are the Right Symmetries for Formal Theorem Proving?: Semantically equivalent rewrites of a Lean statement changed DeepSeek-Prover-V2 success over 64 attempts, such as 62 versus 13 under induction reformulation, so prover success is not invariant.
• Direct Optimization of Generators for Search in Automated Theorem Proving: Compute-aligned training weights tactic cross-entropy by the search’s success probability, so one adapter serves pass@N, BFS, and DFS, while search-specific weights must be derived per scheduler.
• P^3: Joint Program-and-Proof Planning for Verified Code Generation: Commit to a joint plan of decomposition, lemmas, and obligations before writing code; the transfer to SMT systems like Verus is plausible but not empirically shown.
• Graph Representations for Higher-Order Logic and Theorem Proving: A 12-hop GNN over higher-order logic terms with subexpression sharing closed 49.95% of HOL Light validation proofs, versus 37.98% for bag-of-words.
• Formally Validating a Practical Verification Condition Generator: Certifies each Boogie run by proving in Isabelle that its VC matches the CFG; passes before the CFG-to-DAG phase are not certified.
• QbC: Quantum Correctness by Construction: Constructs quantum programs from Hoare-style specifications by refining typed holes, so each step stays correct by construction.
• Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?: An LLM proposes auxiliary lemmas for an inductive strengthening of a hardware safety property, and a checker decides each candidate on 109 design pairs, trying individually inductive candidates first.
• LeanPlan: Optimal Planning with LLM-Generated Heuristics and Admissibility Proofs: LeanPlan has a coding agent write a planning heuristic and a Lean admissibility proof about the exact code A* runs, rejecting sorry, native_decide, and new axioms.
• Machine-Learned Premise Selection for Lean: Premise selection inside Lean: names and bigrams from hypotheses and conclusion with k-NN give Cover 0.29, while random forests and trigrams overfit.
• ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification: The LLM proposes contracts and loop invariants, ESBMC checks them assume-guarantee, and top-down derivation asks only for what the top assertion needs.
• RLMEval: Evaluating Research-Level Neural Theorem Proving: RLMEval has 613 blueprint theorems from six Lean projects; the best pass@128 is 10.3%, and main theorems average 16.6 proof lines versus 6.6 for auxiliary lemmas, so select blueprint theorems.
• CounterExample Guided Neural Synthesis: A neural network proposes bit-vector loop invariants from I/O examples and only the final SMT check gives soundness, and counterexample guidance nearly doubles the benchmarks solved.
• Generative Language Modeling for Automated Theorem Proving: A decoder-only transformer generating Metamath proof steps was the first deep-learning system to get proofs accepted into a formal library, with the checker deciding validity.
• Formal Mathematics Statement Curriculum Learning: Expert iteration on Lean, interleaving search and training, beats search-only at equal compute, reaching 36.6% on miniF2F test at pass@64 and learning from statements without ground-truth proofs.
• Premise Selection for Mathematics by Corpus Analysis and Kernel Methods: Exact minimal dependencies followed by learned ranking raises Mizar ATP solves from 548 to 795 of 2,078 problems (+45.1%), and dependency pruning is a model for trimming Verus context.
• Can Large Language Models Verify System Software? A Case Study Using FSCQ as a Benchmark: Best-first tactic search with off-the-shelf LLMs proves about 38% of sampled FSCQ theorems; human proofs under 64 tokens are most solvable, and long proofs are not solved.
• Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving: Rewarding a Lean tactic by how it changes the number of open goals, with no rollouts, trains a tactic generator to prefer goal-opening steps, though it fails on theorems needing more than one step.
• Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification: Retrieving similar in-project proofs before each tactic reached 32% of Coq theorems versus 24.8% for Tactician, and retrieval supplies most of the gain.
• Ranking LLM-Generated Loop Invariants for Program Verification: A learned ranker reorders LLM-generated loop invariants so correct ones reach the verifier earlier, cutting verifier calls.
• Decidability and Synthesis of Abstract Inductive Invariants: The strongest invariant in an abstract domain is the least fixpoint of the abstract transformer, under best-approximation assumptions.
• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification: A proof-checker reward trains Isabelle proof generation, but it measures only acceptance, so a policy formalization that ignores its action argument still proves.
• Completeness Thresholds for Memory Safety of Array Traversing Programs: Early Technical Report: Completeness thresholds reduce unbounded memory-safety proofs for array-traversing loops to bounded ones; the report is ongoing work without a finished implementation.
• DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition: DeepSeek-Prover-V2 has DeepSeek-V3 write Lean sketches with sorry-haves, and a 7B prover solves subgoals recursively; minif2f reaches 82.4% at 32 samples, with no ablation separating decomposition from scale.
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing: Feeding Lean only a scalar reward, never error text, into MCTS over natural-language proof plans reached 84.2% on MiniF2F versus 82.4% for whole-proof sampling.
• Quantitative Comparison of Credible Compilation and Verification In Coding Agent Compiler Development: Verifying each agent-written compiler optimization took 7.6 to 19.9 times more active time than a checker-certificate approach, falling to 3.5 to 4.3 when checker updates are counted.
• Model Checking C Programs with Loops via k-Induction and Invariants: k-induction plus automatically inferred affine invariants verifies C loops, bounded and unbounded, via base, forward-condition, and inductive steps.
• PRover: Proof Generation for Interpretable Reasoning over Rules: PRover generates a proof graph for rule-based questions, using an ILP to enforce global consistency.
• Generating correctness proofs with neural networks: Proverbot9001 predicts tactic plus argument, where argument selection is the main lever and tactic prediction mostly prunes search, and the Coq kernel checks every script so the model is untrusted.
• Regression verification of unbalanced recursive functions with multiple calls (long version): RVT proves partial equivalence of unbalanced recursive functions by abstracting proven pairs and recursive calls with uninterpreted functions.
• Pipeline for Verifying LLM-Generated Mathematical Solutions: Checks LLM math solutions in Lean through Solver, Translator, and Prover LLM roles; prompts yield lemma chains that let models of 8B or less work.
• Schwarz: Solver-Aware Agentic Program Verification: When a global proof fails, the agent proposes bridge lemmas for a local SMT obligation, checks each one in sequence, then lifts the working lemma back to source.
• VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models: VeCoGen asks an LLM for C, checks it with Frama-C WP against ACSL, and repairs one candidate with verifier feedback; solves 13 of 15 Codeforces problems.
• PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs: PROVE-RT turns real-time schedulability papers into Rocq skeletons first, then fills proofs block by block, rejecting changed theorems, new axioms, and leftover Admitted, since typing a statement is easier than finding a strategy.
• StepFun-Prover Preview: Let’s Think and Verify Step by Step: StepFun-Prover interleaves reasoning, Lean sketches, and REPL feedback, rewarded only by the final proof passing; outcome-only reward limits reward hacking.
• REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning: REAL-Prover is a stepwise Lean prover with premise retrieval trained by hard-negative InfoNCE; its claims are benchmark pass rates, not theorems, and it reports no autoformalization error rate.
• Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4: Snapshotting elaborated Lean proof states avoids re-elaborating per branch, giving 5.6 to 50x overall speedup with identical proof results.
• CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization: Ordering proof states by remaining proof distance and training preference optimization in that curriculum lifted a Lean prover’s MiniF2F pass@1 to 38.5%, though the result is empirical only.
• Code2Inv: A Deep Learning Framework for Program Verification: A neural policy samples invariant candidates from a grammar and the checker returns counterexamples; the 0/1 reward is too sparse, so the paper uses accumulated counterexamples.
• Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean: Lean Copilot’s tactic suggestions are checked by simulating each on the current goal and dropping erroring candidates, so only verified suggestions reach the user.
• Total Haskell is Reasonable Coq: hs-to-coq shallow-embeds total Haskell into Coq; verified Bag functions with proofs of at most eight lines.
• Provably Complete Generalized Planning with LLMs: An LLM wrote Lean generalized-planning programs with kernel-checked proofs that every valid input yields a plan, though the guarantee holds only as far as the supplied validity constraints.
• Reliable Proof Generation with LLMs via Analogical Retrieval and Symbolic Verification: A Case Study in Euclidean Geometry: Retrieving analogous solved geometry proofs by normalized construction and condition similarity, then giving a symbolic verifier’s first error as feedback, yields verified proofs on FormalGeo-7k.
• Formally Solving Answer-Construction Problems in Lean: Lean accepts answer-construction proofs with circular witnesses, such as sInf of a property where a numeral is required, so a compiling proof does not enforce the answer format.
• On Reasoning-Centric LLM-based Automated Theorem Proving: ReCent-Prover asks the LLM for reflection only after branching or irreversible tactics, catching cases like induction without generalization; it reaches 138/200 on CoqStoq with o4-mini, evidence is Rocq only.
• Statistical Proof as a Window into Human-AI Collaboration: Practical Insights and a Community Agenda: Across four paired case studies on research proofs, current general LLMs execute a suitable proof strategy better than they identify one.
• Synthesizing Proofs Using Proof Sharding and Exploration: Proof sharding splits a Dafny proof into per-case lemmas, queries the prover per shard, and iterates only on failing shards; it solves 86/103 single-hole tasks but only 8/49 from scratch.
• Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving: Larus turns incomplete geometry conjectures and sketches into checkable proofs by encoding bounded proof search as constraints for SAT, SMT, or CSP.
• Show Me The Money: An Exercise in Proof-Driven Software Understanding: An LLM with PVS and SeaHorn retrospectively verified a 260-line model of Stellar’s order-book algorithm, proving three properties and finding a counterexample to a fourth.
• ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language: Iterative one-step generation yields proofs that reflect actual model decisions rather than post-hoc rationalizations.
• Completeness of Cyclic Proofs for Symbolic Heaps: Cyclic proof system CSLIDω for symbolic heaps with general inductive definitions is sound, complete, and has a terminating decision procedure.
• EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty: EvolProver augments Lean problems via domain transfer, difficulty variants, and AST equivalence rewrites; a 7B prover reaches 69.80% on minif2f-test versus 52.0% for the base.
• Towards Large Language Model Aided Program Refinement: Constraining an LLM to choose refinement-calculus laws, with a prover checking each step’s proviso and bounded retries, keeps the guarantee relative to the initial spec and the prover.
• Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4: A fine-tuned 7B Isabelle prover proves 341/660 seL4 theorems (51.67%) in 256 attempts; context is an oracle that gets exactly the definitions and lemmas the human proof used.
• PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition: PutnamBench has 1,692 hand-built formalizations of 640 Putnam problems in Lean 4, Isabelle, and Coq.
• Formal Premise Selection With Language Models: Two-stage Isabelle premise selection freezes the retriever and gives the generator the proof state plus top-k premises, and k=4 with contrastive loss worked best.
• Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs: Draft, Sketch, Prove turns an informal proof into a formal sketch with holes that Sledgehammer and tactics fill, and the baseline numbers show the hole-filler alone reaches 20.9%.
• First Neural Conjecturing Datasets and Experiments: Mizar datasets for neural conjecturing separate generation, syntactic filtering, countermodel checks, and proof search.
• VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus: VeriStruct synthesizes Verus View functions, invariants, and proofs per module with planner-chosen components, solving 10 of 11 modules and 128 of 129 functions given comprehensive unit tests.
• VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search: VerMCTS prunes any partial program the verifier rejects, adds a child only on a verified +1, and uses no learned value, since the exact verifier is cheap next to LLM calls.
• MiniF2F in Rocq: Automatic Translation Between Proof Assistants — A Case Study: 478 of 488 MiniF2F statements were translated to Rocq, with syntax checks and then human semantic review; proofs are excluded.
• Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method: DS-Prover splits multi-premise rewrite tactics into single-premise ones for data augmentation and sizes tactic expansion by remaining time.
• LEGO-Prover: Neural Theorem Proving with Growing Libraries: LEGO-Prover grows a library of verified lemma skills that retrieval reuses, raising miniF2F test from 45.5 to 50.0, and failed lemma statements go to a request store.
• Proving Theorems Recursively: Poetry proves level by level, defers subgoals with sorry, then recurses on each deferred subgoal; sketches come from complete proofs, and HALF-PROVED nodes wait for their children.
• GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving: Co-training a Lean prover with a statement fuser that merges easy statements into harder ones, with a reward that penalizes statement modification, gives an implicit curriculum.
• MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving: MA-LoT pairs a prover that writes whole Lean proofs with a corrector that repairs from exact Lean errors; Godel-Prover at 16+2x8 reaches 61.07% on miniF2F at 33% more tokens.
• From Scientific Texts to Verifiable Code: Automating the Process with Transformers: Prometheus refines textual proofs into Dafny by building a skeleton then low-level proofs, with preliminary evaluation only and no rule for assertion selection.
• Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation: Diffusion-Proof trains two 7B block-diffusion Lean models, a prover and a corrector that repairs one failed subgoal, reaching 50.00% on MiniF2F-Test versus 43.85% for a same-data autoregressive baseline.
• Translating Informal Proofs into Formal Proofs Using a Chain of States: Translating informal proofs to Lean works better when a model writes intermediate formal states aligned with the argument and a tactic generator solves each adjacent transition.
• ProofCompass: Enhancing Specialized Provers with LLM Guidance: A general LLM guides a specialized prover with no training, and lemmas mined from failed DSP attempts beat LLM-written lemmas because DSP can use them.
• TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning: TacticZero trains a HOL4 prover from theorem statements only, using a fringe MDP with softmax sampling over fringes so that older fringes keep nonzero probability and backtracking is learned.
• InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search: InternLM2.5-StepProver’s critic ranks proof states from preference pairs, lifting miniF2F-test from 59.4% (best-first) to 65.6% (critic-guided) and 65.9% combined.
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation: Mutating Mathlib theorems by running rewrites in Lean yields new valid theorems whose proofs come from reversing the mutation, though Lean checks only correctness, not usefulness.
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs: Uses the Dafny spec as oracle for arithmetic-bug localization by encoding each Hoare entailment as a lemma; it assumes a single bug and a correct spec, and places the buggy line in 89.7% of programs.
• InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs: A loop-constraint graph exposes inter-loop dependencies, so invariant synthesis for nested and sequential loops gets neighbor context, and repair propagates along the graph.
• ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction: ALPS benchmarks valid creativity: solutions must be original and machine-certified.
• DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search: DeepSeek-Prover-V1.5 combines SFT with natural-language plans and tactic states, RL from proof-assistant feedback, and truncate-and-resume tree search, reaching 60.2% on miniF2F-test.
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data: Dropping autoformalized statements whose hypotheses are inconsistent, detected by proving False after replacing the conclusion, raised miniF2F pass@128 from 38.1% to 42.6% at equal data.
• BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving: BFS-Prover uses length-normalized best-first Lean search with per-tactic verification, reaching 70.83% ± 0.89% on miniF2F-test at a fixed budget, though budgets are not matched in cost.
• Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers: BFS-Prover-V2 reaches 95.08% on miniF2F-test with a planner and 86.1% without, using multi-turn off-policy RL with a +1 reward only on successful paths.
• Automated Discovery of Tactic Libraries for Interactive Theorem Proving: TacMiner mines reusable Rocq tactics from proof-dependence graphs, and a collapsible refactoring is valid only when no unselected node sits between selected ones.
• SmartVerif: Push the Limit of Automation Capability of Verifying Security Protocols by Dynamic Strategies: SmartVerif replaces Tamarin’s static proof search with a dynamic strategy, targeting protocols with global state or unbounded sessions.
• A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation: LeanComb (727 theorems) is a benchmark; ATG4CI pairs LM tactic suggestions with RL tree search and generated 260,466 new theorems over two iterations.
• Automated Formal Proofs of Combinatorial Identities via Wilf–Zeilberger Guidance and LLMs: WZ-LLM decomposes combinatorial identities via Wilf-Zeilberger certificates into Lean sketches, solving 34 of 100 LCI-Test identities end-to-end, with the Lean kernel as the sole correctness criterion.
• Formal Verification of Parameterized Systems based on Induction: wiseParaverifier finds small-instance auxiliary invariants, then generalizes them into parameterized inductive invariants checked by Ivy.
• A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL: A minimal 10-operation proof language mirroring informal outlines, with leaves delegated to Sledgehammer, gives neural provers a smaller search space than raw tactics, and soundness depends on backends.
• Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement Learning: RULES judges a lemma in two ordered sections, precondition then conclusion, and section-aware GRPO penalizes only the wrong section, preventing models from using a conclusion whose assumptions fail.
• Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving: Segment-level supervision trains on tactic sequences bounded by open-goal count changes; goal-aware rollouts raise BFS-Prover-V2-7B from 68.77% to 70.74% on miniF2F.
• Symbolic Search Is Not Exhausted: Persistent Proof-Space Exploration in Lean4: ViaLean keeps a persistent proof atlas of Lean states and closes goals with bounded verified solvers instead of discarding explored branches.
• Learning to Prove Theorems via Interacting with Proof Assistants: CoqGym has 70,856 human Coq proofs from 123 projects, split by project so no test proof comes from a training project, with an environment where agents issue tactics and see new goals.
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models: LeanDojo’s patched extraction gives premise data and an anti-memorization split matters, since lean-gym misjudged 21.1% of correct proofs.
• A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems: Adds Lean 4 proofs for 17 IMO problems, 14 of them missing miniF2F test proofs; the paper’s line and lemma counts are not fully consistent.
• LemmaHead: RAG Assisted Proof Generation Using Large Language Models: RAG with textbook chunks plus iterative proof augmentation reached 40.0% on MiniF2F validation, but basic RAG without good queries was worse than no retrieval.
• CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification: Parameterized Chisel hardware was proved correct once for all legal parameters in Lean, with an agentic loop that reuses Lean-checked lemmas, rather than model-checking each instance.
• Large Language Model for OWL Proofs: LLMs construct faithful OWL proofs by separating axiom extraction, simplification and explanation, with completeness detection.
• Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks: G-CLN learns nonlinear loop invariants from traces and Z3 checks each candidate; fitting all traces is not evidence of inductiveness.
• ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving: ProofEvolve keeps verified partial proof DAGs from failed root attempts, with a closure-based fitness where extending a DAG never lowers the score, and authors report zero false positives on over 400 re-verified solutions.
• Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs: LeanNavigator generates 4.7 million Lean theorem-proof pairs by exploring proof-state graphs, with Lean validating each step.
• Let the Library Speak: Self-Advertised Method Selection for Formal Proving: Method contracts with selection and execution sides let a selector match by applicability rather than similarity; proofs check hole-free terms but not whether the method fits the user intent.
• Efficient verification of imperative programs using auto2: Auto2 uses saturation-based proof search with reusable tables for rewrites, properties, and side conditions, but Verus has no saturation API to copy.
• Getting More out of Large Language Models for Proofs: GPT-4 Coq proof failures were 34.3% hallucinated names and 20.7% missing dependencies, but the six recommendations in this two-page proposal are untested.
• Selene: Pioneering Automated Proof in Software Verification: Selene builds a seL4 proof-generation benchmark by isolating each lemma in its own Isabelle session, reusing verified dependencies.
• Automated Strategy Invention for Confluence of Term Rewrite Systems: AI-invented strategies for the CSI confluence prover use a restricted search space to avoid unsound strategies.
• Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers: Pattern-guided tactic search ranks tactics that match mined transitions first, then falls back to model probability, within a 300-application budget.
• DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent: DreamProver grows a persistent Lean lemma library through wake-sleep cycles, keeping generalized lemmas only when they resemble a theorem cluster, and reports a 61% average gain over Hilbert.
• PhysProver: Advancing Automatic Theorem Proving for Physics: PhysProver runs GRPO on Lean physics with a verifier reward; conjecture synthesis gives 2,608 kept proofs (8.9% yield) and +2.4 points pass@16 on the physics test, with uneven gains.
• VerusSeek: Retrieval-Augmented LLM-Based Proof Synthesis for Rust Programs: VerusSeek retrieves Verus constructs (invariants, lemmas, proof blocks) by verifier error type with bounded context, and every candidate is checked by Verus.
• Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving: Subgoal-based demonstrations split proofs into steps the LLM can reconstruct and Isabelle accepts, while diffusion-based example selection under a context budget fits only 4.79 examples on average.
• SubgoalXL: Subgoal-based Expert Learning for Theorem Proving: Training a proof generator on subgoal annotations that match formal intermediate Isabelle goals, with reward-weighted expert iteration, produced 38k verified proofs over three iterations.
• Lyra: Orchestrating Dual Correction in Automated Theorem Proving: Adding tool correction, which tries a fixed list of automation tactics, and conjecture correction to draft-sketch-prove improves Isabelle miniF2F proofs, and every proof is still Isabelle-checked.
• Solving Formal Math Problems by Decomposition and Iterative Reflection: Delta Prover is a training-free Lean agent on Gemini 2.5 Pro that reaches 95.9% on miniF2F-test, and iterative repair beats best-of-n at the same budget.
• Towards Language Model Guided TLA+ Proof Automation: An LLM proposes decompositions of TLA+ inductive proofs, and TLAPS checks that each child implies its parent, lifting protocol proofs to 38.5-50.0% versus 38.5% for the SAPG baseline.
• Retrieval-Augmented TLAPS Proof Generation with Large Language Models: Splits TLAPS obligations into simpler sub-obligations, which LLMs prove more reliably.
• Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training: Spark-Prover-X1-7B reaches 37.0% average pass@32 across eight prover benchmarks and solves 27 PutnamBench problems through three training stages.
• SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner: SCOPE splits proof work: a 135M planner picks operators, a symbolic engine computes exactly, and a compiler emits Lean tactics that Lean checks.
• GenesisGeo: Technical Report: GenesisGeo generates one million synthetic geometry problems needing auxiliary constructions, with DDAR proof traces, and trains a small multimodal prover on them.
• Premise Selection for a Lean Hammer: Lean Hammer’s neural premise selector reaches a 30.1% full proof rate on Mathlib-test, below the 41.0% from ground-truth premises, so retrieval is the incomplete step.
• From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates: An LLM proposes SOS structure, symbolic computation repairs it exactly, and Lean checks it, with pass rates falling from 44.1% at three variables to 36.7% at five.