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.

翻译：自动形式化推理中的一个关键挑战是搜索空间随证明深度呈指数级增长，导致计算不可行。这种分支现象源于对给定证明目标可应用的大量候选证明策略。然而，这些策略中许多在语义上相似或会导致执行错误，两种情况均会浪费宝贵资源。我们通过仅利用先前证明尝试生成的合成数据，解决了有效剪枝该搜索空间的问题。我们首先证明，可以生成语义感知的策略表示，这些表示能捕捉策略对证明环境的影响、成功概率及执行时间。随后，我们提出一种新颖的过滤机制，利用这些表示通过行列式点过程选择语义多样且高质量的证明策略。我们的方法——3D-Prover——设计为通用框架，可增强任何底层策略生成器。通过在miniF2F和LeanDojo基准测试中增强流行的开源证明大语言模型，我们验证了3D-Prover的有效性。实验表明，该方法能提升整体证明成功率，并在策略成功率、执行时间和多样性方面带来显著改进。代码已开源：https://github.com/sean-lamont/3D-Prover。