LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving

我们提出了 LeanConjecturer，这是一个利用大语言模型（LLMs）在 Lean 4 中自动生成大学水平数学猜想的流程。我们的混合方法结合了基于规则的上下文提取与基于大语言模型的定理陈述生成，从而应对形式化定理证明中数据稀缺的挑战。通过迭代生成与评估，LeanConjecturer 从 40 个 Mathlib 种子文件中生成了 12,289 条猜想，其中 3,776 条被判定为语法正确且非平凡，即无法通过 \texttt{aesop} 策略证明。我们展示了这些生成的猜想在强化学习中的实用性，特别是通过“群体相对策略优化”（GRPO）方法，表明针对特定领域猜想的训练可以提升定理证明的能力。我们的方法平均每种子文件生成 103.25 条新猜想，为定理证明系统创建训练数据提供了一个可扩展的解决方案。我们的系统已成功验证了多个拓扑学中的非平凡定理，包括半开集、α-开集和前开集的性质，显示出其在超越现有结果的数学发现方面的潜力。

这篇论文旨在解决形式化定理证明中训练数据稀缺的问题，特别是如何自动产生具有挑战性的、大学水平的数学猜想（以Lean 4语言表达），从而为强化学习在定理证明中的应用提供高质量的数据支持。这是一个相对较新的问题，因为随着LLM的发展，研究者开始探索其在形式化数学和自动化证明中的潜力。

论文提出了一种混合方法LeanConjecturer，结合了基于规则的上下文提取与基于大语言模型（LLM）的定理生成。这种方法利用少量的Lean种子文件，通过迭代生成和筛选机制，自动生成大量非平凡且语法正确的数学猜想。相比现有研究，该工作的创新点在于将LLM与领域特定规则相结合，并引入评估机制来确保生成猜想的难度和价值。

{"从40个Mathlib种子文件中生成12,289个猜想，其中3,776个被验证为非平凡且语法正确",平均每个种子文件生成103.25个新猜想，展示了方法的高扩展性,成功验证了拓扑学中关于semi-open、alpha-open和pre-open集合的非平凡定理,"使用Group Relative Policy Optimization (GRPO) 进行强化学习实验，显示定向训练可提升定理证明能力",为形式化数学和自动化定理证明提供了潜在的新数据源}

{"Towards Understanding and Harnessing the Potential of Large Language Models in Theorem Proving","Premise Selection and External Knowledge Integration for Mathematics with Deep Learning","Synthetic Proof Generation for Theorem Provers using Language Models","Formal Mathematics Statement Curriculum Learning","Reinforcement Learning for Theorem Proving with Tree-Based Policies"}