arXiv CSopen access

Automating Formal Verification with Agent-Guided Tree Search

Automating Formal Verification with Agent-Guided Tree Search by

arXiv:2605.27485v1 [cs.LO] 26 May 2026

Leo Yao S.B. in Physics and Electrical Engineering and Computer Science, Massachusetts Institute of Technology, 2025. Submitted to the Department of Electrical Engineering and Computer Science in partial fulfillment of the requirements for the degree of MASTER OF ENGINEERING IN ELECTRICAL ENGINEERING AND COMPUTER SCIENCE at the MASSACHUSETTS INSTITUTE OF TECHNOLOGY May 2026

© 2026 Leo Yao. All rights reserved. The author hereby grants to MIT a nonexclusive, worldwide, irrevocable, royalty-free license to exercise any and all rights under copyright, including to reproduce, preserve, distribute and publicly display copies of the thesis, or release the thesis under an open-access license. Authored by:

Leo Yao Department of Electrical Engineering and Computer Science May 22, 2026

Certified by:

Max Tegmark Professor of Physics, Thesis Supervisor

Accepted by:

Katrina LaCurts Chair, Master of Engineering Thesis Committee

2

Automating Formal Verification with Agent-Guided Tree Search by Leo Yao Submitted to the Department of Electrical Engineering and Computer Science on May 22, 2026 in partial fulfillment of the requirements for the degree of MASTER OF ENGINEERING IN ELECTRICAL ENGINEERING AND COMPUTER SCIENCE

ABSTRACT Formal verification offers a path to provably correct software, but writing verified code remains expensive enough that the technique is rarely used in production. Recent large language models can accelerate this work, and recent benchmarks measure their ability to translate specifications into code and machine-checked proofs of correctness. This thesis evaluates the state of such LLM-driven verified-code generation (“vericoding”) in Lean and develops search-based methods for improving verification performance. We first reproduce a subset of the vericoding-benchmark Lean leaderboard on a current cross-vendor model pool, finding that non-reasoning performance remains roughly steady on US closed-source models while open-weight models have slightly improved. We update the iterative methodology of vericoding-benchmark with an agentic loop equipped with mathlib search, finding that model performance greatly improves and scales with agent budget. GPT-5.4 nearly saturates the benchmark at 95.0% on 423 specs with K = 50 LLM calls. We then design two agentdirected tree-search formulations: a state-based orchestrator that branches on partial-proof states, and a context-based orchestrator that branches on full subagent contexts. Compared against the agent baseline, the context-based design solves a wider range of intermediatedifficulty specs at lower token cost, while the agent baseline retains an advantage on the hardest specs, where uninterrupted iteration matters most. We conclude that search structure has selective advantages over a strong agent baseline, and that more challenging benchmarks drawn from modern code are important to measure and drive further progress in automated formal verification. Code available upon request by contacting the author at [email protected]. Thesis supervisor: Max Tegmark Title: Professor of Physics

3

4

Acknowledgments I would like to thank my research advisor, Professor Max Tegmark, for four years of guidance and support. Thank you for introducing me to numerous areas of study across physics, machine learning, and formal verification. It has been an honor to be part of your group for the majority of my time at MIT. Thank you to research group members David Baek, Max Tan, and Ionel-Emilian Chiosa for insightful discussions, contributions to research direction, and technical assistance; collaborators at the Beneficial AI Foundation for their mentorship and for building the benchmark this thesis stands on; and staff in the MIT Department of Physics and MIT EECS Department for their administrative assistance. I am grateful to my undergraduate research supervisor, Dr. Ziming Liu, for multiple years of dedicated mentorship and helping shape me as a researcher. I am also grateful to Professor Soonwon Choi for thoughtful guidance as my undergraduate academic advisor and Professor Michael Sipser for taking me on as a teaching assistant. Finally, I would like to thank my family and friends for their continued dedication, understanding, and support.

5

6

Contents List of Figures List of Tables

9 11

1 Introduction

13

2 Literature Review 2.1 Current Language Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Formal Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.3 Machine Learning Methods for Lean . . . . . . . . . . . . . . . . . . . . . . 2.4 Benchmarks for LLM-Driven Formal Verification . . . . . . . . . . . . . . . .

17 17 19 20 22

3 Updated Baselines for Lean Verification 3.1 Vericoding Benchmark Targeted Reproduction . . . . . . . . . . . . . . . . . 3.1.1 Benchmark Subset Selection . . . . . . . . . . . . . . . . . . . . . . . 3.1.2 Harness Setup . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.1.3 Model Selection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.1.4 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.1.5 Chain-of-Thought Emission . . . . . . . . . . . . . . . . . . . . . . . 3.2 Agentic Loop Baseline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2.2 Experimental Setup . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2.3 Initial Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2.4 Agent Tool Call Behavior . . . . . . . . . . . . . . . . . . . . . . . . 3.2.5 Longer-Context Evaluations . . . . . . . . . . . . . . . . . . . . . . .

25 25 25 26 27 29 30 32 32 34 34 36 39

4 Search Methods for Lean Verification 4.1 Searching Over Partial Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . 4.1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.1.2 Experimental Setup . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.1.3 Initial Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.1.4 Subagent Search Behavior . . . . . . . . . . . . . . . . . . . . . . . . 4.1.5 Final Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2 Searching Over Agent Contexts . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.2 Experimental Setup . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.3 Initial Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

43 43 43 44 46 46 50 54 54 55 55

7

4.2.4 4.2.5

Empty-Context Resume Behavior . . . . . . . . . . . . . . . . . . . . Final Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

56 59

5 Conclusion

63

References

67

8

List of Figures 3.1 3.2 3.3 3.4

Claude Opus 4.7 think-block excerpt on a bignum task. . . . . . . . . . . . . K = 10 agent solve rate vs. unique tokens, full set and per subset. . . . . . . Per-turn tool-call rates across the first ten agent turns. . . . . . . . . . . . . K = 50 agent solve rate vs. unique tokens, full set and per subset. . . . . . .

4.1 4.2

State-based orchestrator solve rate vs. unique tokens, full set and per subset. 47 State-based + resume orchestrator solve rate vs. unique tokens, full set and per subset. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Context-based orchestrator solve rate vs. unique tokens, full set and per subset. 57 Final orchestrator solve rate vs. unique tokens, full set and per subset. . . . . 61

4.3 4.4

9

28 37 38 41

10

List of Tables 3.1 Cross-model Vericoder reproduction results on the Lean 423-spec set. . . . . 3.2 Reproduction vs. Vericoding paper baseline, comparing model generations. . 3.3 Proportion of output emitted as thinking, for each model. . . . . . . . . . . . 3.4 Multi-block emission rates, by model. . . . . . . . . . . . . . . . . . . . . . . 3.5 Per-subset solve rates of the agent baseline at K = 10. . . . . . . . . . . . . 3.6 Per-model tool-call behavior across ten agent turns. . . . . . . . . . . . . . . 3.7 Agent pass rate at varying K, by subset. . . . . . . . . . . . . . . . . . . . . 3.8 gpt-5.4 cumulative solves on bignum every five LLM calls. . . . . . . . . . . .

30 31 32 33 35 39 42 42

4.1 State-based orchestrator pass rate at varying K, by subset. . . . . . . . . . . 4.2 Parent tool-call distribution for state-based orchestrator. . . . . . . . . . . . 4.3 State-based orchestrator subagent tool-call totals per variation. . . . . . . . . 4.4 State-based + resume orchestrator pass rate at varying K, by subset. . . . . 4.5 Parent tool-call distribution for state-based + resume orchestrator. . . . . . 4.6 State-based + resume orchestrator subagent tool-call totals per variation. . . 4.7 Context-based orchestrator pass rate at varying K, by subset. . . . . . . . . 4.8 Context-based orchestrator round-2 dispatch vs. resume subagent behavior. . 4.9 Final orchestrator pass rate at varying K, by subset. . . . . . . . . . . . . . 4.10 Final orchestrator round-2 dispatch vs. resume subagent behavior. . . . . . .

48 48 50 51 53 53 56 58 60 62

11

12

Chapter 1 Introduction With the development and growing application of artificial intelligence (AI) in recent years, the question of safety has grown from a niche research area into a mainstream concern [1]. A key technical question in AI safety is trustworthiness: whether AI systems are faithful to human goals, and reliably act in support of those goals when exposed to different inputs and environments. This question becomes more important as models become more powerful and are deployed with increasing autonomy: unlike the purely chat-interface models of a few years ago, present-day models are run as agents which can write code, interact with the web, and execute actions on computer systems. AI agents have been able to complete longer and more complicated tasks, with a measure of completed task length doubling every seven months [2–4]. One possible tail-risk scenario is that of recursive self-improvement, in which improvements feed back into AI research itself. In such a regime, research progress and capabilities accelerate exponentially, possibly outpacing the techniques and safeguards used to keep up with and control them [5]. Even today, techniques used to align models do not fully mitigate the risks of unintended behavior and misuse. Agents have been observed taking destructive actions within compute environments or inadvertently publicizing sensitive information, and current models can supply guidance on biological or chemical weapons or generate harmful content [6,7].

13

Coding in particular has been broadly transformed by recent developments in AI capabilities. Current generation large language models (LLMs) excel at generating large quantities of code from oftentimes vague natural language descriptions, a practice commonly referred to as vibe coding [8]. While such code often looks correct at first glance, it may contain bugs or security vulnerabilities that are not immediately apparent [9,10]. The conventional approach is to use collections of tests, from individual unit tests of functions to larger end-to-end tests of behavior, to attempt to check correctness. Modern coding agents are able to autonomously write and run tests to try to detect and correct errors. However, AI-assisted software development is still marked by frequent hallucinations and deviations from the expected task, leading to behavior such as avoiding or changing the tests, hardcoding success cases, or even pretending that tests have passed when they have not. An alternative is formal verification: a method to prove the correctness of mathematical theorems or computer programs, written in formal languages that can be checked by computers. These methods were first developed for mathematics, to allow for computer-assisted validation of long or intricate proofs. The most active language ecosystem is Lean 4, along with the community-maintained library mathlib, which has formalized substantial portions of undergraduate- and graduate-level mathematics [11]. Human-formalized collections of questions drawn from competition mathematics, such as miniF2F [12], PutnamBench [13], and various IMO (International Mathematics Olympiad) formalizations, serve as benchmarks for automated methods. AI capabilities have rapidly progressed in the last few years, with systems such as DeepMind’s AlphaProof reaching human-level IMO performance [14]. Compared to test-based approaches, formal verification has the advantage of guaranteeing that an implementation adheres to its full specification. This guarantee matters more now that frontier models can accelerate the process of finding and exploiting vulnerabilities [6,7]—the best way to avoid exploits is to prove them impossible. Verified code is not a hypothetical: provably correct software ships today in domains from cryptography to kernels to compilers [15– 17]. However, each of these projects took significant human expert effort, which is why formal

14

verification remains rare in production systems. Recent work on LLM-driven formal verification spans reinforcement learning [18], subgoal decomposition [19], and tree search over proof states [14,20], alongside the tooling and library integrations that make these methods usable. However, most research focuses on mathematical benchmarks, while verified coding is comparatively less studied. This thesis studies the application of LLM-driven methods to formal verification problems in code, devising and testing various agent-driven search approaches to construct proofs. The rest of the thesis proceeds as follows. In Chapter 2, we review the literature surrounding current language models, formal verification, and machine learning methods for Lean. In Chapter 3, we provide updated baselines for Lean verification using both the original iterative prompting approach and an agent-based framework. In Chapter 4, we introduce two agent-guided search methods and evaluate them in comparison with our baselines. We conclude in Chapter 5 with directions for future work.

15

16

Chapter 2 Literature Review 2.1

Current Language Models

Modern LLMs are built on the transformer architecture, which succeeds previous recurrent architectures with a self-attention mechanism that can be parallelized in training [21]. Current frontier models are decoder-only autoregressive transformers [22], which generate text one token at a time, conditioning each new token on all preceding context. These models are first pretrained on massive corpora of unstructured text drawn from much of the public internet, in which the model learns to predict the next token from previous ones. It has been found empirically that these models obey scaling laws: loss decreases as a power-law in compute, dataset size, and parameter count [23,24]. This regularity has driven rapid increases in model size and training compute in recent years. Without further training, pretrained LLMs produce raw continuations of input rather than answering questions or following user instructions. To adapt these models into useful assistants, an additional post-training step is required. The standard approach is reinforcement learning from human feedback (RLHF), in which the model is fine-tuned against a reward model trained on human preferences [25,26]. Variants such as Constitutional AI reduce reliance on human labels by combining model self-critique with AI-generated preference feedback [27],

17

and direct preference optimization (DPO) collapses RLHF’s two-stage pipeline into a single preference-based classification loss [28]. Additional improvements in capabilities come from inference-time reasoning, where models generate intermediate reasoning steps in a chain-of-thought before returning final responses [29]. This substantially improves performance on multi-step tasks, and also scales with tokens spent on thinking. Recent training methods reward final-answer correctness and let the model learn its reasoning process via reinforcement learning [30,31]. Beyond just responding to user inputs, recent LLMs are increasingly deployed as agents that can access and modify external systems. They do so through tool use, which exposes external functions to the agent through structured requests. This capability was advanced by methods such as ReAct, which interleaves reasoning steps with tool calls [32], and Toolformer, which trains models to invoke tools without supervision [33]. Common tools now include web search for retrieving up-to-date information, script and shell access for running code, and connections to third-party apps and APIs. The standard interface for tool integration is the Model Context Protocol (MCP), originally introduced by Anthropic in late 2024 [34] and since donated to the Linux Foundation’s Agentic AI Foundation [35]. The protocol allows developers to expose toolsets to any compatible client via dedicated MCP servers. These capabilities are increasingly available to broader audiences through consumer-facing agents such as Claude Code [36], OpenAI’s Codex [37], and the open-source OpenCode [38], and are increasingly integrated into development environments and other end-user applications. Between scaling and integration of external tools, model capabilities have advanced rapidly. On METR’s time horizon benchmark, the frontier task length at 50% completion reliability has roughly doubled every four to seven months, reaching around fourteen hours for current leading models [2–4]. Just this year, reported offensive cyber capabilities have risen sharply. Anthropic’s Claude Mythos Preview demonstrated the ability to autonomously discover and exploit zero-day vulnerabilities in major operating systems and browsers, and was held back from public release [6]. OpenAI’s GPT-5.5, released in April 2026, also demonstrated a step

