mlsanityData to 14 Oct 2026

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

arXiv 2410.11133 ↗First posted 14 Oct 2024cs.AI cs.LOcited by 6

Not on the map. Why?

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.

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

26 of 45 references.

References · 26

  1. 2021Evaluating Large Language Models Trained on Codecited by 8,320
  2. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,392
  3. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  4. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  5. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  6. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  7. 2022HyperTree Proof Search for Neural Theorem Provingcited by 197
  8. 2016Video Summarization with Long Short-term Memorycited by 142
  9. 2022Formal Mathematics Statement Curriculum Learningcited by 142
  10. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  11. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
  12. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 109
14 more
  1. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 98
  2. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 82
  3. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 53
  4. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  5. 2017Deep Network Guided Proof Searchcited by 47
  6. 2020INT: An Inequality Benchmark for Evaluating Generalization in Theorem Provingcited by 44
  7. 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
  8. 2015A formal proof of the Kepler conjecturecited by 42
  9. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  10. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  11. 2016Holophrasm: a neural Automated Theorem Prover for higher-order logiccited by 29
  12. 2017Creating Capsule Wardrobes from Fashion Imagescited by 24
  13. 2018Learning to Reason with HOL4 tacticscited by 14
  14. 2024BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Provingcited by 2

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 6.

6 papers.

  1. 2026LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learningcited by 7
  2. 2026Free Lunch for Pass@k? Low Cost Diverse Sampling for Diffusion Language Modelscited by 5
  3. 2026Reliability-Aware Determinantal Point Processes for Robust Informative Data Selection in Large Language Modelscited by 1
  4. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  5. 2026PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofscited by 0
  6. 2026Improving the Diversity of LLM Outputs without a Trade-offcited by 0