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

2024-10-14 · Sean Lamont, Christian Walder, Amir Dezfouli, Paul Montague, Michael Norrish

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-valid and miniF2F-test benchmarks by augmenting the ReProver LLM. 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.

📄 PDF Abstract BibTeX arXiv:2410.11133

Code (0)

등록된 구현이 없습니다.

Tasks

Automated Theorem ProvingDiversityPoint Processesvalid

Methods 이 논문이 사용한 방법론

Pruning 설명 없음

AWARE We propose to theoretically and empirically examine the effect of incorporating weighting schemes into walk-aggregating GNNs. To this end, we propose a simple, interpretable, and…

HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement

2025-05-21 · Jilin Hu, Jianyu Zhang, Yongwang Zhao, Talia Ringer

Formal methods is pivotal for verifying the reliability of critical systems through rigorous mathematical proofs. However, its adoption is hindered by labor-intensive manual proofs and the expertise required to use theor…

Automated Theorem Proving Mathematical Proofs

HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

2019-04-05 · Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy 외

We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of arbitrary mathematical theories and the…

Automated Theorem Proving BIG-bench Machine Learning Deep Learning Deep Reinforcement Learning+3

A Theoretical Framework for Self-Play Theorem Proving Algorithms

2026-06-01 · Thomas Chen, Zhiyuan Li arxiv

Self-play, a type of training algorithm that enables a model to self-improve, has recently shown promising empirical results in the context of formal theorem proving using Large Language Models (LLMs). (Dong & Ma, 2025) …

Contrastive Learning

Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study

2026-01-22 · Zachary Burton arxiv

RL-trained Lean theorem provers mode-collapse at inference time: on miniF2F-test with DeepSeek-Prover-V1.5-RL, doubling the i.i.d.\ sampling budget from $k{=}32$ to $k{=}64$ produces zero additional solved theorems (42/2…

Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction

2025-08-05 · Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang 외 arxiv

We introduce Goedel-Prover-V2, a series of open-source language models that set a new state-of-the-art in automated theorem proving. Built on the standard expert iteration and reinforcement learning pipeline, our approac…

Automated Theorem Proving Reinforcement Learning