18

change in offensive cyber capability, and is rated “High” for cybersecurity under the company’s Preparedness Framework, prompting expanded safeguards under OpenAI’s Trusted Access for Cyber program [7]. These capabilities pose increasing risks to existing software infrastructure, and the underlying rate of progress may itself continue to accelerate.

2.2

Formal Verification

Proof assistants were first developed for mathematics in the late 1980s and 1990s, to automate the verification of lengthy arguments or extensive case analyses. Each is built around a small logical kernel that mechanically checks every step, an architecture originating in Stanford LCF [39] and consolidated in Edinburgh LCF [40], and reusable libraries of definitions and theorems. Coq (recently renamed Rocq) is based on the Calculus of Inductive Constructions [41], and has been used for landmark pure-math formalizations such as the Four-Color [42] and Feit-Thompson theorems [43], as well as verified software including the C compiler CompCert [17]. Isabelle/HOL is built on classical higher-order logic [44] and maintains the Archive of Formal Proofs, a large community-curated library of formalized results [45]; it is also the system used to verify the seL4 microkernel [16]. Agda treats proofs and programs uniformly, with a clean functional-language syntax and dependent pattern matching [46]. Lean was created by Leonardo de Moura at Microsoft Research in 2013 [47], combining a small trusted dependent-type-theory kernel with support for both interactive and automated theorem proving. Lean 3 introduced a metaprogramming framework in which proof procedures are themselves Lean programs, in contrast to Coq’s Ltac domain-specific tactic language [48]. The community-maintained library mathlib, factored out of Lean’s core library in 2017, consolidates definitions and theorems within a single repository, with shared dependencies and consistent style [49]. By 2025 it contained over two million lines of formalized mathematics. It also supports notable standalone projects such as Scholze’s Liquid Tensor Experiment [50]

19

and the Polynomial Freiman-Ruzsa conjecture [51]. Lean 4 [11], released in 2021, rewrites the kernel, elaborator, and tactic framework in Lean itself, creating a unified language for both proofs and programs. The community port of mathlib to Lean 4 completed in 2023. The Lean ecosystem consists of tooling that exposes proof state programmatically: tactic libraries such as Aesop provide configurable best-first proof search for Lean [52], and the Lean language server exposes elaboration state, goals, and diagnostics over a uniform protocol. A more recent Model Context Protocol bridge wraps the language server, making this proof state directly queryable by LLM agents [53]. Beyond mathematics, Lean is increasingly being used for code verification, in projects such as the Rust-to-Lean Aeneas pipeline [54,55] and VCV-io, a framework for cryptographic-protocol proofs [56]. This combination of a unified language, a deep mathematical library, and a programmatic tooling ecosystem has made Lean 4 the focal point of current AI-driven proof methods. Other code-focused verifiers, such as Dafny, F*, and Verus, replace user-written proofs with SMT-backed automation: the programmer annotates the program with specifications and invariants, and the solver discharges the resulting obligations. Dafny [57] is the canonical example, underlying academic systems-verification projects such as IronFleet for distributed systems [58] and VeriBetrKV for storage [59]. F* [60] is similarly SMT-backed but further extends the type system, underlying active cryptographic-verification research including HACL* [15], whose verified code is reused in libraries such as libcrux [61]. Verus [62] extends Rust with verification annotations while preserving the language’s core structure, and has been applied in projects such as OwlC for cryptographic protocols [63] and dalek-lite for the curve25519-dalek elliptic-curve library [64].

2.3

Machine Learning Methods for Lean

The earliest applications of machine learning to Lean were interfaces that allowed ML systems to inspect proof state and test tactic steps, used both to train autonomous provers

20

and to assist humans. This approach originated with OpenAI’s GPT-f on Metamath [65], was ported to Lean by PACT [66], and extended in the curriculum-learning system that followed [18]. LeanDojo [67] is an open-source toolkit that extracts (state, tactic) training data from mathlib, bundled with a benchmark and ReProver, a retrieval-augmented tactic predictor. It is now the default environment for Lean ML work. More recent infrastructure includes Pantograph [68], which supports subgoal manipulation for tree-search methods, and LeanInteract [69], a Python wrapper around the Lean 4 REPL. Editor-side tools such as llmstep [70] and LeanCopilot [71] surface LLM tactic suggestions to humans writing proofs interactively. Reinforcement learning (RL) trains a model against a reward signal, updating its policy toward higher-reward outputs; in theorem proving, the reward is typically a binary success signal on completed proofs. RL-trained tactic policies are then paired with a tree-search procedure that expands candidate tactic steps and backtracks on failure to systematically explore the proof space. This combination was the first approach taken to automate Lean theorem proving. The line was opened by Polu et al. [18], which applied expert-iteration-based RL on Lean through the lean-gym infrastructure. Hypertree Proof Search [20] introduced a Monte Carlo Tree Search (MCTS)-inspired algorithm operating on proof hypergraphs. AlphaProof [14] extended this template with an AlphaZero-style value network; in combination with AlphaGeometry 2, it formed the system that reached silver-medal level at IMO 2024. A subsequent open-source wave including Kimina-Prover [72], DeepSeek-Prover-V2 [73], Goedel-Prover-V2 [74], and BFS-Prover [75,76] has continued the line of RL-trained-provers with stronger base models and richer training pipelines, sometimes replacing explicit search with model-internal reasoning. A more recent contrasting approach is to take a general-purpose LLM and give it access to Lean tooling, without fine-tuning the base model. The earliest published example is COPRA [77], which used GPT-4 in-context with proof-environment feedback and lemma retrieval; most subsequent activity uses Anthropic’s Model Context Protocol and

21

the Lean-LSP-MCP bridge [53]. Recent systems include Ax-Prover, an MCP-native prover harness [78]; Numina-Lean-Agent, Claude Code with an extended Lean MCP [79]; and Delta Prover, an iterative-repair and decomposition agent [80]. These systems are competitive with specialized provers on standard benchmarks without additional training. Subgoal decomposition splits a goal into separately-proved subproblems using Lean sorrys as placeholders, adopted by Hilbert [19], Mechanic [81], and Aristotle [82]. APOLLO [83] uses Lean’s structured error signals to localize failing subblocks in a generated proof, followed by a targeted repair pipeline. Adaptive retrieval, with roots in ReProver [67], surfaces relevant lemmas during proof search, used in REAL-Prover (over mathlib) [84] and LemmaHead (over olympiad textbooks) [85]. Test-time reinforcement learning adapts the model to a specific problem at inference, applied by AlphaProof [14] and the Kimina-Prover TTRL extension [86].

2.4

Benchmarks for LLM-Driven Formal Verification

Most existing benchmarks for LLM-driven formal theorem proving are based on mathematics. The de facto standard is miniF2F [12], a set of olympiad-level math statements formalized in multiple proof assistants. Recent systems report increasingly high pass rates, with leading provers exceeding 90%. PutnamBench [13], drawn from the undergraduate-level Putnam Competition, remains more challenging for current systems, with varying pass rates. Leading systems are also evaluated on the latest IMO and Putnam contests to test performance on problems guaranteed to be outside training data. Compared to math, code verification has far fewer benchmarks, many small or verifierspecific. DafnyBench [87] is the established Dafny benchmark, comprising 782 programs pairing specifications with code. The release baseline was a 68% pass rate for Claude 3 Opus on filling in proof annotations; later evaluations report substantially higher pass rates. For Lean and Verus, several benchmarks have been proposed since 2024 but none have been

22

reused widely enough to dominate, leaving the field without a single standard reference. vericoding-benchmark [88] is the largest code benchmark to date, evaluating end-to-end verified-code generation from formal specifications across more than 12,000 problems in Dafny, Verus, and Lean. At release, Lean verification was the hardest of the three with a reported pass rate of only 27%, leaving substantial headroom for improvement via stronger base models, frameworks, or agentic scaffolds.

23

24

Chapter 3 Updated Baselines for Lean Verification 3.1

Vericoding Benchmark Targeted Reproduction

3.1.1

Benchmark Subset Selection

We begin by obtaining updated baselines for Lean verification on a targeted subset of highquality verification tasks from vericoding-benchmark [88], to track improvements in current models since the original release. We evaluate on three Lean subsets: bignum, verified_cogen, and verina, totaling 423 problems. The bignum subset comprises 62 tasks derived from arithmetic algorithms on big numbers commonly used in cryptography, written from scratch by the Vericoding authors in Dafny and translated into Lean using an LLM-based approach. The verina subset is the original Lean release of the Verina benchmark from UC Berkeley’s sunblaze group [89], a curated collection of 189 modular tasks covering data structures, algorithms, and mathematical properties. The verified_cogen subset contains 172 tasks drawn from JetBrains Research’s VerifiedCogen benchmark [90] of Verus programs focusing on memory safety and functional correctness, also translated via LLM. We exclude the remaining Lean subsets in the benchmark (NumpySimple, NumpyTriple, APPS-test, HumanEval/CLEVER, DafnyBench, and FVAPPS) because their specifications were 25

obtained either by autoformalization from natural language documentation, by LLM translation of informal Python sources, or in part from GitHub scrapes. Among our three selected subsets, bignum was the most challenging in the original Vericoding evaluation with an overall pass rate of 12.9% (model union over the nine evaluated LLMs), verina sat at an intermediate difficulty of 25.4%, and verified_cogen was the most solved at 44.2%.

3.1.2

Harness Setup

We use the iterative self-correction harness of the original paper, referred to as the Vericoder. At each iteration, the model is shown the original Lean spec, with sorry placeholders for missing implementations and <vc-helpers> tags for optional auxiliary definitions, and is asked to return a JSON array of textual replacements (one element per placeholder, in source order). These replacements are substituted into the spec and the resulting file is verified using the Lean compiler. If verification fails, the next iteration is given the failing code together with the Lean error log. Each new set of replacements is always inserted into the unmodified original spec rather than into the previous iteration’s output. No external tools, retrieval, or web access is provided. We keep the same proof-bypass validation step, which rejects any candidate whose generated blocks contain known cheating patterns, such as sorry or admit (Lean’s incomplete-proof markers), axiom declarations, unsafe and Unchecked.cast type-correctness escape hatches, or @[extern] attributes that defer the implementation to native code. Each spec is allowed five iterations. The original evaluation allowed ten attempts on the bignum subset and five on the other two; we use five attempts uniformly across all three subsets to keep per-spec compute comparable. The paper does not note a specific reasoning configuration or an output token limit. We initially followed the code defaults when testing models: no explicit reasoning_effort or thinking budget is passed to the API, and an output cap of 16,384 tokens per call. We ended up adopting a non-reasoning baseline due to issues with output token caps and for consistency of cross-model comparisons. 26

3.1.3

Model Selection

We evaluate ten models across US labs and leading open-source contenders. The closed-source set consists of seven models: GPT-5.4 and GPT-5.4-mini from OpenAI, Claude Sonnet 4.6 and Claude Haiku 4.5 from Anthropic, Gemini 3 Flash (Preview) and Gemini 3.1 Flash-Lite (Preview) from Google, and Grok 4.20 from xAI. All seven emit no reasoning at default API settings. We excluded the following models from the closed-source set: • GPT-5.5: defaults to medium reasoning (can be turned off, not default); often spends entire output token cap on reasoning without returning content • Claude Opus 4.7: defaults to no reasoning, but spontaneously emits <think> followed by raw chain-of-thought into visible output • Gemini 3 Pro (Preview): defaults to high reasoning (cannot be turned off); also hits token cap • Grok 4.3: defaults to low reasoning (can be turned off); skipped for consistency The behavior of Opus 4.7 is particularly notable. Because the harness only extracts content within a JSON code block, the model is allowed to emit other prose without breaking the parser. Opus 4.7 appears to take advantage of this on almost every call, to a much greater extent than other models. Further, the output text appears to be a genuine model chain-of-thought, as opposed to a summary, with first-person hedging, false starts, and self-correction between failed proof attempts (Figure 3.1). In addition to consuming output tokens, this emission represents a leak in chain-of-thought protections implemented by US frontier labs in the last year. OpenAI introduced this practice with o1, surfacing only CoT summaries to users [31], and Anthropic and Google have since followed with redacted or rewritten reasoning blocks. These spontaneous <think> blocks

27

in plain output circumvent that block on raw reasoning, and may be a means by which continued reasoning trace collection and distillation of frontier models can occur. Figure 3.1: Excerpt of a Claude Opus 4.7 response on the bignum_Add_NormalizeBitString task at iteration 3. The model emits a <think> block of roughly 960 lines, including submission candidates, before closing the tag and producing a final JSON array. Total response length: 35,601 characters. <think> Let me analyze the errors and fix them. The main issues are: 1. The `natToBits` helper has omega issues 2. The proof structure has indentation issues (`·` appears unexpected) 3. Need to prove `ValidBitString` Let me simplify. I'll make `Add_` just return a valid string and prove both parts. ... [~960 lines of chain-of-thought omitted, including intermediate code blocks] ... sorry ``` Still stuck. OK submitting. </think> Looking at the errors, I need to fix: 1. The `omega` issues in `str2int_natToBits` ... ```json ["-- LLM HELPER\ndef natToBits : Nat -> List Char\n "natToBitString (Str2Int s1 + Str2Int s2)", "refine <...>"] ```

