用合成数据提升大模型证明能力，实现高效定理自动证明。
LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
- 设计新方法生成多样化中间证明状态数据
- 在MiniF2F上达到60.74%的单次通过率
- 适合研究自动推理与大模型应用的学者
近年来大语言模型（LLMs）的发展推动了自动化定理证明的研究，主流方法是将分步推理的LLM与树搜索结合。本文提出一种新的证明状态探索方法，用于训练数据合成，可生成涵盖广泛中间证明状态的多样化策略，从而支持对LLM作为策略模型的一次性微调。同时引入自适应束宽策略，在树搜索中平衡探索与利用。在MiniF2F和ProofNet基准上的评估显示，本方法在严格的Pass@1指标下优于强基线，平均通过率分别达60.74%和21.18%，验证了大规模合成数据在推进自动化定理证明中的关键作用。
原文摘要 · Abstract (English)
Recent advancements in large language models (LLMs) have sparked considerable interest in automated theorem proving and a prominent line of research integrates stepwise LLM-based provers into tree search. In this paper, we introduce a novel proof-state exploration approach for training data synthesis, designed to produce diverse tactics across a wide range of intermediate proof states, thereby facilitating effective one-shot fine-tuning of LLM as the policy model. We also propose an adaptive beam size strategy, which effectively takes advantage of our data synthesis method and achieves a trade-off between exploration and exploitation during tree search. Evaluations on the MiniF2F and ProofNet benchmarks demonstrate that our method outperforms strong baselines under the stringent Pass@1 metric, attaining an average pass rate of $60.74\%$ on MiniF2F and $21.18\%$ on ProofNet. These results underscore the impact of large-scale synthetic data in advancing automated theorem proving.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。