用确定性点过程筛选高多样性、高质量证明策略，提升自动定理证明效率。
3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
- 通过语义感知表示捕捉策略效果、成功率与耗时，构建可量化策略特征。
- 在miniF2F和LeanDojo上提升整体证明率，策略成功率与多样性显著改善。
- 不依赖真实数据，仅用历史证明生成合成数据，通用性强适合各类证明模型。
自动形式推理的核心挑战在于搜索空间呈指数级膨胀，源于每步可选的大量证明策略。许多策略语义相似或导致执行错误，浪费计算资源。本文提出3D-Prover，仅利用历史证明生成的合成数据，构建能表征策略对证明环境影响、成功概率与执行时间的语义感知表示。进一步引入确定性点过程（Determinantal Point Processes）设计新颖筛选机制，优先选择语义多样且质量高的策略。该方法具有通用性，可无缝集成至任意底层策略生成器。在miniF2F与LeanDojo基准上，通过增强主流开源证明大模型，显著提升整体证明率、策略成功率、执行效率及策略多样性。代码已公开于https://github.com/sean-lamont/3D-Prover。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。