| 0 => []\n

...",

We also evaluate the latest versions of three leading open-source models: GLM 5.1, DeepSeek V4 Pro, and Qwen 3.6 27B. GLM and DeepSeek were both evaluated in the original Vericoding paper [88]; we additionally include Qwen, which has recently developed into one of the strongest open-weight models [91]. These models all ship reasoning on by default, but since all seven closed-source models in our set run with reasoning off, we explicitly disable 28

reasoning for these models to align baselines. We run all models through OpenRouter. For closed models, we prefer providers with favorable pricing characteristics.1 For open models, we pin to official or non-quantized providers when possible.2

3.1.4

Results

Table 3.1 reports per-subset and aggregate solve rates, theoretical cost (at published provider rates), and total tokens (input + output). GPT-5.4 leads in non-reasoning Lean verification at 24.6%. Claude Sonnet 4.6 and Gemini 3 Flash form a second tier above 10%, followed by the three open-weight models. Claude Haiku 4.5 solves four specs, while GPT-5.4-mini, Gemini 3.1 Flash-Lite and Grok 4.20 fail to solve any of the 423 tasks. To compare against the original Vericoding evaluation, we recompute the paper’s permodel pass rates restricted to the same three subsets we ran (Table 3.2). Generational deltas are modest, with the closed-source US models gaining between +0.7% and +4.0% over previous generation siblings. At the budget tier the picture reverses: GPT-5.4-mini, Gemini 3.1 Flash-Lite, and Grok 4.20 all regressed to 0% from nonzero paper-baseline numbers. This pattern points to very little capability improvement on mid- and budget-tier models when reasoning is disabled. The current generation’s effort appears to have been concentrated on reasoning-mode behavior, which this non-reasoning baseline does not capture. A change from the previous year is that the open-weight frontier now outperforms the smallest closed models without reasoning: GLM 5.1 (4.3%), DeepSeek V4 Pro (2.1%), and Qwen 3.6 27B (1.7%) all sit above Claude Haiku 4.5 (0.9%). Compared to previous generations, 1

When available, we request flex processing, which offers a 50% discount while accepting higher latency and lower throughput. This option is available for GPT models through OpenAI and Gemini models through Google Vertex; we configure OpenRouter to use those providers. This option is not available for Claude (we allow any provider), and Grok models (only available through the xAI provider). Even when requested, discounted processing is not guaranteed; adherence rates appear to vary with global inference demand, with best results outside US business hours. 2 We use the official providers for GLM 5.1 (Z.ai) and Qwen 3.6 27B (Alibaba), which do not report any quantization; model weights are published online as BF16. The official DeepSeek provider is blocked due to data policy guardrails; we use third-party providers for DeepSeek V4 Pro which report a FP8 quantization.

29

Table 3.1: Cross-model reproduction of the Vericoding Lean benchmark, non-reasoning baseline. Each model is given five iterations per spec, matching the paper’s Lean protocol [88], except on bignum. Closed-source rows run with reasoning off by default. Open-source rows (GLM, DeepSeek, Qwen) have reasoning explicitly disabled. The model union counts a task as solved if any of the ten models solved it. Cost is computed at provider published list rates; Tokens is the sum of input and output. Lean gpt-5.4 claude-sonnet-4.6 gemini-3-flash glm-5.1 deepseek-v4-pro qwen-3.6-27b claude-haiku-4.5 gpt-5.4-mini gemini-3.1-flash-lite grok-4.20 model union

BigNum

VerifCogen

Verina

Totals ↓

Cost

Tokens

62 tasks

172 tasks

189 tasks

423 tasks

–

–

9.7% 9.7% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0%

33.1% 15.7% 8.7% 4.1% 2.9% 2.9% 1.7% 0.0% 0.0% 0.0%

21.7% 15.3% 14.8% 5.8% 2.1% 1.1% 0.5% 0.0% 0.0% 0.0%

24.6% 14.7% 10.2% 4.3% 2.1% 1.7% 0.9% 0.0% 0.0% 0.0%

$23.57 $50.98 $5.71 $15.82 $17.80 $8.56 $12.36 $3.57 $1.72 $5.66

5.2M 7.8M 6.4M 8.0M 6.9M 6.0M 8.3M 3.4M 5.8M 4.4M

12.9%

42.4%

29.1%

32.2%

–

–

both GLM 5.1 (+3.3% over GLM 4.5) and DeepSeek V4 Pro (+2.1% over DeepSeek V3.1) show improvements, though the absolute gap to GPT-5.4 remains large.

3.1.5

Chain-of-Thought Emission

Looking more closely at model responses, several models also emit visible chain-of-thought into the output channel. The Vericoder prompt instructs the model to output JSON, but does not specifically forbid prose: it instructs the model to “Return a JSON array with EXACTLY N replacements. . . in order from top to bottom”. We analyze the distribution and proportion of visible thinking across models, prorating each spec’s response characters against its API-reported output_tokens. Results are reported in Table 3.3. Anthropic models spend a large share of every output budget on visible deliberation before their final JSON: Claude Sonnet 4.6 averages 56.6%, and Claude Haiku 4.5 averages 26.9%. The open-source models, asked to disable reasoning, emit qualitatively similar but

30

Table 3.2: Comparison of our reproduction against the Vericoding paper baseline [88], both restricted to the same three Lean subsets (bignum, verified_cogen, verina; n = 423). Paper percentages recomputed on the three tested subsets. Reproduction deviates slightly as bignum also has five iterations in the reproduction, as opposed to ten in the original paper. Change computed from unrounded pass rates. Our model

Ours

Paper sibling

Paper

Change

gpt-5.4 claude-sonnet-4.6 gemini-3-flash glm-5.1 deepseek-v4-pro qwen-3.6-27b claude-haiku-4.5 gpt-5.4-mini gemini-3.1-flash-lite grok-4.20

24.6% 14.7% 10.2% 4.3% 2.1% 1.7% 0.9% 0.0% 0.0% 0.0%

gpt-5 claude-sonnet-4 gemini-2.5-pro glm-4.5 deepseek-chat-v3.1 no sibling no sibling gpt-5-mini gemini-2.5-flash grok-code

22.5% 10.6% 9.5% 0.9% 0.0% — — 2.6% 0.2% 2.4%

+2.1% +4.0% +0.7% +3.3% +2.1% — — −2.6% −0.2% −2.4%

milder deliberation: Qwen 3.6 27B at 23.7% of budget, DeepSeek V4 Pro at 13.6%, and GLM 5.1 at 10.4%. Grok, Gemini, and GPT models emit little to no visible thinking. Further, many responses contain multiple JSON code blocks in succession (a draft, then a self-corrected refinement, then another); however, the harness regex extracts only the first. We measure and report rates of multiple code blocks in Table 3.4. This behavior concentrates in the same models that emit visible deliberation: Claude Sonnet 4.6 emits multiple JSON blocks on 53.9% of its 1,817 responses (worst-case 13 blocks spanning 41,082 characters), Claude Haiku 4.5 on 16.0%, and the open-weight models at lower rates (Qwen 8.3%, DeepSeek 1.1%, GLM 0.7%). GPT-5.4, GPT-5.4-mini, and Gemini 3.1 Flash-Lite always emit a single code block. The code-block-capturing logic of the Vericoding harness appears designed for small amounts of incidental text (such as “Here’s the answer” or similar), not extended withinresponse reasoning with successive candidate blocks. The cross-provider comparison is therefore unfair in two opposing directions for the Anthropic and open-source models. They may gain an advantage from extended within-response reasoning that refines their answers, 31

Table 3.3: Proportion of output emitted as thinking, for each model. Token counts prorate output characters against API-reported output_tokens for each model. The model output cap is set to 16,384 tokens. Model claude-sonnet-4.6 claude-haiku-4.5 qwen-3.6-27b deepseek-v4-pro glm-5.1 grok-4.20 gemini-3-flash gemini-3.1-flash-lite gpt-5.4 gpt-5.4-mini

N 1,817 2,010 1,633 1,774 2,028 1,597 1,927 2,032 1,768 1,584

prose / total mean tokens 56.6% 26.9% 23.7% 13.6% 10.4% 2.3% 0.1% 0.0% 0.0% 0.0%

717 180 237 111 97 8 0 0 0 0

p95 tokens

max tokens

1,439 889 1,646 239 253 0 0 0 0 0

15,595 2,222 13,538 15,620 13,245 9,724 411 160 0 0

but are simultaneously penalized when that reasoning emits intermediate JSON code blocks. The harness first-match extractor consumes the first generated code block as final, discarding any subsequent refinements. As a result, cross-model comparisons are not strictly comparable due to differing model behavior and handling. Future reproductions of the Vericoding harness could either adjust the original extraction logic to handle multiple code blocks, or explicitly instruct models to emit only a single code block with no visible deliberation.

3.2

Agentic Loop Baseline

3.2.1

Motivation

In the previous section, we reran the original Vericoding harness with updated models. However, this does not represent an honest baseline in the context of current model capabilities, as the configuration does not make use of three methodologies that are commonly used in model evaluations, and known to improve performance. The first is reasoning. Without it, the model must begin decoding its answer immediately upon receiving the prompt, without any room for planning or outlining. Modern frontier

32

Table 3.4: Multi-block emission: fraction of responses that contain more than one code block. multi% is the percentage of responses with more than one block; med. blocks is the median block count among multi-block responses. Model claude-sonnet-4.6 claude-haiku-4.5 qwen-3.6-27b deepseek-v4-pro glm-5.1 grok-4.20 gemini-3-flash gpt-5.4 gemini-3.1-flash-lite gpt-5.4-mini

N

multi%

med. blocks

max blocks

1,817 2,010 1,633 1,774 2,028 1,597 1,927 1,768 2,032 1,584

53.9% 16.0% 8.3% 1.1% 0.7% 0.1% 0.1% 0.0% 0.0% 0.0%

2 2 3 3 2 2 2 — — —

13 5 13 15 10 2 2 — — —

models are post-trained for this mode [30,31] and tend to use it naturally when permitted. The second is the agentic loop. Instead of starting every round with a new context, each round’s submission and result are appended as new turns to the end of the conversation. The model can refine its approach across rounds by building on prior attempts, as opposed to being forced to rederive understanding each turn. Model providers optimize for this mode through server-side KV caching, eliminating the forward pass over the prior conversation on continuing turns. The third is access to external knowledge via tools. In the context of Lean, this takes the form of a Lean MCP server, which provides access to a search tool. The tool provides access to multiple Lean search providers which handle natural language and type-pattern queries, allowing the model to broadly access lemma names and confirm type signatures when constructing proofs. Almost all current LLM-driven Lean theorem proving systems use one or more of these methods, and recent agent-loop harnesses like Numina-Lean-Agent [79] combine all three, layered with additional scaffolding. For a modern, capability-honest baseline, we build a harness combining an agent loop, reasoning, and Lean search, against which tree-search algorithms in later sections can be evaluated. 33

3.2.2

Experimental Setup

We maintain the same input and output format as the original Vericoding setup: each spec is presented with one or more sorry holes, and submissions are expressed as a JSON array of replacement strings. We change the submission method from text output to a submit_code tool, which enforces the replacements JSON formatting via schema validation rather than relying on the model to produce a valid code block. We also filter the compiler output to remove build noise before returning feedback as tool output. We expose the search_mathlib tool from the Lean-LSP-MCP server [53], which dispatches to LeanFinder and Loogle; the model can choose which provider to use per call. As the model now has a search tool in addition to submission, we initially set the budget for each spec to ten LLM calls. The loop terminates early on a submit_code call that verifies, otherwise running until the budget is exhausted. If the model outputs text instead of a tool call, it is nudged to continue calling tools. We evaluate across the six models from OpenAI, Anthropic, and Google tested in the previous section. Reasoning effort is explicitly set to medium across all models, and we use the same 423-spec subset.

3.2.3

Initial Results

With ten LLM calls in the agent harness and medium reasoning, the union over all six models solves 263 / 423 specs (62.2%). Table 3.5 reports per-subset and aggregate solve rates. The six models all improve substantially over the Vericoder baseline of Section 3.1 on the same 423 specs: GPT-5.4 lifts from 24.6% to 60.3% (a 2.45× gain), while GPT-5.4-mini, Claude Haiku 4.5, and Gemini 3.1 Flash-Lite score significantly more than the previous 0-1%. A small number of runs (1.8% of spec and model combinations) crash due to output-truncation errors when reasoning tokens consume the entire per-call output budget, with 74% of crashes occurring on Claude Sonnet 4.6 runs. For a fair comparison between agent and Vericoder pipelines, we compare token spend and solve rate by round for the agent harness. As the agentic loop relies on the reuse of a 34

Table 3.5: Per-subset solve rates at K = 10 across the six LLMs evaluated, alongside the six-model union and the Vericoder union for the same six models. Cost is total spend at provider list rates assuming perfect prompt caching and free cache reads; Tokens is the corresponding unique token count (output includes reasoning). BigNum

VerifCogen

Verina

Totals ↓

Cost

Tokens

62 tasks

172 tasks

189 tasks

423 tasks

–

–

gpt-5.4 gpt-5.4-mini claude-sonnet-4.6 gemini-3-flash claude-haiku-4.5 gemini-3.1-flash-lite

19.4% 12.9% 11.3% 6.5% 11.3% 3.2%

