Theorem proving is a fundamental task in mathematics. With the advent of large language models (LLMs) and interactive theorem provers (ITPs) like Lean, there has been growing interest in integrating LLMs and ITPs to automate theorem proving. In this approach, the LLM generates proof steps (tactics), and the ITP checks the applicability of the tactics at the current goal. The two systems work together to complete the proof. In this paper, we introduce DS-Prover, a novel dynamic sampling method for theorem proving. This method dynamically determines the number of tactics to apply to expand the current goal, taking into account the remaining time compared to the total allocated time for proving a theorem. This makes the proof search process more efficient by adjusting the balance between exploration and exploitation as time passes. We also augment the training dataset by decomposing simplification and rewrite tactics with multiple premises into tactics with single premises. This gives the model more examples to learn from and helps it to predict the tactics with premises more accurately. We perform our experiments using the Mathlib dataset of the Lean theorem prover and report the performance on two standard datasets, MiniF2F and ProofNet. Our methods achieve significant performance gains on both datasets. We achieved a state-of-the-art performance (Pass@1) of 14.2% on the ProofNet dataset and a performance of 29.8% on MiniF2F, slightly surpassing the best-reported Pass@1 of 29.6% using Lean.

翻译：定理证明是数学中的一项基本任务。随着大型语言模型（LLM）和交互式定理证明器（ITP）如Lean的出现，将LLM与ITP集成以自动化定理证明的研究兴趣日益增长。该方法中，LLM生成证明步骤（策略），ITP检查策略在当前目标下的适用性，两个系统协同完成证明。本文提出了DS-Prover，一种新颖的定理证明动态采样方法。该方法通过考虑证明定理总分配时间的剩余时间，动态确定扩展当前目标所需应用的策略数量。随着时间推移，通过调整探索与利用之间的平衡，使得证明搜索过程更加高效。我们还通过将包含多个前提的简化和重写策略分解为单前提策略来增强训练数据集。这为模型提供了更多学习样本，并帮助其更准确地预测带前提的策略。我们使用Lean定理证明器的Mathlib数据集进行实验，并在两个标准数据集MiniF2F和ProofNet上报告性能。我们的方法在两个数据集上均取得了显著性能提升。在ProofNet数据集上实现了14.2%的最优性能（Pass@1），在MiniF2F上达到了29.8%的成绩，略高于使用Lean报告的最佳Pass@1结果29.6%。