# daVinci-Prover: Agent-Native Mid-Training for Formal Theorem Proving

> daVinci-Prover's 33.7B-token mid-training corpus, combining skill priors with agent-native trajectories, boosts theorem-proving pass@1 by 13.7 points over SFT baselines.

- **Source:** [arXiv](https://arxiv.org/abs/2611.16433)
- **Published:** 2026-11-14
- **Permalink:** https://picx.dev/p/FPHs2t
- **Whiteboard:** https://picx.dev/p/FPHs2t/image

## Summary

## Summary (Overview)

- **Core contribution**: Introduces **daVinci-Prover**, a family of formal theorem-proving models trained on a novel **agent-native mid-training corpus** (33.7B tokens) that combines mathematical skill priors with environment-native agent trajectories, plus a lightweight prover harness for collecting high-quality SFT data.
- **Key finding**: Mid-training improves Qwen3-8B pass@1 by an average of **13.7 points** over the matched Base + SFT baseline across MiniF2F, FATE-M, and ProofNet, with consistent gains on Qwen3.5-9B and Qwen3.5-35B-A3B models.
- **Harness design**: The daVinci-Prover harness enables iterative edit–check–revise loops with Lean4, supporting 7 tools, isolated workspaces, and verifier-grounded feedback; it collects ~36K high-quality agent trajectories for SFT.
- **Data ablation**: Agent-native trajectories ($\mathcal{D}_{agent}$, 8.4B tokens) yield larger gains than skill-prior data ($\mathcal{D}_{skill}$, 25.3B tokens) alone, but the two are complementary—combining them gives the best performance.
- **Memory compaction**: A model-free trajectory compression method yields near-saturating MiniF2F performance (97.1 pass@1) and dramatic gains on FATE-H (42.0 for 35B model vs. 16.3 without compaction).

---

## Introduction and Theoretical Foundation

Formal theorem proving converts mathematical statements and proofs into machine-checkable computational objects. Lean proof assistants offer an attractive interface for LLMs because they combine mathematical reasoning trajectories with verifiable feedback. The paper identifies **three paradigms** of LLM-based provers:

1. **Whole-proof generation**: Complete proofs in a single pass (e.g., DeepSeek-Prover, Goedel Prover).
2. **Agentic proving**: Model interacts with an executable environment, inspects workspaces, queries libraries, runs Lean, interprets verifier feedback, and iteratively revises proofs.
3. **Orchestrated systems**: Multiple components coordinated in structured workflows (e.g., Seed-Prover 1.5, Hilbert).

The authors argue that existing formal-reasoning corpora are dominated by **whole-proof trajectories**, which fail to expose essential proving behaviors such as:
- Decomposing goals into sub-theorems
- Exploring alternative proof steps
- Verifying intermediate reasoning
- Localizing and repairing failures

**Key theoretical insight**: These capabilities should be injected into **mid-training data** as reusable mathematical skill priors (not left to post-training). Additionally, agentic provers require **agent-native trajectories** that capture authentic interactions with Lean—including proof states, verifier feedback, and failed attempts—to reduce the distribution gap between static training and interactive inference.

---

## Methodology

### 3.1 Theorem-Proving Skill Priors ($\mathcal{D}_{skill}$)

Four types of trajectories are constructed:

**(a) Decomposition and Assembly Trajectories**: A teacher LLM receives a Lean theorem + verified reference proof and generates:
- A natural-language proof plan
- Auxiliary lemmas with dependency information
- A complete assembled Lean proof

**(b) Verified Subgoal Search Data**: Replaying verified proofs to extract intermediate states, then:
- A proposal model generates diverse tactics
- Tactics are combined with reference tactics, anonymized, shuffled, and executed independently
- Retain successful closures, accepted open states, and Lean errors (exclude timeouts)

**(c) Revision Trajectories**: Structured diagnosis with four fields:
- **location**: affected lemma/proof step
- **symptom**: observed failure
- **cause**: underlying issue
- **fix**: targeted correction

**(d) Informal Reasoning and Verification Trajectories**: From Nemotron-Math-Proofs-v2, covering proof generation with self-evaluation, proof verification, and meta-verification.

### 3.2 daVinci-Prover Harness

The harness formulates proving as an iterative **edit–check–revise loop**:
- Input theorem copied into `scratch/solution.lean`
- 7 tools available (edit candidates, inspect files, retrieve Lean declarations, run focused checks)
- Writable `scratch/` directory for proof candidates; read-only `target/` for Lean/Mathlib project
- Every edit triggers verification; draft checks expose local goals; placeholder-free candidates undergo strict verification
- Episode terminates only when a candidate passes strict Lean verification AND declaration/type match the original theorem

### 3.3 Final Dataset: daVinci-Prover 33.7B Collection

**Data sources**: NuminaMath-LEAN, AoPS, Lean Workbook, Goedel LM/SFT dataset v2, OProofs. Contamination filtering removes 0.03427% of tokens overlapping with evaluation benchmarks.

**Data replay**: Parent examples (logical trajectories before 32K chunking) are assigned replay budgets; high-quality parents selected with source-specific scores.

**Corpus composition**:

| Category | # Samples (M) | # Toks. (B) | Share (%) |
|---|---|---|---|
| Pre-Replay Data | 8.131 | 28.6 | 84.8 |
| Self-verification | 0.083 | 5.70 | 16.9 |
| Theorem Decomposition | 4.662 | 8.43 | 25.0 |
| Proof Revision | 1.027 | 3.84 | 11.4 |
| Proof Search | 1.962 | 3.45 | 10.2 |
| Environment-Aware Agent Trajectories | 0.397 | 7.17 | 21.3 |
| Replay Data | 1.454 | 5.11 | 15.2 |
| **Total** | **9.585** | **33.70** | **100.0** |

### 4 Supervised Fine-Tuning

- **Data source**: Harness rollouts on Goedel-LM/RL dataset V2 (~99K problems), limited to 30 turns / 200 tool calls, collected with DeepSeek-V4-Flash-0731.
- **~36K high-quality trajectories** spanning algebra, number theory, geometry, analysis, combinatorics, topology, probability, linear algebra, abstract algebra, logic.
- Filtering: remove low-quality trajectories (excessive repetition, unnecessary tool calls, <5 turns), retain only those fitting 144K-token context.

---

## Empirical Validation / Results

### Benchmark Performance (pass@8, daVinci-Prover harness)

| Model | #Params | MathOlympiad | MiniF2F | ProofNet | ProverBench | Putnam |
|---|---|---|---|---|---|---|
| DeepSeek-V4-Flash-0731 | 284B-A13B | **52.2** | **95.9** | **56.5** | **68.9** | **39.7** |
| Qwen3.5-9B-Base + SFT | 9B | 32.3 | 92.6 | 51.1 | 66.2 | 22.3 |
| Qwen3.5-9B-Midtrain + SFT | 9B | 35.3 | 93.9 | 52.7 | 66.5 | 24.9 |
| Qwen3.5-35B-Base + SFT | 35B-A3B | 35.8 | 93.0 | 52.7 | 66.5 | 24.3 |
| Qwen3.5-35B-Midtrain + SFT | 35B-A3B | 36.1 | 94.3 | 53.8 | 67.1 | 26.5 |

### Harness Effectiveness (pass@1, 3 runs)

| Model | MiniF2F | FATE-M | FATE-H | Putnam |
|---|---|---|---|---|
| Qwen3.6-35B-A3B | 68.0 | 48.7 | 4.0 | 3.0 |
| Qwen3.6-35B-A3B (w/ ret.) | 73.0 | 57.3 | 5.0 | 3.4 |
| DeepSeek-V4-Flash | 90.2 | 94.7 | 19.0 | 18.9 |
| DeepSeek-V4-Flash (w/ ret.) | 91.3 | 99.3 | 29.0 | 22.8 |

Retrieval tool consistently improves performance, especially on harder benchmarks (FATE-H, Putnam).

### Data Component Ablation (Qwen3.5-9B)

| Component | Tokens | MiniF2F | FATE-M | ProofNet |
|---|---|---|---|---|
| Qwen3.5-9B Base | - | 87.4 | 88.4 | 42.9 |
| $\mathcal{D}_{skill}$ | 25.3B | 87.8 | 89.8 | 43.6 |
| $\mathcal{D}_{agent}$ | 8.4B | 88.8 | 92.2 | 43.5 |
| $\mathcal{D}_{skill} + \mathcal{D}_{agent}$ | 33.7B | **90.1** | **93.3** | **44.5** |

### Comparison with Existing Corpora (Qwen3-8B)

| Data component | MiniF2F | FATE-M | ProofNet |
|---|---|---|---|
| Qwen3-8B-Base + SFT | 73.4 | 68.0 | 28.4 |
| Oprover-8B-Base + SFT | 80.3 | 73.1 | 30.3 |
| Qwen3-Base + Midtrain (ours) + SFT | **85.3** | **85.3** | **40.4** |

### Memory Compaction Effect (pass@1, 3 runs)

| Model | MiniF2F | FATE-M | FATE-H |
|---|---|---|---|
| **w/o memory compact** | | | |
| Qwen3.5-midtrain-9B | 90.1 | 93.3 | 16.7 |
| Qwen3.5-midtrain-35B | 90.1 | 93.7 | 16.3 |
| **w/ memory compact** | | | |
| Qwen3.5-midtrain-9B | **97.1** | 96.7 | 28.0 |
| Qwen3.5-midtrain-35B | **97.1** | **97.3** | **42.0** |

### Other Key Findings

- **Scaling**: Performance follows an approximately **log-linear trend** with mid-training data volume; most gains achieved within first 15B tokens (3.96 and 11.11 points over base on MiniF2F and FATE-M).
- **Training dynamics**: Mid-trained checkpoints start SFT with lower loss and remain better aligned; after one epoch, mid-training improves avg@5 by 5.33 (9B) and 5.08 (35B) points, matching base model's epoch-5 pass@5.
- **Agent behavior**: Mid-trained models show earlier file construction, more auxiliary-check passing (11.8%→12.7% at 9B; 12.6%→13.4% at 35B), and more decomposition on hard problems.

---

## Theoretical and Practical Implications

1. **Distribution alignment matters**: Agent-native trajectories ($\mathcal{D}_{agent}$) provide larger gains per token than skill priors ($\mathcal{D}_{skill}$) because they bridge the gap between static next-token training and interactive proving—models learn the same interaction primitives encountered at inference time.

2. **Complementarity of supervision**: Skill priors (decomposition, search, diagnosis, self-verification) and agent-native trajectories are *not substitutable*—combining them consistently outperforms either alone. Effective proving requires both *knowing how to reason about a proof* and *knowing how to realize that reasoning through environment interaction*.

3. **Mid-training as foundation**: Mid-training provides a stronger initialization for downstream SFT, enabling faster adaptation and better final performance. The 9B midtrain model even surpasses the 35B-A3B base model on MiniF2F, suggesting gains come from mid-training rather than model scale.

4. **Context management is critical**: Memory compaction dramatically improves long-horizon proving (FATE-H: 16.7→28.0 for 9B; 16.3→42.0 for 35B), suggesting that effective context management can better expose the capacity of larger models.

5. **Data composition > data scale**: Our 33B-token corpus outperforms Oprover's 65B-token corpus, demonstrating that targeted composition (skill priors + agent trajectories) is more effective than sheer volume.

---

## Conclusion

The paper introduces **daVinci-Prover**, combining agent-native mid-training with verifier-grounded supervised fine-tuning for interactive theorem proving. Key takeaways:

- A 33.7B-token mid-training corpus covering decomposition, search, self-verification, revision, and environment-native agent trajectories provides a strong foundation for theorem-proving agents.
- The lightweight daVinci-Prover harness effectively collects ~36K high-quality agent trajectories that transfer proving behavior to smaller models.
- Mid-training consistently improves performance over SFT-only baselines across multiple model families and benchmarks, with ablations confirming the complementary roles of mathematical skill priors and agent-native trajectories.
- Memory compaction enables near-saturating MiniF2F performance and substantial gains on challenging benchmarks.

**Future directions** implied by the work include: further scaling mid-training data, exploring reinforcement learning on top of the mid-trained initialization, and extending the approach to other proof assistants or interactive reasoning domains. All data, models, harness, and training infrastructure will be open-sourced for reproducibility.

---

_Markdown view of https://picx.dev/p/FPHs2t, served by PicX — AI-generated visual whiteboard summaries of research papers._