75.0% 43.6% 34.9% 25.6% 24.4% 21.5%

60.3% 38.1% 30.7% 24.9% 17.5% 11.1%

60.3% 36.6% 29.6% 22.5% 19.4% 14.2%

$65.06 $25.88 $41.10 $16.42 $9.54 $2.23

10.9M 11.4M 5.9M 6.3M 4.4M 2.7M

model union Vericoder (6 models)

19.4% 12.9%

78.5% 41.9%

61.4% 28.6%

62.2% 31.7%

– –

– –

Lean

cached input prefix across LLM calls, we count unique tokens: the sum of input and output tokens across all unique blocks, not counting duplicate cache reads. We compute cost by multiplying unique input and output tokens by respective billing rates, which corresponds to the assumption of optimal caching for all input blocks and free cache reads.3 The original Vericoder constructs a new prompt each turn, resulting in minimal caching across rounds.4 Figure 3.2 plots solve rate against unique tokens for the six models, iterated over the number of model calls. Original token count and solve rate from Vericoder are also indicated. At matched unique-token budgets, the OpenAI, Anthropic, and Gemini families all lie above their Vericoder counterparts from Section 3.1. Gemini 3.1 Flash-Lite emits the fewest tokens of any model evaluated, and at matched unique-token budgets it outperforms Gemini 3 Flash. GPT-5.4 emits fewer cumulative tokens than GPT-5.4-mini despite solving more specs. Both 3

In practice, actual cache hit rates vary depending on timing of requests, provider routing, and other uncontrollable factors; however, they are generally high for a simple agentic loop as described. Cached tokens are also not entirely free; they are typically discounted around 90% for recent models. For a 10-turn agentic loop, 10 cache reads averaging half the input adds approximately 50% to the input price. Some providers, such as Anthropic, additionally charge extra for cache writes over standard input prices. 4 The Vericoder prompt is not optimized for prefix caching, as it increments the turn count early in the prompt. We still observe a small amount of prompt caching for providers that automatically cache within blocks. The prompt consists of instructions + error + original file + last submitted file; with a bit of reordering, the instructions + original file could be cached, reducing unique input by around 50%. However, even a 50% decrease in Vericoder unique tokens would not significantly change the results at matched tokens.

35

OpenAI models use adaptive reasoning, which allocates reasoning tokens based on problem difficulty. GPT-5.4 can resolve specs in fewer tokens because the problem is easier relative to its capabilities, whereas GPT-5.4-mini thinks longer on the same problem without always succeeding. Claude Sonnet 4.6 uses the fewest tokens per spec of the mid-tier models, but performs worse than the budget-tier GPT-5.4-mini at a higher cost. The bottom row of Figure 3.2 shows per-subset solve trajectories. bignum remains challenging across all six models, with the six-model union covering only 12 / 62 specs (19.4%) versus 62.2% on the full set. This union is exactly the set of specs solved by GPT-5.4, with every other model’s solves being a strict subset. The two Claude models tie at 11.3% (7 / 62 each), while both Gemini models perform particularly poorly on this subset, with Gemini 3 Flash leveling off at 6.5% of specs solved and Gemini 3.1 Flash-Lite only reaching 3.2%.

3.2.4

Agent Tool Call Behavior

For a comparison of submission counts, we look into tool-calling behavior of models in the agent harness. Figure 3.3 plots per-turn averages of total tool calls, search_mathlib calls, and submit_code calls across the first ten turns, normalized by the number of specs still active at that round. Most models batch multiple tool calls, more in the initial rounds than later ones. OpenAI models use parallel tool calling most aggressively, with GPT-5.4 issuing three search_mathlib calls in 77% of search turns, with a maximum of four. Claude Sonnet 4.6 calls two parallel searches on 82% of its search turns and never more than two. Gemini 3 Flash only requests multiple searches on 8% of search turns, and Gemini 3.1 Flash-Lite never batches, always making one tool call per turn. No model ever issues more than one submit_code call in a single turn, though parallel submissions are not explicitly forbidden. Mixing a search and a submission inside one turn is also rare: only Claude Sonnet 4.6 (1.4% of turns) and Gemini 3 Flash (0.14%) ever do so, while the other four models always keep the two tools separate. Table 3.6 aggregates per-turn averages over the ten-turn window and the search-to-submit 36

Figure 3.2: Solve rate vs. average unique tokens per spec, iterated over K = 1, 2, . . . , 10 model calls, for each of the six LLMs. Top: full 423-spec set. Bottom row, left to right: bignum, verified_cogen, and verina subsets. Dashed vertical lines mark each LLM’s Vericoder tokens per spec from Section 3.1, with diamond markers at the corresponding Vericoder solve rate. 37

Figure 3.3: Average total tool calls per turn (left), search_mathlib calls per turn (middle), and submit_code calls per turn (right), across the first ten turns of the agent loop on the full 423-spec set. Per-turn averages are conditional on a spec still being active at that round. ratio for each model. The OpenAI models utilize retrieval most heavily: GPT-5.4-mini issues 7.2 searches for every submit and GPT-5.4 issues 5.3. GPT-5.4-mini’s higher ratio likely reflects the problems being harder relative to its capabilities, requiring more lemma lookups before each submission attempt. Conversely, weaker-performing models have a lower search-to-submit ratio, such as Claude Haiku 4.5 with a ratio of 1.8. Gemini 3.1 Flash-Lite inverts the ratio entirely at 0.28, submitting in most turns as opposed to searching. This suggests the weaker models are less tuned to the task’s combined demands of logical reasoning and lemma lookup. For every model except Gemini 3.1 Flash-Lite, the sum of average submit calls per turn is less than five, indicating that models on average invoke the Lean compiler fewer times than in the Vericoder baseline.

38

Table 3.6: Per-model summary of tool-call behavior across the first ten agent turns on the full 423-spec set. Totals sum per-turn averages over rounds 1–10; Ratio is total search_mathlib divided by total submit_code. gpt-5.4 gpt-5.4-mini claude-sonnet-4.6 claude-haiku-4.5 gemini-3-flash gemini-3.1-flash-lite

3.2.5

Total search

Total submit

Total calls

Ratio

17.53 13.77 12.24 7.63 7.86 2.11

3.48 1.93 3.28 4.46 2.83 7.89

21.00 15.70 15.52 12.09 10.70 10.00

5.29 7.17 3.91 1.80 2.81 0.28

Longer-Context Evaluations

The Figure 3.2 curves climb roughly linearly through K = 10 for most models. GPT-5.4-mini solves a greater proportion of specs in the first few turns, then marginal solve rate starts decreasing. GPT-5.4 shows no sign of slowing, with a similar number of additional solves each turn. Test-time scaling theory predicts that solve rate eventually flattens: as a model approaches its capability ceiling for the task, additional tokens provide less additional benefit, and the curve plateaus. The K = 10 trajectories give little to no evidence of this transition, indicating that more turns may continue to provide increases in overall benchmark performance. To test further scaling behavior, we extend the agent loop on the same 423-spec set past K = 10. We narrow our tests to OpenAI and Google models, as the OpenAI models produced the highest absolute solve rates at K = 10, the Google models offer a low-cost comparison, and both are offered by providers with favorable pricing. We resume every spec and model in increments of ten LLM calls, ending at a final budget of K = 50 per spec. Figure 3.4 shows pass rate curves through K = 50 for all four models. GPT-5.4 climbs from 60.3% at K = 10 to 95.0% at K = 50, while the other three models each improve by roughly 10 to 20 percentage points over the same range. Table 3.7 reports per-subset pass rates and per-spec tokens up to K = 50. GPT-5.4

39

reaches 87.1% on bignum, 96.5% on verified_cogen, and 96.3% on verina; the three weaker models pick up most of their additional solves on verified_cogen and verina while making little to no additional progress on bignum. All models except Gemini 3.1 Flash-Lite spend the fewest tokens on verified_cogen and substantially more tokens on bignum, reflecting relative subset difficulties and adaptive reasoning effort; Gemini 3.1 Flash-Lite does not show appreciable output length differences across subsets. For GPT-5.4 and to a lesser extent GPT-5.4-mini, marginal tokens per round decreases as K grows, since specs solved at earlier rounds no longer contribute additional tokens to the running average. Particularly notable is the solve rate of GPT-5.4 on bignum across rounds, shown in Table 3.8. After an initial nine solves at K = 5, marginal progress slows to three to five additional specs per five-round increment, reaching 20 / 62 (32.3%) at K = 20. The curve then accelerates sharply: 22 specs are solved between K = 20 to 30, more than doubling the cumulative solve count. The model solves another eight specs to reach 50 / 62 (80.6%) at K = 35 before the rate decays, with only four more solves by K = 50. Per-task solve trajectories of this shape have been noted in the test-time scaling literature [92]. The 95.0% pass rate at K = 50 for GPT-5.4 indicates that vericoding-benchmark is effectively saturated by recent model capabilities. GPT-5.4 is currently considered the mid-tier model in OpenAI’s lineup, and saturation is achieved at medium reasoning; it is possible that frontier models such as GPT-5.5, with higher reasoning effort, can reach saturation in significantly fewer turns. Taken together, the reasoning, agentic loop, and MCP tool changes produce substantial improvements over the Vericoder baseline, across subsets and models. The agent harness establishes a strong baseline reflecting modern model capabilities, and the Pareto curves provide benchmarks against which tree-search methods can be evaluated at matched token usage.

40

Figure 3.4: K = 50 continuation of four-LLM agent comparison, beyond the K = 10 cap of Figure 3.2. Top: full 423-spec set. Bottom row, left to right: bignum, verified_cogen, and verina subsets. Dashed vertical lines mark each LLM’s Vericoder tokens per spec from Section 3.1, with diamond markers at the corresponding Vericoder solve rate.

41

Table 3.7: Agent benchmark pass rate at varying LLM-call budgets K, across the four LLMs evaluated. Each cell shows pass rate / average unique tokens per spec at that K. Subset

K=10

n

K=20

K=30

K=40

K=50

gpt-5.4 BigNum 62 19.4% / 46k 32.3% / 94k 67.7% / 123k 83.9% / 135k 87.1% / 139k VerifCogen 172 75.0% / 19k 89.5% / 26k 94.8% / 27k 95.3% / 28k 96.5% / 29k 96.3% / 45k Verina 189 60.3% / 26k 86.2% / 38k 92.1% / 41k 93.7% / 44k Combined 423 60.3% / 26k 79.7% / 41k 89.6% / 48k 92.9% / 51k 95.0% / 52k gpt-5.4-mini BigNum 62 12.9% / 40k 12.9% / 84k 14.5% / 129k 16.1% / 172k 17.7% / 207k VerifCogen 172 43.6% / 20k 55.2% / 39k 61.6% / 53k 69.2% / 65k 70.9% / 74k Verina 189 38.1% / 28k 43.9% / 52k 48.1% / 72k 52.9% / 89k 57.1% / 101k Combined 423 36.6% / 27k 44.0% / 51k 48.7% / 72k 54.1% / 91k 57.0% / 105k gemini-3-flash BigNum 62 6.5% / 24k 6.5% / 35k 8.1% / 49k 8.1% / 63k VerifCogen 172 25.6% / 11k 33.1% / 17k 39.0% / 22k 43.6% / 28k Verina 189 24.9% / 15k 30.7% / 23k 38.1% / 32k 39.2% / 42k Combined 423 22.5% / 15k 28.1% / 22k 34.0% / 30k 36.4% / 39k

9.7% / 78k 45.9% / 33k 40.2% / 52k 38.1% / 48k

gemini-3.1-flash-lite BigNum 62 VerifCogen 172 Verina 189 Combined 423

3.2% / 7k 3.2% / 11k 3.2% / 15k 3.2% / 19k 21.5% / 6k 25.0% / 11k 26.7% / 16k 27.9% / 21k 11.1% / 7k 21.2% / 12k 24.9% / 17k 25.4% / 22k 14.2% / 6k 20.1% / 11k 22.5% / 16k 23.2% / 21k

3.2% / 23k 31.4% / 26k 25.4% / 28k 24.6% / 26k

Table 3.8: gpt-5.4 cumulative solves on bignum, sampled every five LLM calls through K = 50. Highlighted rows indicate the K = 20 to 30 range, where 22 of the eventual 54 solves occur. K

solved / 62

%

Change

5 10 15 20 25 30 35 40 45 50

9 12 15 20 31 42 50 52 53 54

14.5% 19.4% 24.2% 32.3% 50.0% 67.7% 80.6% 83.9% 85.5% 87.1%

+9 +3 +3 +5 +11 +11 +8 +2 +1 +1

42

Chapter 4 Search Methods for Lean Verification 4.1

Searching Over Partial Proofs

4.1.1

Motivation

The agent loop of Section 3.2 substantially improves over the Vericoder of Section 3.1, and extended to K = 50 in Section 3.2.5, GPT-5.4 reaches 95.0% on the combined 423-spec set and 87.1% on bignum, effectively saturating the benchmark. However, this saturation is confined to the strongest tested model and incurs significant token cost. At K = 50, GPT-5.4-mini reaches only 17.7% on bignum, picking up just three additional solves on this subset between K = 10 and K = 50. Each bignum spec at K = 50 averages 139k unique tokens for GPT-5.4 and 207k unique tokens for GPT-5.4-mini. A sign that faster solves are possible is the shape of GPT-5.4’s bignum solve curve (Table 3.8): the cumulative rate climbs slowly through K = 20 at 32.3%, then jumps to 67.7% across K = 20 → 30, before flattening to its K = 50 ceiling of 87.1%. One possible reason for this shape is context-induced anchoring: once an agent starts attempting a strategy in the first few turns, subsequent turns are more likely to extend and reinforce that strategy rather than reconsider it [93,94]. This may lead to an initial plateau before the model switches directions and constructs a solve using a more viable strategy. For smaller models, the agent 43

