Conjecturing: An Overlooked Step in Formal Mathematical Reasoning

📄 arXiv: 2510.11986v1 📥 PDF

作者: Jasivan Alex Sivakumar, Philipp Borchert, Ronald Cardenas, Gerasimos Lampouras

分类: cs.CL, cs.AI

发布日期: 2025-10-13

💡 一句话要点

提出ConjectureBench评估LLM在形式化数学推理中被忽视的猜想步骤，并设计Lean-FIRe方法提升性能。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 自动形式化 猜想 大型语言模型 数学推理 数据集 评估框架 Lean-FIRe

📋 核心要点

  1. 现有自动形式化方法忽略了猜想这一关键步骤，导致对LLM能力的评估不准确。
  2. 提出ConjectureBench数据集和Lean-FIRe方法，分别用于评估和提升LLM的猜想能力。
  3. 实验表明，考虑猜想后，LLM的自动形式化性能被高估，Lean-FIRe成功自动形式化了多个PutnamBench问题。

📝 摘要（中文）

自动形式化是将非形式化的数学陈述用形式化语言表达的任务，通常被视为一个直接的翻译过程。然而，这忽略了一个关键的前置步骤：猜想。许多数学问题在没有首先猜想出一个结论（例如显式答案或特定界限）的情况下，无法直接形式化。由于大型语言模型（LLM）已经在自动形式化方面表现挣扎，并且对其猜想能力的评估有限且常常与自动形式化或证明纠缠在一起，因此理解其影响尤其具有挑战性。为了解决这个差距，我们扩充了现有数据集以创建ConjectureBench，并重新设计了评估框架和指标，专门用于衡量LLM的猜想能力，既作为一个独立的任务，也在自动形式化流程中。我们对包括GPT-4.1和DeepSeek-V3.1在内的基础模型的评估表明，当在评估期间考虑猜想时，它们的自动形式化性能被大大高估了。然而，不应假定提供猜想。我们设计了一种推理时方法Lean-FIRe来改进猜想和自动形式化，据我们所知，它首次成功地对13个PutnamBench问题使用GPT-4.1和7个问题使用DeepSeek-V3.1进行了端到端的自动形式化。我们证明，虽然LLM拥有生成准确猜想的必要知识，但提高自动形式化性能需要将猜想视为一个独立的任务，并进一步研究如何将其正确地整合到自动形式化中。最后，我们提供了前瞻性指导，以引导未来的研究朝着改进猜想的方向发展，这是形式化数学推理中一个被忽视的步骤。

🔬 方法详解

问题定义：论文旨在解决自动形式化过程中忽略猜想步骤的问题。现有方法通常将自动形式化视为直接翻译，忽略了在形式化之前需要先提出合理的数学猜想。这导致对LLM在自动形式化任务中的真实能力评估不准确，并且阻碍了端到端自动形式化性能的提升。

核心思路：论文的核心思路是将猜想视为自动形式化流程中一个独立的、至关重要的步骤。通过显式地评估和改进LLM的猜想能力，可以更准确地衡量其在自动形式化任务中的表现，并最终提升端到端的自动形式化性能。论文认为，LLM已经具备生成准确猜想的知识，但需要更好的方法来引导和利用这些知识。

技术框架：论文提出了ConjectureBench数据集和Lean-FIRe方法。ConjectureBench用于评估LLM的猜想能力，包含扩充的数学问题，并设计了专门的评估指标。Lean-FIRe是一种推理时方法，旨在改进LLM的猜想和自动形式化能力。具体流程未知，但其目标是提升LLM生成准确猜想的能力，并将其整合到自动形式化流程中。

关键创新：论文的关键创新在于强调了猜想在自动形式化中的重要性，并将其作为一个独立的研究方向。通过ConjectureBench数据集和Lean-FIRe方法，论文提供了一种评估和改进LLM猜想能力的新途径。这是首次尝试将猜想显式地纳入自动形式化流程中，并取得了初步的成功。

关键设计：关于Lean-FIRe方法的具体技术细节，例如关键参数设置、损失函数、网络结构等，论文摘要中没有详细描述。ConjectureBench数据集的构建细节也未知。这些细节可能在论文正文中详细阐述。

🖼️ 关键图片

img_0

📊 实验亮点

实验结果表明，在考虑猜想步骤后，LLM的自动形式化性能被显著高估。Lean-FIRe方法成功地使用GPT-4.1自动形式化了13个PutnamBench问题，使用DeepSeek-V3.1自动形式化了7个问题，实现了端到端自动形式化的突破。这证明了LLM具备生成准确猜想的潜力，并验证了将猜想作为独立任务进行研究的有效性。

🎯 应用场景

该研究成果可应用于自动化定理证明、数学知识发现、以及智能教育等领域。通过提升LLM的猜想能力，可以帮助数学家和研究人员更高效地进行数学研究，并为学生提供更智能化的学习辅助工具。未来，该研究有望推动人工智能在数学领域的更广泛应用。

📄 摘要（原文）

Autoformalisation, the task of expressing informal mathematical statements in formal language, is often viewed as a direct translation process. This, however, disregards a critical preceding step: conjecturing. Many mathematical problems cannot be formalised directly without first conjecturing a conclusion such as an explicit answer, or a specific bound. Since Large Language Models (LLMs) already struggle with autoformalisation, and the evaluation of their conjecturing ability is limited and often entangled within autoformalisation or proof, it is particularly challenging to understand its effect. To address this gap, we augment existing datasets to create ConjectureBench, and redesign the evaluation framework and metric specifically to measure the conjecturing capabilities of LLMs both as a distinct task and within the autoformalisation pipeline. Our evaluation of foundational models, including GPT-4.1 and DeepSeek-V3.1, reveals that their autoformalisation performance is substantially overestimated when the conjecture is accounted for during evaluation. However, the conjecture should not be assumed to be provided. We design an inference-time method, Lean-FIRe to improve conjecturing and autoformalisation, which, to the best of our knowledge, achieves the first successful end-to-end autoformalisation of 13 PutnamBench problems with GPT-4.1 and 7 with DeepSeek-V3.1. We demonstrate that while LLMs possess the requisite knowledge to generate accurate conjectures, improving autoformalisation performance requires treating conjecturing as an independent task, and investigating further how to correctly integrate it within autoformalisation. Finally, we provide forward-looking guidance to steer future research toward improving conjecturing, an overlooked step of formal mathematical reasoning.