# 3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes

arXiv: https://arxiv.org/abs/2410.11133 · HTML: https://mlsanity.com/paper/2410.11133/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 26 of its 45 references that are in the map.
- First posted on arXiv 14 Oct 2024.

## Builds on (most cited first, 26 of 26)

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Video Summarization with Long Short-term Memory](https://mlsanity.com/paper/1605.08110/) (2016)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving](https://mlsanity.com/paper/2007.02924/) (2020)
- [Learning to Prove Theorems by Learning to Generate Theorems](https://mlsanity.com/paper/2002.07019/) (2020)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving](https://mlsanity.com/paper/2305.16366/) (2023)
- [Holophrasm: a neural Automated Theorem Prover for higher-order logic](https://mlsanity.com/paper/1608.02644/) (2016)
- [Creating Capsule Wardrobes from Fashion Images](https://mlsanity.com/paper/1712.02662/) (2017)
- [Learning to Reason with HOL4 tactics](https://mlsanity.com/paper/1804.00595/) (2018)
- [BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving](https://mlsanity.com/paper/2403.03401/) (2024)

## Built on by (most cited first, 6 of 6)

- [LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning](https://mlsanity.com/paper/2603.21065/) (2026)
- [Free Lunch for Pass@k? Low Cost Diverse Sampling for Diffusion Language Models](https://mlsanity.com/paper/2603.04893/) (2026)
- [Reliability-Aware Determinantal Point Processes for Robust Informative Data Selection in Large Language Models](https://mlsanity.com/paper/2602.00885/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs](https://mlsanity.com/paper/2607.16997/) (2026)
- [Improving the Diversity of LLM Outputs without a Trade-off](https://mlsanity.com/paper/2609.33038/) (2026)

## Abstract (arXiv)

A key challenge in automated formal reasoning is the intractable search space, which grows exponentially with the depth of the proof. This branching is caused by the large number of candidate proof tactics which can be applied to a given goal. Nonetheless, many of these tactics are semantically similar or lead to an execution error, wasting valuable resources in both cases. We address the problem of effectively pruning this search, using only synthetic data generated from previous proof attempts. We first demonstrate that it is possible to generate semantically aware tactic representations which capture the effect on the proving environment, likelihood of success, and execution time. We then propose a novel filtering mechanism which leverages these representations to select semantically diverse and high quality tactics, using Determinantal Point Processes. Our approach, 3D- Prover, is designed to be general, and to augment any underlying tactic generator. We demonstrate the effectiveness of 3D-Prover on the miniF2F and LeanDojo benchmarks by augmenting popular open source proving LLMs. We show that our approach leads to an increase in the overall proof rate, as well as a significant improvement in the tactic success rate, execution time and diversity. We make our code available at https://github.com/sean-lamont/3D-Prover.