may continue to attempt tactics within a fixed strategy while a more successful direction is never explored. Tree-search methods are a general family of algorithms that maintain multiple candidate states, choosing at each step which one to extend. Applied to proofs, tree search has been a dominant approach across years of work, and naturally serves as a counter to such anchoring. In the standard setup, nodes of the search tree are partial-proof states (a tactic state with its open goals, or one abstraction layer above such as a sketch or subgoal frontier), and the goal is to reach a node corresponding to a fully written, verified proof. A search algorithm then governs which node to expand next. Previous proof-search systems mostly follow a score-then-expand pattern. An evaluation signal, either a hand-coded heuristic or a learned value head, assigns each node a numerical score; a selection rule, such as PUCT in MCTS-style systems like AlphaProof [14] or bestfirst-by-policy in BFS-Prover [75], uses these scores to pick the next node to expand. The systems differ mainly on the granularity of expansion, ranging from one Lean tactic per edge in MCTS to an entire proof sketch or subgoal in draft-then-fill approaches [19,73]. We hypothesize that LLMs can offer a more flexible alternative: through direct prompting, we can ask a model to reason about high-level proof direction, as opposed to just attempting implementation. We aim to replace both the numerical evaluation signal and selection rule, with two primary model roles. A parent agent handles evaluation and selection, proposing the next high-level strategy to attempt. A subagent then handles expansion, attempting to extend the partial-proof state towards a complete, verified solution.

4.1.2

Experimental Setup

We design a state-based orchestrator, which consists of a parent agent that directs the proof, and subagents which explore the proof-state tree. At the start, the parent uses an explore_variations call to spawn multiple subagents for up to five turns each. Each subagent is primed with a different advice string drawn from a five-class strategy palette 44

so that subagents pursue different proof directions. The palette deliberately includes recent automation tactics such as grind, which are powerful techniques for automatically closing goals but under-represented in older pretraining data. Each subagent branches off the parent’s conversation, inheriting the full history of prior decisions and the current partial-proof state, which starts at the original spec. Like the agent harness, subagents are equipped with search_mathlib and submit_code tools to query mathlib and attempt proofs. On a verified submit_code the proof is returned and the parent exits; otherwise each subagent returns a debrief summarizing what it tried and what blocked it. A subagent that judges its direction dead can also abandon early, returning a debrief before using all turns. Given the subagent debriefs, the parent can choose to update the base state against which replacements are generated. update_base commits a partial-proof state surfaced by one of the subagents, and undo_base reverts to the previous base. Each update_base and undo_base step walks an explicit proof-state tree implicitly created by the subagents: the new base may carry fewer sorry holes if the subagent closed subgoals, or more if the replacement introduces auxiliary lemmas with their own sorry placeholders. Subsequent subagents fill replacements against the new base rather than the original spec, so the parent’s commits act as a decomposition mechanism: each committed step narrows or sharpens the remaining work for the next round. After optional base update or undo, explore_variations is called again to dispatch a new round of subagents with refined advice. The parent is advised to include specific lemma names discovered from previous subagents when constructing new advice. The parent loop repeats until a complete proof verifies, or a budget of 50 LLM calls is exhausted, accumulated across all parent and subagent turns. We run experiments with GPT-5.4 and GPT-5.4-mini, the two best-performing LLMs from the agent baseline, again at medium reasoning effort on the same 423-spec set used in Section 3.2.

45

4.1.3

Initial Results

At K = 50, the orchestrator solves 287 / 423 specs (67.8%) with GPT-5.4 and 210 / 423 (49.6%) with GPT-5.4-mini. Against the agent baseline at K = 50, the orchestrator trails by 27.2% on GPT-5.4 and by 7.4% on GPT-5.4-mini. The parent loop’s tool-call distribution confirms that the orchestrator runs the intended pipeline. Table 4.2 gives the distribution of parent tool calls over the K = 50 budget and the share of specs which use each tool at least once. The parent is instructed (but not forced) to open with explore_variations, and GPT-5.4 follows this instruction exactly, with all specs using explore_variations. A minor instruction-following lapse is noticed for GPT-5.4-mini, which immediately calls update_base for seven specs at first. One of these specs succeeds and exits, leading to the count of 422 specs using explore_variations. Figure 4.1 plots solve rate against unique tokens. The K = 1 solve rate is close to zero, as the parent has an initial reasoning turn before dispatching subagents. After the first turn, the solve rate shows its fastest increase through K = 6, corresponding to the parent turn plus five subagent turns, trailing the agent by only 5.0% for GPT-5.4 and 2.6% for GPT-5.4-mini. Table 4.1 reports per-subset pass rates and per-spec tokens up to K = 50. A large fraction of solves occur in the first explore_variations. For GPT-5.4, 52.2% of specs finish in exactly one parent turn (a variation from the first explore_variations submits a verified proof); for GPT-5.4-mini this share is 37.8%; specs solved in the first explore_variations make up at least 50% of solved specs for each model. Within the first explore_variations, most wins come from the first subagent out of up to four dispatched. The first subagent by itself generates a 41.8% solve rate for GPT-5.4 and 29.1% for GPT-5.4mini.

4.1.4

Subagent Search Behavior

To understand how the orchestrator budget is spent, we analyze how subagents allocate their five-turn budget between search_mathlib and submit_code calls. Table 4.3 reports 46

Figure 4.1: State-based orchestrator solve rate against unique tokens, plotted alongside Section 3.2 agent baseline, for gpt-5.4 and gpt-5.4-mini. Top: full 423-spec set. Bottom row, left to right: bignum, verified_cogen, and verina subsets. Orchestrator curves start later along the token axis because the first explore_variations parent call is made before any subagent submits. 47

Table 4.1: State-based orchestrator pass rate at varying LLM-call budgets K, for gpt-5.4 and gpt-5.4-mini. Each cell shows pass rate / average unique tokens per spec at that K. Subset

n

K=10

K=20

K=30

K=40

K=50

gpt-5.4 BigNum 62 16.1% / 32k 19.4% / 63k 22.6% / 90k 24.2% / 115k 32.3% / 139k VerifCogen 172 55.8% / 18k 65.7% / 30k 73.3% / 38k 76.7% / 45k 80.8% / 50k Verina 189 41.8% / 24k 49.2% / 43k 57.7% / 57k 61.4% / 68k 67.7% / 78k Combined 423 43.7% / 23k 51.5% / 40k 58.9% / 54k 62.2% / 65k 67.8% / 75k gpt-5.4-mini BigNum 62 12.9% / 31k 14.5% / 59k 14.5% / 82k 14.5% / 106k 14.5% / 123k 62.8% / 67k VerifCogen 172 40.7% / 20k 48.3% / 35k 54.1% / 46k 59.3% / 57k Verina 189 29.6% / 23k 39.2% / 43k 42.9% / 60k 47.1% / 75k 49.2% / 88k Combined 423 31.7% / 23k 39.2% / 42k 43.3% / 58k 47.3% / 72k 49.6% / 85k

Table 4.2: Parent-loop tool-call distribution over the K = 50 budget across all 423 specs. Calls counts total invocations; % of calls is the share within each model; Specs counts unique specs on which the tool is called at least once. Tool

Calls

% of calls

Specs

% of specs

704 195 67

72.9% 20.2% 6.9%

423 152 54

100.0% 35.9% 12.8%

1087 495 62

66.1% 30.1% 3.8%

422 223 54

99.8% 52.7% 12.8%

gpt-5.4 explore_variations update_base undo_base gpt-5.4-mini explore_variations update_base undo_base

48

per-variation totals separately for the first and second explore_variations call within each spec, alongside the corresponding agent baseline from Section 3.2. For GPT-5.4, the search-to-submit ratio inside a first-explore variation is 11.5, more than double the agent’s ratio of 5.3 over a ten-turn budget. The ratio remains elevated in the second explore at 8.2, even though the parent has already received one round of debriefs and can pass refined advice. GPT-5.4-mini’s first-explore ratio is 9.5 against an agent ratio of 7.2, dropping to 4.7 in the second explore. These high search ratios, combined with the five-turn subagent budget, lead to low submission counts: a variation averages roughly one submit_code call across all four cohorts (0.77 to 1.14). Each subagent inherits the parent’s prompt and partial-proof state but no tool history, so its early turns are dominated by running lemma searches, overlapping with searches other variations have already performed in prior rounds. Whereas the agent in Section 3.2 can use early searches across all rounds, every orchestrator dispatch leads to fresh searches in subagents. This motivates allowing subagent context to be preserved across parent rounds, rather than forcing each variation to rebuild it from scratch. We extend the parent’s toolset with a resume_variations call: instead of spawning fresh subagents, the parent picks one or more prior subagents and continues them, optionally with refreshed advice consolidated from all current debriefs. The parent retains discretion over which variations to resume, allowing it to prioritize promising subagents while conserving LLM-call budget by not resuming the rest. The partial progress mechanism of update_base and undo_base remains unchanged. However, committing a new base implicitly invalidates any prior subagent context, since the partial-proof target a resumed subagent was working against no longer matches. After an update_base or undo_base, we make previous subagents ineligible for resume and require the parent to dispatch fresh subagents.

49

Table 4.3: Average tool-call totals per subagent variation over its five-turn budget, split by first or second parent explore_variations call. Turns/Var is the average number of active turns per variation (out of five). Ratio is total search_mathlib divided by total submit_code across the variation. Agent rows are ten-turn totals from the Section 3.2 baseline (Table 3.6). Model

Block

gpt-5.4 gpt-5.4 gpt-5.4 gpt-5.4-mini gpt-5.4-mini gpt-5.4-mini

4.1.5

# Var

Turns/Var

Search

Submit

Ratio

agent (10 turns) 1st explore 2nd explore

— 982 582

— 4.22 4.56

17.53 11.24 9.36

3.48 0.98 1.14

5.29 11.47 8.21

agent (10 turns) 1st explore 2nd explore

— 894 511

— 4.38 4.20

13.77 7.30 4.25

1.93 0.77 0.91

7.17 9.48 4.67

Final Results

Adding resume_variations to the parent toolset negatively affects the combined solve rate. At K = 50, GPT-5.4 drops 1.4% to land at 66.4% (281 / 423), while GPT-5.4-mini regresses 2.6% to 47.0% (199 / 423). Figure 4.2 plots the resume-enabled orchestrator against the Section 4.1.3 no-resume orchestrator and the Section 3.2 agent, showing small gains and losses between models and subsets. Table 4.4 reports per-subset pass rates and per-spec tokens up to K = 50. Table 4.5 reports the new parent tool-call distribution. GPT-5.4-mini makes heavier use of resume_variations, accounting for 21.7% of parent calls compared to 11.0% for GPT-5.4. explore_variations, update_base, and undo_base each drop relative to the no-resume distribution in Table 4.2. This difference in usage rate also translates into per-spec coverage: GPT-5.4-mini uses resume on 53.9% of specs, while GPT-5.4 resumes on only 21.3%. The intended design of resume_variations was for subagents granted more turns to shift from searching to submitting. Table 4.6 shows the opposite: for the second parent turn when resume is chosen, search_mathlib accounts for 91.9% of subagent calls on GPT-5.4 and 93.0% on GPT-5.4-mini, higher than both the corresponding fresh second-explore rates and the first-explore rates. A possible reason is that the advice provided to resumed subagents contains methods and lemma names across the first round of subagents, leading resumed 50

Table 4.4: State-based + resume orchestrator pass rate at varying LLM-call budgets K, for gpt-5.4 and gpt-5.4-mini. Each cell shows pass rate / average unique tokens per spec at that K. Subset

n

K=10

K=20

K=30

K=40

K=50

gpt-5.4 BigNum 62 12.9% / 30k 14.5% / 62k 19.4% / 89k 22.6% / 116k 24.2% / 142k VerifCogen 172 54.7% / 18k 65.1% / 30k 73.8% / 38k 77.9% / 44k 82.6% / 49k Verina 189 46.6% / 21k 52.9% / 38k 57.7% / 51k 61.4% / 62k 65.6% / 72k Combined 423 44.9% / 21k 52.2% / 38k 58.6% / 51k 62.4% / 62k 66.4% / 73k gpt-5.4-mini BigNum 62 12.9% / 29k 12.9% / 59k 14.5% / 88k 14.5% / 114k 17.7% / 137k VerifCogen 172 37.2% / 19k 45.9% / 34k 49.4% / 49k 51.2% / 63k 57.6% / 75k 47.1% / 81k Verina 189 31.7% / 19k 36.5% / 35k 41.8% / 52k 43.9% / 67k Combined 423 31.2% / 20k 36.9% / 39k 40.9% / 56k 42.6% / 72k 47.0% / 87k

subagents to search again for mentioned lemmas instead of refining submissions. We ran small-batch evaluations on several additional orchestrator modifications: • Dynamic turn budgets: allocates varying turn budgets depending on the number of subagents, to keep each explore_variations call count a similar amount towards the total budget • Skeptical LLM reviewer: a second model reviews the debriefs from the subagents, returning a second proof feasibility signal to the parent agent • Submission Elo ranking: submissions from subagents are ranked by an LLM judge and assigned Elo scores, with the top submissions across rounds exposed to the parent agent On the spec batches we evaluated, none of these shifted the headline solve rate beyond run-to-run variance; we leave further exploration of these methods to future work.

51

Figure 4.2: State-based + resume orchestrator solve rate against unique tokens, plotted alongside Section 4.1.3 no-resume predecessor and Section 3.2 agent baseline, for gpt-5.4 and gpt-5.4-mini. Top: full 423-spec set. Bottom row, left to right: bignum, verified_cogen, and verina subsets. 52

