Research map / Large language models / Agents, code and math
3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes 3D-Prover, which learns tactic embeddings from synthetic proof-attempt transitions and uses k-DPP filtering to select diverse, high-quality tactics for Lean theorem proving with ReProver and InternLM2.5-Step-Prover.
Problem
Automated theorem proving search explodes exponentially with proof depth because many candidate tactics are semantically redundant or fail with execution errors, wasting expensive prover resources.
Approach
Train a transition model (encoder-predictor-decoder) on synthetic data from prior proof attempts to produce semantically aware tactic embeddings predicting error status, execution time, and output; then filter candidate tactics with a k-DPP using these embeddings as diversity features and predicted success/time-weighted logits as quality scores, before execution.
Key results
- On miniF2F-test with ReProver at K=8, 3D-Prover reaches 24.4% Pass@1 versus 22.4% for Top-K (+8.9% relative).
- On miniF2F-test with InternLM2.5-Step-Prover (BFS, K=8), 3D-Prover achieves 45.7% Pass@1 versus 44.3% for Top-K (+3.2%).
- Tactic success rate per node on miniF2F-valid at K=8 rises from 39.0% (Top-K) to 56.5% with lambda_s=0.5, versus 27.7% with no filtering.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| filter candidate tactics with 3D-Prover instead of selecting Top-K | ReProver · miniF2F-test Pass@1, K=8 | Pass@1: 22.4 -> 24.4 | Helped |
| filter candidate tactics with 3D-Prover instead of selecting Top-K | ReProver · miniF2F-valid Pass@1, K=16 | Pass@1: 26.6 -> 29.1 | Helped |
| filter candidate tactics with 3D-Prover instead of Top-K | InternLM2.5-Step-Prover with BFS · miniF2F-test Pass@2, K=8 | Pass@2: 44.9 -> 47.3 | Helped |
| filter candidate tactics with 3D-Prover instead of no filtering | InternLM2.5-Step-Prover with Critic Guided search · miniF2F-test Pass@6 | Pass@6: 49.0 -> 53.1 | Helped |
| use transition-model embeddings instead of tactic-reconstruction autoencoder embeddings (ablation) | 3D-Prover with ReProver · miniF2F-valid Pass@1, K=8 | Pass@1: 23.0 -> 25.0 | Helped |
| use transition-model embeddings instead of tactic-reconstruction autoencoder embeddings (ablation) | 3D-Prover with ReProver · miniF2F-valid Pass@1, K=16 | Pass@1: 27.9 -> 29.1 | Helped |
| use transition-model embeddings instead of tactic-reconstruction autoencoder embeddings (ablation) | 3D-Prover with ReProver · miniF2F-valid Pass@1, K=32 | Pass@1: 27.0 -> 28.7 | Helped |
| increase error weight from λ_s=0.1 to λ_s=0.5 (ablation) | 3D-Prover with ReProver · miniF2F-valid tactic success rate per node, K=8 | tactic success rate: 43.3 ± 0.1 -> 56.5 ± 0.1 | Helped |
| increase diversity temperature from θ=1 to θ=4 (ablation) | 3D-Prover with ReProver · miniF2F-valid unique subgoals per successful tactic, K=8 | unique subgoals: 90.1 ± 0.1 -> 91.1 ± 0.1 | Helped |
| increase time weight from λ_τ=0.1 to λ_τ=1.0 (ablation) | 3D-Prover with ReProver · miniF2F-valid tactic execution time, K=8 | execution time (milliseconds): 155 ± 0.5 -> 136 ± 0.5 | Helped |
| increase diversity temperature from θ=1 to θ=4 (ablation) | 3D-Prover with ReProver · miniF2F-valid Pass@1, K=16 | Pass@1: 29.1 -> 26.6 | Hurt |
| increase time weight from λ_τ=0.1 to λ_τ=1.0 (ablation) | 3D-Prover with ReProver · miniF2F-valid Pass@1, K=8 | Pass@1: 25.0 -> 22.5 | Hurt |
Surprising findings
- Filtering on predicted error probability did not consistently improve Pass@1, with the authors suggesting false negatives in error prediction may discard useful tactics.
- Tree search improvements were reported to be much smaller than gains from improving the base generator, consistent with the paper's framing of search as an augmentation.
Limitations
- Limited experimental scale: many runs and hyperparameter sweeps were infeasible, with only 15 runs on miniF2F-valid for ablations.
- No hyperparameter tuning for the main results, and the comprehensive sweep was prohibitively expensive.
- Transition model trained only on one proof attempt per benchmark, with evaluation on InternLM limited to Pass@2 (BFS) and Pass@6 (Critic Guided).
Experimental setup
Datasets: miniF2F-valid miniF2F-test LeanDojo Novel Premises
Benchmarks: miniF2F-valid miniF2F-test LeanDojo Novel Premises
Metrics: Pass@1 Pass@k tactic success rate unique subgoal percentage cosine similarity of subgoals execution time BLEU ROUGE-L F1 MSE
Baselines: No Filtering Top-K Random Autoencoder Critic Guided search
Builds on: ReProver k-DPP LeanDojo BAIT
Closest papers by meaning
- MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.89)
- ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.87)
- Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers (ICML 2026 · similarity 0.87)
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data (ICLR 2024 · similarity 0.87)
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.87)
- DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (ICLR 2025 · similarity 0.87)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.