Table 4.5: Parent-loop tool-call distribution over the K = 50 budget across all 423 specs, with resume_variations enabled. Calls counts total invocations; % of calls is the share within each model; Specs counts unique specs on which the tool is called at least once. Tool

Calls

% of calls

Specs

% of specs

617 160 102 47

66.6% 17.3% 11.0% 5.1%

423 132 90 40

100.0% 31.2% 21.3% 9.5%

805 354 332 42

52.5% 23.1% 21.7% 2.7%

423 187 228 38

100.0% 44.2% 53.9% 9.0%

gpt-5.4 explore_variations update_base resume_variations undo_base gpt-5.4-mini explore_variations update_base resume_variations undo_base

Table 4.6: Average tool-call totals per subagent variation, split by parent call: first explore_variations, second explore_variations, or resume_variations chosen as the second decision. Turns/Var is the average number of active turns per variation; explore variations have a five-turn budget, while resume variations are cumulative with their source explore (up to ten turns total). Ratio is total search_mathlib divided by total submit_code across the variation. Model Block # Var Turns/Var Search Submit Ratio gpt-5.4 gpt-5.4 gpt-5.4

1st explore 2nd explore resume (as 2nd)

1,001 395 148

4.27 4.32 8.45

9.31 7.32 17.37

0.89 0.91 1.53

10.49 8.03 11.38

gpt-5.4-mini gpt-5.4-mini gpt-5.4-mini

1st explore 2nd explore resume (as 2nd)

950 380 272

4.40 4.12 8.57

6.11 3.29 11.62

0.65 0.79 0.87

9.35 4.16 13.34

53

4.2

Searching Over Agent Contexts

4.2.1

Motivation

In Section 3.2 we found that models perform well with longer context, allowing for more turns to search lemmas and refine proof attempts. The analysis in Section 3.2.4 and Section 4.1.4 breaks down the behavior of subagents across turns: early searches of lemmas in context help the model craft more submissions, and without this context subagents return to searching instead of submitting. Compared to the agent loop’s search-to-submit ratio of 5.3 for GPT-5.4 over the first ten turns, the ratio for empty-context subagents more than doubles to 11.5, despite half the turn budget. The design of the state-based orchestrator takes nodes to be partial-proof states against which the next round of subagents is dispatched. However, subagent contexts are not preserved between rounds; this throws away exactly the chain of mathlib queries, verifier diagnostics, and abandoned tactics that produced the updated state. The reframing is to save the path (context), instead of just the node (partial proof). The challenge is reasoning, not formatting: completing the proof needs the same evidence base that the prior subagent used. Narrowing the proof simplifies the replacements to generate, but generating valid output is not the bottleneck, and the previous context implicitly carries the partial-proof progress. The same logic applies for the parent, which can make better decisions looking back at the entire subagent context rather than per-round debriefs, which compress multiple subagent turns into a single paragraph. Together, these observations motivate a design which gives first-class support to continuous context while preserving a tree-search structure. We keep the parent-director / subagentprover framework from Section 4.1, including advice-primed subagents and parent-side access to the proof-state tree. We change what an edge of the search tree carries: rather than only the partial-proof state at its endpoint, the edge inherits the parent’s full message history plus the subagent’s per-turn transcript. Searching through multiple proof states creates a tree of

54

branching contexts, each carrying reasoning history and an evidence base for further searches.

4.2.2

Experimental Setup

We design a context-based orchestrator with emphasis on context preservation. The parent agent starts by dispatching a single subagent, running for up to ten turns instead of five. Subagents succeed, fail, or abandon as usual and return a debrief, but the parent operates on top of this context rather than only the compressed debrief. The subagent transcript, including all tool calls, is recorded as an endpoint on which the next parent decision can branch. The parent is given two tools that operate on the available endpoints. dispatch_subagent spawns a new subagent with a fresh advice block from the parent. resume_endpoint instead re-enters a prior subagent’s exact context, allowing it to continue with a fresh turn allowance. These two tools naturally build a tree: one creates a new branch, and the other continues an existing one. The parent may also choose to abandon a spec early if determined infeasible. The total budget across parent and subagent turns remains at 50 LLM calls, and we again use GPT-5.4 and GPT-5.4-mini.

4.2.3

Initial Results

Our context-based orchestrator outperforms the state-based orchestrator from Section 4.1.3 on GPT-5.4, reaching 81.8% at K = 50 (+14.0%); on GPT-5.4-mini it remains nearly unchanged at 49.9% (+0.3%). Figure 4.3 plots solve rate against average unique tokens per spec, and Table 4.7 reports per-subset solve rates across K. The context-based orchestrator initially produces solves at a similar rate as the previous one, as the first few turns correspond to the first subagent in both designs. The slope of the solve curve improves, matching the agent through ten LLM calls as opposed to quickly plateauing. This is not surprising as the new orchestrator acts as an agentic loop in its first subagent dispatch. This matching remains through K = 10 even with an initial parent turn, 55

Table 4.7: Context-based orchestrator pass rate at varying LLM-call budgets K, for gpt-5.4 and gpt-5.4-mini. Each cell shows pass rate / average unique tokens per spec at that K. Subset

n

K=10

K=20

K=30

K=40

K=50

gpt-5.4 BigNum 62 17.7% / 38k 29.0% / 68k 40.3% / 96k 45.2% / 122k 45.2% / 148k VerifCogen 172 68.6% / 17k 77.3% / 25k 84.9% / 30k 87.2% / 33k 89.5% / 35k Verina 189 56.6% / 23k 72.0% / 34k 79.9% / 40k 84.1% / 45k 86.8% / 48k Combined 423 55.8% / 23k 67.8% / 35k 76.1% / 44k 79.7% / 51k 81.8% / 57k gpt-5.4-mini BigNum 62 14.5% / 36k 14.5% / 68k 17.7% / 95k 17.7% / 123k 17.7% / 154k 60.5% / 64k VerifCogen 172 47.7% / 19k 52.3% / 31k 55.8% / 43k 58.7% / 54k Verina 189 33.9% / 26k 42.3% / 43k 48.1% / 61k 49.7% / 75k 50.8% / 89k Combined 423 36.6% / 24k 42.3% / 42k 46.8% / 59k 48.7% / 73k 49.9% / 88k

reaffirming the strength of initial reasoning. However, the Pareto picture is less favorable at later iterations, with the GPT-5.4 orchestrator curve crossing below the agent curve after K = 10 for the two easier subsets. On the challenging bignum subset, the orchestrator maintains a slight lead over the agent through K = 20, before falling off afterwards.

4.2.4

Empty-Context Resume Behavior

Within the orchestrator curves, there is a notable drop-off in solve rate after K = 10. As subagents run for ten turns, this drop-off point corresponds to the first parent decision, between resuming the first subagent and dispatching a new one. Dispatching a new subagent currently starts a new context to avoid possible strategy lock-in. However, previously in Section 4.1 we found that short-context subagents search more heavily, even when given direct advice and lemma names from the parent agent, which negatively impacted performance of the previous orchestrator. We analyze this by comparing the behavior of dispatched and resumed subagents after the first parent decision. We group parent decisions, and analyze the search and submit rates of resulting subagents. We find that resumed subagents succeed more often and average faster 56

Figure 4.3: Context-based orchestrator solve rate against unique tokens, plotted alongside Section 3.2 agent baseline, for gpt-5.4 and gpt-5.4-mini. Top: full 423-spec set. Bottom row, left to right: bignum, verified_cogen, and verina subsets.

57

Table 4.8: Behavioral comparison of round-2 dispatch and resume subagents (the parent’s decision turn after a failed initial dispatch) on the context-based orchestrator with gpt-5.4. The dispatch column reports dispatch_subagent calls, which run with an empty context. The resume column reports resume_endpoint calls, which run off the round-1 context. Metric n (round-2 cases) Round-2 solve rate Mean turns to terminate Mean search_mathlib calls Mean submit_code calls Mean search_mathlib calls per turn Mean submit_code calls per turn Search-to-submit ratio

Dispatch

Resume

95 17.9%

62 38.7%

7.8 15.1 1.9 1.95 0.24 8.1

4.1 2.3 2.7 0.55 0.64 0.8

termination, but this is expected as the parent is more likely to resume subagents closer to a proof. More notably, there is a significant difference in the ratio between searches and submits, with dispatched subagents again searching more than five times as often as resumed ones. We infer that the first context of ten turns is likely to be useful base information: initial reasoning, lemma searches, and reusable early submissions. Removing the base context requires the model to rederive this from scratch, even when given context of what to try next. The fix is to also have subagents branch off an explicit context endpoint. The parent may give a new direction synthesized from multiple endpoints, but previous information leading up to the endpoint is retained and available to build on. Previously, new subagents branched from the root, starting with only the parent advice. This change also allows more branching of contexts, allowing a tree of endpoints to take shape rather than independent lines of search. The parent is also explicitly advised in the prompt to resume from endpoints rather than start new branches from the root, though the option remains available.

58

4.2.5

Final Results

The final context-based orchestrator reaches 88.2% with GPT-5.4 and 54.8% with GPT5.4-mini at K = 50, a +6.4% and +4.9% lift over the previous design on the same grid. Figure 4.4 plots solve rate against average unique tokens per spec, and Table 4.9 reports per-subset solve rates across K. Table 4.10 repeats the round-2 behavioral comparison from Table 4.8 for the final orchestrator. The rate at which the parent chooses between dispatch and resume remains roughly similar. The resumed subagent’s success rate moderately increases, while dispatched subagents maintain a similar success rate as before. More notably, the search-to-submit ratio for dispatch drops over 50%, indicating a substantial shift in behavior: rather than searching mathlib from scratch, the subagent spends more of its turns on submissions because the source endpoint’s prior search results are already in context. The ratio remains higher than resume’s 0.6, which is expected, as dispatch asks the subagent to go in a different direction and a fraction of its turns are spent reorienting. Mean turns to termination also drops from 7.8 to 5.7, which improves the Pareto curve because successful specs no longer contribute tokens at higher rounds. Our final orchestrator design is competitive with the agent baseline through K = 20 on the combined 423-spec set, but solve rate slows past that point (Figure 4.4). The agent extended to K = 50 reaches a higher solve rate on every GPT-5.4 subset, while for GPT-5.4-mini, the orchestrator and agent remain within a couple of percentage points. The pattern varies in shape across subsets and models. On verified_cogen, the easiest subset, the GPT-5.4 orchestrator incurs extra tokens in the first few turns and solves specs slower than the agent, only closing the gap when they both plateau. On verina, the orchestrator stays close to the agent baseline at low K but shows a drop-off in solve rate at higher K. On the hardest benchmark, bignum, the orchestrator instead leads the agent through a significant portion of the token range, with the two curves crossing near 120k unique tokens per spec. At K = 50, the GPT-5.4 agent reaches 87.1% on bignum against 59

Table 4.9: Final orchestrator pass rate at varying LLM-call budgets K, for gpt-5.4 and gpt-5.4-mini. Each cell shows pass rate / average unique tokens per spec at that K. Subset

n

K=10

K=20

K=30

K=40

K=50

gpt-5.4 BigNum 62 22.6% / 38k 35.5% / 72k 51.6% / 101k 64.5% / 123k 72.6% / 141k VerifCogen 172 65.1% / 19k 86.6% / 26k 93.6% / 28k 93.6% / 29k 94.2% / 30k Verina 189 59.8% / 24k 76.2% / 35k 84.1% / 41k 85.7% / 46k 87.8% / 50k Combined 423 56.5% / 24k 74.5% / 37k 83.2% / 45k 85.8% / 50k 88.2% / 55k gpt-5.4-mini BigNum 62 16.1% / 35k 16.1% / 72k 17.7% / 113k 17.7% / 149k 17.7% / 179k 67.4% / 77k VerifCogen 172 46.5% / 19k 50.6% / 34k 58.1% / 50k 65.1% / 65k Verina 189 38.6% / 25k 44.4% / 44k 49.2% / 65k 52.9% / 85k 55.6% / 100k Combined 423 38.5% / 24k 42.8% / 44k 48.2% / 66k 52.7% / 86k 54.8% / 102k

the orchestrator’s 72.6%, roughly fifteen percentage points ahead. For GPT-5.4-mini, the orchestrator shows small gains over the agent on some subsets and falls slightly behind on others, staying within a couple of percentage points. We attribute this behavior to a tradeoff in intermediate parent reasoning. On specs that require a strategy search across distinct proof approaches, the parent’s ability to dispatch a new subagent with a different palette class lets it find a working approach faster than the agent’s single-context exploration. However, this hurts the orchestrator on specs that require deep iteration within a single approach, as every parent decision is a potential context switch that interrupts that iteration, and the agent’s unbroken trajectory through K = 50 converts more of these deep-iteration specs.

60

Figure 4.4: Final orchestrator solve rate against unique tokens, plotted alongside Section 4.2 context-based predecessor and Section 3.2 agent baseline, for gpt-5.4 and gpt-5.4-mini. Top: full 423-spec set. Bottom row, left to right: bignum, verified_cogen, and verina subsets.

61

Table 4.10: Behavioral comparison of round-2 dispatch and resume subagents (the parent’s decision turn after a failed initial dispatch) on the final orchestrator with gpt-5.4. dispatch_subagent typically branches from a non-root endpoint, so the dispatched subagent inherits the source endpoint’s prior message history along with the parent’s fresh advice. Metric n (round-2 cases) Round-2 solve rate Mean turns to terminate Mean search_mathlib calls Mean submit_code calls Mean search_mathlib calls per turn Mean submit_code calls per turn Search-to-submit ratio

62

Dispatch

Resume

100 18.0%

70 48.6%

5.7 7.0 1.8 1.23 0.33 3.8

3.5 1.3 2.4 0.39 0.68 0.6

Chapter 5 Conclusion We provide an updated evaluation for LLM-driven verified-code generation in Lean and devise search-based methods to improve verification performance. Benchmarking recent frontier and open-weight models against the existing vericoding-benchmark Lean harness, closed-source US models show little year-over-year movement without reasoning, while open-weight models slightly edge up. By replacing the original Vericoding harness with an agentic loop and incorporating mathlib search, solve rates significantly increase, scaling with additional LLM calls. GPT-5.4 hits 95.0% on the 423-spec subset at K = 50 LLM calls, nearly saturating the benchmark. On top of the agent loop we build two orchestrators: a state-based design that picks which partial-proof state to extend next, and a context-based design that picks which complete subagent context to fork from. We find that the benefit of search structure depends on the difficulty and width of the underlying problems. A broad but shallow search, like the state-based orchestrator, quickly closes a wide swath of easier specs that are helped with an initial planning turn, but struggles to build up persistent progress on harder specs. A context-aware tree search, like our final orchestrator design, is able to solve a range of more difficult problems that require strategies across distinct proof approaches, and does so faster than the agent baseline. The tradeoff is that intermediate parent decisions interrupt the deep iteration that the agent baseline uses

63

to crack the hardest specs, so the orchestrator closes those goals more slowly. A second observation is that vericoding-benchmark is likely saturated by recent frontier models. We evaluated on GPT-5.4 at medium reasoning, one generation behind the current flagship GPT-5.5, and not at xhigh, the maximum supported reasoning effort. Contamination of the benchmark is also a possibility: while GPT-5.4’s claimed knowledge cutoff of August 31, 2025 is before the release of vericoding-benchmark in September 2025, the model could have been exposed to the verification tasks in post-training pipelines. Future models are increasingly likely to have the benchmark tasks incorporated into training, especially as interest in improving formal verification capabilities remains high. More difficult formalverification benchmarks, ideally with specs drawn from recent human-written code, are needed both to cleanly separate algorithmic progress from model capabilities, and to serve as a concrete test for those developing formal verification algorithms. Real-world deployments of these systems also require different tradeoffs and considerations than the ones we make in this thesis. We idealize provider pricing by counting unique input + output tokens, without always using optimal caching strategies (such as handling tool schema changes), and assume perfect prompt caching with free cache reads. In practice, efficient harnesses may require more engineering and algorithmic considerations, and best practices for interfacing with model providers also change quickly. A complementary direction to our custom orchestrator implementation is building search and dispatch on top of existing agent harnesses, inheriting their tool ecosystems and optimizations. However, this comes at the cost of less control over the underlying context, and being tied to nuances and development changes of an existing system. In either case, the right design depends on the end user and the target application, not necessarily a single benchmark score. Formal verification continues to grow as an area of research, thanks in part to improving model capabilities that lower the cost of writing and checking proofs. In cybersecurity, mature verification tooling can harden existing codebases by formally ruling out vulnerabilities before the next exploit hits. For developing reliable agents, machine-checkable correctness provides

64

an automatic scaffold, lengthening the task horizon over which intermediate steps can be validated without a human in the loop. At a longer horizon, automated formal verification could be used to verify AI systems themselves, complementing mechanistic interpretability by guaranteeing how a model behaves as opposed to explaining its internal logic. Taken together, these problems make automatic formal verification a high-impact domain in the present and future, and one where continued algorithmic progress, alongside advances in tooling and testing, can deliver outsized returns.

65

66

References [1] Y. Bengio et al. “Managing extreme AI risks amid rapid progress.” Science, 384(6698), May 2024, pp. 842–845. issn: 1095-9203. doi: 10.1126/science.adn0117. url: http: //dx.doi.org/10.1126/science.adn0117. [2] T. Kwa et al. Measuring AI Ability to Complete Long Software Tasks. 2025. doi: 10.48550/ARXIV.2503.14499. url: https://arxiv.org/abs/2503.14499. [3] METR. Time Horizon 1.1. Model Evaluation & Threat Research, Jan. 2026. url: https://metr.org/blog/2026-1-29-time-horizon-1-1/ (visited on 05/04/2026). [4] METR. Task-Completion Time Horizons of Frontier AI Models. Live aggregation page; reports Claude Opus 4.6 at a 14h30m time horizon as of 2026-02-21. Model Evaluation & Threat Research, 2026. url: https://metr.org/time-horizons/ (visited on 05/04/2026). [5] D. Hendrycks, M. Mazeika, and T. Woodside. An Overview of Catastrophic AI Risks. 2023. doi: 10.48550/ARXIV.2306.12001. url: https://arxiv.org/abs/2306.12001. [6] Anthropic. Claude Mythos Preview System Card. Anthropic, Apr. 2026. url: https: //anthropic.com/claude-mythos-preview-system-card (visited on 05/04/2026). [7] OpenAI. GPT-5.5 System Card. OpenAI, Apr. 2026. url: https://openai.com/index/ gpt-5-5-system-card/ (visited on 05/04/2026). [8] C. Meske, T. Hermanns, E. von der Weiden, K.-U. Loser, and T. Berger. Vibe Coding as a Reconfiguration of Intent Mediation in Software Development: Definition, Implications,

67

and Research Agenda. 2025. doi: 10.48550/ARXIV.2507.21928. url: https://arxiv.org/ abs/2507.21928. [9] H. Pearce, B. Ahmad, B. Tan, B. Dolan-Gavitt, and R. Karri. “Asleep at the Keyboard? Assessing the Security of GitHub Copilot’s Code Contributions.” In: 2022 IEEE Symposium on Security and Privacy (SP). IEEE, May 2022, pp. 754–768. doi: 10.1109/sp46214.2022.9833571. url: http://dx.doi.org/10.1109/SP46214.2022.9833571. [10] D. Blain and M. Noiseux. Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code. 2026. doi: 10.48550/ARXIV.2604.05292. url: https://arxiv.org/abs/2604.05292. [11] L. d. Moura and S. Ullrich. “The Lean 4 Theorem Prover and Programming Language.” In: Automated Deduction – CADE 28. Springer International Publishing, 2021, pp. 625– 635. isbn: 9783030798765. doi: 10.1007/978-3-030-79876-5_37. url: http://dx.doi. org/10.1007/978-3-030-79876-5_37. [12] K. Zheng, J. M. Han, and S. Polu. MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics. 2021. doi: 10.48550/ARXIV.2109.00110. url: https: //arxiv.org/abs/2109.00110. [13] G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaudhuri. PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition. 2024. doi: 10 . 48550 / ARXIV . 2407 . 11214. url: https : //arxiv.org/abs/2407.11214. [14] T. Hubert et al. “Olympiad-level formal mathematical reasoning with reinforcement learning.” Nature, 651(8106), Nov. 2025, pp. 607–613. issn: 1476-4687. doi: 10.1038/ s41586-025-09833-y. url: http://dx.doi.org/10.1038/s41586-025-09833-y. [15] J.-K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche. “HACL*: A Verified Modern Cryptographic Library.” In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. CCS ’17. ACM, Oct. 2017, 68

pp. 1789–1806. doi: 10.1145/3133956.3134043. url: http://dx.doi.org/10.1145/ 3133956.3134043. [16] G. Klein et al. “seL4: formal verification of an OS kernel.” In: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. SOSP09. ACM, Oct. 2009, pp. 207–220. doi: 10.1145/1629575.1629596. url: http://dx.doi.org/10.1145/1629575. 1629596. [17] X. Leroy. “A Formally Verified Compiler Back-end.” Journal of Automated Reasoning, 43(4), Nov. 2009, pp. 363–446. issn: 1573-0670. doi: 10.1007/s10817-009-9155-4. url: http://dx.doi.org/10.1007/s10817-009-9155-4. [18] S. Polu, J. M. Han, K. Zheng, M. Baksys, I. Babuschkin, and I. Sutskever. Formal Mathematics Statement Curriculum Learning. 2022. doi: 10.48550/ARXIV.2202.01344. url: https://arxiv.org/abs/2202.01344. [19] S. Varambally, T. Voice, Y. Sun, Z. Chen, R. Yu, and K. Ye. Hilbert: Recursively Building Formal Proofs with Informal Reasoning. 2025. doi: 10.48550/ARXIV.2509.22819. url: https://arxiv.org/abs/2509.22819. [20] G. Lample, M.-A. Lachaux, T. Lavril, X. Martinet, A. Hayat, G. Ebner, A. Rodriguez, and T. Lacroix. HyperTree Proof Search for Neural Theorem Proving. 2022. doi: 10.48550/ARXIV.2205.11491. url: https://arxiv.org/abs/2205.11491. [21] A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, L. Kaiser, and I. Polosukhin. Attention Is All You Need. 2017. doi: 10.48550/ARXIV.1706.03762. url: https://arxiv.org/abs/1706.03762. [22] T. B. Brown et al. Language Models are Few-Shot Learners. 2020. doi: 10.48550/ ARXIV.2005.14165. url: https://arxiv.org/abs/2005.14165. [23] J. Kaplan, S. McCandlish, T. Henighan, T. B. Brown, B. Chess, R. Child, S. Gray, A. Radford, J. Wu, and D. Amodei. Scaling Laws for Neural Language Models. 2020. doi: 10.48550/ARXIV.2001.08361. url: https://arxiv.org/abs/2001.08361. 69

[24] J. Hoffmann et al. Training Compute-Optimal Large Language Models. 2022. doi: 10.48550/ARXIV.2203.15556. url: https://arxiv.org/abs/2203.15556. [25] P. Christiano, J. Leike, T. B. Brown, M. Martic, S. Legg, and D. Amodei. Deep reinforcement learning from human preferences. 2017. doi: 10.48550/ARXIV.1706.03741. url: https://arxiv.org/abs/1706.03741. [26] L. Ouyang et al. Training language models to follow instructions with human feedback. 2022. doi: 10.48550/ARXIV.2203.02155. url: https://arxiv.org/abs/2203.02155. [27] Y. Bai et al. Constitutional AI: Harmlessness from AI Feedback. 2022. doi: 10.48550/ ARXIV.2212.08073. url: https://arxiv.org/abs/2212.08073. [28] R. Rafailov, A. Sharma, E. Mitchell, S. Ermon, C. D. Manning, and C. Finn. Direct Preference Optimization: Your Language Model is Secretly a Reward Model. 2023. doi: 10.48550/ARXIV.2305.18290. url: https://arxiv.org/abs/2305.18290. [29] J. Wei, X. Wang, D. Schuurmans, M. Bosma, B. Ichter, F. Xia, E. Chi, Q. Le, and D. Zhou. Chain-of-Thought Prompting Elicits Reasoning in Large Language Models. 2022. doi: 10.48550/ARXIV.2201.11903. url: https://arxiv.org/abs/2201.11903. [30] DeepSeek-AI et al. DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning. 2025. doi: 10.48550/ARXIV.2501.12948. url: https://arxiv. org/abs/2501.12948. [31] OpenAI. OpenAI o1 System Card. OpenAI, Dec. 2024. url: https://openai.com/index/ openai-o1-system-card/ (visited on 05/04/2026). [32] S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y. Cao. ReAct: Synergizing Reasoning and Acting in Language Models. 2022. doi: 10.48550/ARXIV. 2210.03629. url: https://arxiv.org/abs/2210.03629. [33] T. Schick, J. Dwivedi-Yu, R. Dessì, R. Raileanu, M. Lomeli, L. Zettlemoyer, N. Cancedda, and T. Scialom. Toolformer: Language Models Can Teach Themselves to Use Tools. 2023. doi: 10.48550/ARXIV.2302.04761. url: https://arxiv.org/abs/2302.04761. 70

[34] Anthropic. Introducing the Model Context Protocol. Anthropic, Nov. 2024. url: https: //www.anthropic.com/news/model-context-protocol (visited on 05/04/2026). [35] Anthropic. Donating the Model Context Protocol and establishing the Agentic AI Foundation. Anthropic, Dec. 2025. url: https://www.anthropic.com/news/donatingthe-model-context-protocol-and-establishing-of-the-agentic-ai-foundation (visited on 05/04/2026). [36] Anthropic. Claude Code: Anthropic’s agentic coding system. Anthropic, 2025. url: https://www.anthropic.com/product/claude-code (visited on 05/04/2026). [37] OpenAI. Codex: AI Coding Partner from OpenAI. OpenAI, 2025. url: https://openai. com/codex/ (visited on 05/05/2026). [38] Anomaly. OpenCode: The open source AI coding agent. Anomaly, 2025. url: https: //opencode.ai/ (visited on 05/05/2026). [39] R. Milner. Logic for Computable Functions: Description of a Machine Implementation. Tech. rep. STAN-CS-72-288. Stanford University, Department of Computer Science, May 1972. url: http://i.stanford.edu/pub/cstr/reports/cs/tr/72/288/CS-TR-72-288.pdf (visited on 05/04/2026). [40] M. J. Gordon, A. J. Milner, and C. P. Wadsworth. Edinburgh LCF. Springer Berlin Heidelberg, 1979. isbn: 9783540385264. doi: 10 . 1007 / 3 - 540 - 09724 - 4. url: http : //dx.doi.org/10.1007/3-540-09724-4. [41] T. Coquand and C. Paulin. “Inductively defined types.” In: COLOG-88. Springer Berlin Heidelberg, 1990, pp. 50–66. isbn: 9783540469636. doi: 10.1007/3-540-52335-9_47. url: http://dx.doi.org/10.1007/3-540-52335-9_47. [42] G. Gonthier. “Formal Proof—The Four-Color Theorem.” Notices of the American Mathematical Society, 55(11), 2008, pp. 1382–1393. url: https://www.ams.org/notices/ 200811/tx081101382p.pdf (visited on 05/04/2026).

71

[43] G. Gonthier et al. “A Machine-Checked Proof of the Odd Order Theorem.” In: Interactive Theorem Proving. Springer Berlin Heidelberg, 2013, pp. 163–179. isbn: 9783642396342. doi: 10.1007/978-3-642-39634-2_14. url: http://dx.doi.org/10.1007/978-3-642-396342_14. [44] Isabelle/HOL. Springer Berlin Heidelberg, 2002. isbn: 9783540459491. doi: 10.1007/3540-45949-9. url: http://dx.doi.org/10.1007/3-540-45949-9. [45] Archive of Formal Proofs contributors. Archive of Formal Proofs. AFP requests entrylevel citations for specific proofs; this cite refers to the archive as a whole. Archive of Formal Proofs, 2026. url: https://www.isa-afp.org/ (visited on 05/04/2026). [46] U. Norell. “Towards a practical programming language based on dependent type theory.” PhD thesis. Göteborg, Sweden: Chalmers University of Technology, Sept. 2007. url: https://research.chalmers.se/en/publication/46311 (visited on 05/04/2026). [47] L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. “The Lean Theorem Prover (System Description).” In: Automated Deduction - CADE-25. Springer International Publishing, 2015, pp. 378–388. isbn: 9783319214016. doi: 10.1007/978-3319-21401-6_26. url: http://dx.doi.org/10.1007/978-3-319-21401-6_26. [48] G. Ebner, S. Ullrich, J. Roesch, J. Avigad, and L. de Moura. “A metaprogramming framework for formal verification.” Proceedings of the ACM on Programming Languages, 1(ICFP), Aug. 2017, pp. 1–29. issn: 2475-1421. doi: 10.1145/3110278. url: http: //dx.doi.org/10.1145/3110278. [49] T. mathlib Community. “The lean mathematical library.” In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. POPL ’20. ACM, Jan. 2020, pp. 367–381. doi: 10.1145/3372885.3373824. url: http://dx.doi. org/10.1145/3372885.3373824. [50] Lean Prover Community. Liquid Tensor Experiment. Lean formalization of the main theorem of liquid vector spaces, completed July 2022 in response to Peter Scholze’s 72

challenge. GitHub, 2022. url: https://github.com/leanprover-community/lean-liquid (visited on 05/04/2026). [51] T. Tao and PFR formalization contributors. The Polynomial Freiman–Ruzsa Conjecture: A digitisation of the proof in Lean 4. 2023. url: https://teorth.github.io/pfr/ (visited on 05/04/2026). [52] J. Limperg and A. H. From. “Aesop: White-Box Best-First Proof Search for Lean.” In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP ’23. ACM, Jan. 2023, pp. 253–266. doi: 10.1145/3573105.3575671. url: http://dx.doi.org/10.1145/3573105.3575671. [53] O. Dressler. Lean LSP MCP: Tools for agentic interaction with the Lean theorem prover. Mar. 2025. url: https://github.com/oOo0oOo/lean-lsp-mcp (visited on 05/04/2026). [54] S. Ho and J. Protzenko. “Aeneas: Rust verification by functional translation.” Proceedings of the ACM on Programming Languages, 6(ICFP), Aug. 2022, pp. 711–741. issn: 24751421. doi: 10.1145/3547647. url: http://dx.doi.org/10.1145/3547647. [55] Lean FRO. Aeneas: Bridging Rust to Lean for Formal Verification. Lean Language, 2025. url: https://lean-lang.org/use-cases/aeneas/ (visited on 05/04/2026). [56] D. Tuma and N. Hopper. VCVio: A Formally Verified Forking Lemma and Fiat-Shamir Transform, via a Flexible and Expressive Oracle Representation. Cryptology ePrint Archive, Paper 2024/1819. Nov. 2024. url: https://eprint.iacr.org/2024/1819 (visited on 05/04/2026). [57] K. R. M. Leino. “Dafny: An Automatic Program Verifier for Functional Correctness.” In: Logic for Programming, Artificial Intelligence, and Reasoning. Springer Berlin Heidelberg, 2010, pp. 348–370. isbn: 9783642175114. doi: 10.1007/978-3-642-175114_20. url: http://dx.doi.org/10.1007/978-3-642-17511-4_20.

73

[58] C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. Setty, and B. Zill. “IronFleet: proving practical distributed systems correct.” In: Proceedings of the 25th Symposium on Operating Systems Principles. SOSP ’15. ACM, Oct. 2015, pp. 1– 17. doi: 10.1145/2815400.2815428. url: http://dx.doi.org/10.1145/2815400.2815428. [59] T. Hance, A. Lattuada, C. Hawblitzel, J. Howell, R. Johnson, and B. Parno. “Storage Systems are Distributed Systems (So Verify Them That Way!)” In: 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, Nov. 2020, pp. 99–115. isbn: 978-1-939133-19-9. url: https://www.usenix. org/conference/osdi20/presentation/hance (visited on 05/04/2026). [60] N. Swamy et al. “Dependent types and multi-monadic effects in F*.” In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’16. ACM, Jan. 2016, pp. 256–270. doi: 10.1145/2837614.2837655. url: http://dx.doi.org/10.1145/2837614.2837655. [61] Cryspen. libcrux: The formally verified crypto library for Rust. GitHub, 2024. url: https://github.com/cryspen/libcrux (visited on 05/04/2026). [62] A. Lattuada, T. Hance, C. Cho, M. Brun, I. Subasinghe, Y. Zhou, J. Howell, B. Parno, and C. Hawblitzel. “Verus: Verifying Rust Programs using Linear Ghost Types.” Proceedings of the ACM on Programming Languages, 7(OOPSLA1), Apr. 2023, pp. 286– 315. issn: 2475-1421. doi: 10.1145/3586037. url: http://dx.doi.org/10.1145/3586037. [63] P. Singh, J. Gancher, and B. Parno. OwlC: Compiling Security Protocols to Verified, Secure, High-Performance Libraries. Cryptology ePrint Archive, Paper 2025/1092. June 2025. url: https://eprint.iacr.org/2025/1092 (visited on 05/04/2026). [64] Beneficial AI Foundation. dalek-lite: A pure-Rust implementation of group operations on Ristretto and Curve25519. Verus proofs over a fork of curve25519-dalek. GitHub, 2025. url: https : / / github . com / Beneficial - AI - Foundation / dalek - lite (visited on 05/04/2026). 74

[65] S. Polu and I. Sutskever. Generative Language Modeling for Automated Theorem Proving. 2020. doi: 10.48550/ARXIV.2009.03393. url: https://arxiv.org/abs/2009.03393. [66] J. M. Han, J. Rute, Y. Wu, E. W. Ayers, and S. Polu. Proof Artifact Co-training for Theorem Proving with Language Models. 2021. doi: 10.48550/ARXIV.2102.06203. url: https://arxiv.org/abs/2102.06203. [67] K. Yang, A. M. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anandkumar. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. 2023. doi: 10.48550/ARXIV.2306.15626. url: https://arxiv.org/abs/2306.15626. [68] L. Aniva, C. Sun, B. Miranda, C. Barrett, and S. Koyejo. Pantograph: A Machine-toMachine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4. 2024. doi: 10.48550/ARXIV.2410.16429. url: https: //arxiv.org/abs/2410.16429. [69] A. Poiroux, V. Kuncak, and A. Bosselut. LeanInteract: A Python Interface for Lean 4. 2025. url: https://github.com/augustepoiroux/LeanInteract (visited on 05/04/2026). [70] S. Welleck and R. Saha. LLMSTEP: LLM proofstep suggestions in Lean. 2023. doi: 10.48550/ARXIV.2310.18457. url: https://arxiv.org/abs/2310.18457. [71] P. Song, K. Yang, and A. Anandkumar. Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean. 2024. doi: 10.48550/ARXIV.2404.12534. url: https://arxiv.org/abs/2404.12534. [72] H. Wang et al. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning. 2025. doi: 10.48550/ARXIV.2504.11354. url: https: //arxiv.org/abs/2504.11354. [73] Z. Z. Ren et al. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition. 2025. doi: 10.48550/ARXIV.2504. 21801. url: https://arxiv.org/abs/2504.21801.

75

[74] Y. Lin et al. Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction. 2025. doi: 10.48550/ARXIV.2508.03613. url: https://arxiv.org/abs/2508.03613. [75] R. Xin, C. Xi, J. Yang, F. Chen, H. Wu, X. Xiao, Y. Sun, S. Zheng, and K. Shen. BFSProver: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving. 2025. doi: 10.48550/ARXIV.2502.03438. url: https://arxiv.org/abs/2502.03438. [76] R. Xin, Z. Zheng, Y. Nie, K. Yuan, and X. Xiao. Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers. 2025. doi: 10.48550/ARXIV.2509.06493. url: https://arxiv.org/abs/2509.06493. [77] A. Thakur, G. Tsoukalas, Y. Wen, J. Xin, and S. Chaudhuri. An In-Context Learning Agent for Formal Theorem-Proving. 2023. doi: 10.48550/ARXIV.2310.04353. url: https://arxiv.org/abs/2310.04353. [78] B. Breen, M. Del Tredici, J. McCarran, J. A. Mijares, W. W. Yin, K. Sulimany, J. M. Taylor, F. H. L. Koppens, and D. Englund. Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics. 2025. doi: 10.48550/ARXIV.2510.12787. url: https://arxiv.org/abs/2510.12787. [79] J. Liu et al. Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics. 2026. doi: 10.48550/ARXIV.2601.14027. url: https://arxiv.org/ abs/2601.14027. [80] Y. Zhou et al. Solving Formal Math Problems by Decomposition and Iterative Reflection. 2025. doi: 10.48550/ARXIV.2507.15225. url: https://arxiv.org/abs/2507.15225. [81] R. Qiu, Y. Cao, J. Liu, D. Guo, X.-S. Gao, L. Zhi, and R. Feng. Mechanic: SorrifierDriven Formal Decomposition Workflow for Automated Theorem Proving. 2026. doi: 10.48550/ARXIV.2603.24465. url: https://arxiv.org/abs/2603.24465. [82] T. Achim et al. Aristotle: IMO-level Automated Theorem Proving. 2025. doi: 10.48550/ ARXIV.2510.01346. url: https://arxiv.org/abs/2510.01346. 76

[83] A. Ospanov, F. Farnia, and R. Yousefzadeh. APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning. 2025. doi: 10.48550/ARXIV.2505.05758. url: https://arxiv.org/abs/2505.05758. [84] Z. Shen et al. REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning. 2025. doi: 10.48550/ARXIV.2505.20613. url: https://arxiv.org/abs/2505. 20613. [85] T. Yang, M. Yan, H. Zhao, and T. Yang. LemmaHead: RAG Assisted Proof Generation Using Large Language Models. 2025. doi: 10.48550/ARXIV.2501.15797. url: https: //arxiv.org/abs/2501.15797. [86] Numina and Kimi Team. Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models. Hugging Face Blog, July 2025. url: https://huggingface.co/blog/AIMO/kimina-prover (visited on 05/04/2026). [87] C. Loughridge, Q. Sun, S. Ahrenbach, F. Cassano, C. Sun, Y. Sheng, A. Mudide, M. R. H. Misu, N. Amin, and M. Tegmark. DafnyBench: A Benchmark for Formal Software Verification. 2024. doi: 10.48550/ARXIV.2406.08467. url: https://arxiv.org/ abs/2406.08467. [88] S. Bursuc et al. A benchmark for vericoding: formally verified program synthesis. 2025. doi: 10.48550/ARXIV.2509.22908. url: https://arxiv.org/abs/2509.22908. [89] Z. Ye, Z. Yan, J. He, T. Kasriel, K. Yang, and D. Song. VERINA: Benchmarking Verifiable Code Generation. 2025. doi: 10 . 48550 / ARXIV . 2505 . 23135. url: https : //arxiv.org/abs/2505.23135. [90] JetBrains-Research. Verified code benches. JetBrains Research, 2025. url: https:// github . com / JetBrains - Research / verified - cogen / tree / main / benches (visited on 05/20/2026). [91] A. Yang et al. Qwen3 Technical Report. 2025. doi: 10.48550/ARXIV.2505.09388. url: https://arxiv.org/abs/2505.09388. 77

[92] B. Brown, J. Juravsky, R. Ehrlich, R. Clark, Q. V. Le, C. Ré, and A. Mirhoseini. Large Language Monkeys: Scaling Inference Compute with Repeated Sampling. 2024. doi: 10.48550/ARXIV.2407.21787. url: https://arxiv.org/abs/2407.21787. [93] M. Zhang, O. Press, W. Merrill, A. Liu, and N. A. Smith. How Language Model Hallucinations Can Snowball. 2023. doi: 10.48550/ARXIV.2305.13534. url: https: //arxiv.org/abs/2305.13534. [94] J. Lou and Y. Sun. Anchoring Bias in Large Language Models: An Experimental Study. 2024. doi: 10.48550/ARXIV.2412.06593. url: https://arxiv.org/abs/2412.06593.

78

Related documents

• The Complexity Kink: A Prompt-Side Structural Complexity Index for Code-Generation Reliability#978496
• Semantic Layer Induction from Raw Telemetry via Hierarchical LLM and RAG Abstraction#978497
• The Output-Space Hypothesis: Enumerative Equivalence Checking for Tensor Programs#978498
• DeltaSelect: Affordable A/B Testing for Coding Agents#978499
• Code-as-Auditor: Executable Compliance Reasoning via Regulation-to-Code#978500