FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory

📄 arXiv: 2510.02335v1 📥 PDF

作者: Xiao-Wen Yang, Zihao Zhang, Jianuo Cao, Zhi Zhou, Zenan Li, Lan-Zhe Guo, Yuan Yao, Taolue Chen, Yu-Feng Li, Xiaoxing Ma

分类: cs.CL, cs.AI

发布日期: 2025-09-26

💡 一句话要点

FormalML：用于评估机器学习理论中形式化子目标补全的基准测试

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

关键词: 形式化定理证明 子目标补全 机器学习理论 Lean 4 基准测试

📋 核心要点

  1. 现有大型语言模型在形式化定理证明中表现出潜力，但缺乏在复杂证明中补全子目标的能力。
  2. 论文提出FormalML基准测试，专注于机器学习理论的形式化子目标补全，包含优化和概率不等式等问题。
  3. 实验评估表明现有证明器在FormalML上存在准确性和效率的局限性，亟需更强大的LLM定理证明器。

📝 摘要（中文）

大型语言模型（LLM）最近在形式化定理证明方面取得了显著进展。然而，它们作为数学家的实用助手，在复杂证明中填补缺失步骤的能力仍未得到充分探索。我们将这一挑战定义为子目标补全任务，即LLM必须完成人类提供的草图中未解决的简短但重要的证明义务。为了研究这个问题，我们引入了FormalML，这是一个基于机器学习基础理论构建的Lean 4基准测试。通过使用将程序性证明转换为声明性形式的翻译策略，我们提取了4937个涵盖优化和概率不等式的问题，难度各不相同。FormalML是第一个结合前提检索和复杂研究级上下文的子目标补全基准。对最先进的证明器的评估突显了准确性和效率方面的持续局限性，强调了需要更强大的基于LLM的定理证明器来实现有效的子目标补全。

🔬 方法详解

问题定义：论文旨在解决大型语言模型在形式化定理证明中，无法有效补全人类提供的证明草图中缺失的子目标的问题。现有方法在处理复杂、研究级别的数学证明时，准确性和效率都存在瓶颈，难以作为数学家的实用助手。

核心思路：论文的核心思路是构建一个专门针对机器学习理论的形式化子目标补全基准测试，即FormalML。通过提供大量具有不同难度的子目标补全问题，促进LLM在该领域的应用和发展。这种方法旨在推动LLM在更复杂的数学推理任务中的应用。

技术框架：FormalML基准测试基于Lean 4定理证明器构建，包含以下主要步骤：1) 从机器学习的基础理论中提取证明；2) 使用翻译策略将程序性证明转换为声明性形式；3) 构建包含4937个子目标补全问题的基准测试，涵盖优化和概率不等式等领域。该基准测试结合了前提检索和复杂的研究级上下文。

关键创新：FormalML的关键创新在于它是第一个专门针对机器学习理论的形式化子目标补全基准测试。它结合了前提检索和复杂的研究级上下文，更贴近实际的数学研究场景。此外，它提供了一个标准化的平台，用于评估和比较不同LLM在子目标补全任务中的性能。

关键设计：FormalML的关键设计包括：1) 使用Lean 4作为定理证明器，提供强大的形式化推理能力；2) 使用翻译策略将程序性证明转换为声明性形式，方便LLM理解和处理；3) 构建包含4937个问题的基准测试，覆盖优化和概率不等式等领域，难度各不相同；4) 结合前提检索，模拟实际数学研究中需要查找相关定理和引理的过程。

📊 实验亮点

论文通过对最先进的证明器在FormalML上的评估，揭示了现有方法在准确性和效率方面的局限性。实验结果表明，即使是最先进的证明器，在处理复杂的子目标补全问题时仍然面临挑战，这突显了开发更强大的LLM定理证明器的必要性。FormalML的发布为该领域的研究提供了一个重要的基准。

🎯 应用场景

FormalML的研究成果可应用于自动化定理证明、数学辅助工具开发以及机器学习理论研究。通过提升LLM在形式化推理方面的能力，可以加速数学研究进程，并为机器学习算法的正确性提供更强的保障。未来，该基准测试可以扩展到其他数学领域，并促进LLM在科学发现中的应用。

📄 摘要（原文）

Large language models (LLMs) have recently demonstrated remarkable progress in formal theorem proving. Yet their ability to serve as practical assistants for mathematicians, filling in missing steps within complex proofs, remains underexplored. We identify this challenge as the task of subgoal completion, where an LLM must discharge short but nontrivial proof obligations left unresolved in a human-provided sketch. To study this problem, we introduce FormalML, a Lean 4 benchmark built from foundational theories of machine learning. Using a translation tactic that converts procedural proofs into declarative form, we extract 4937 problems spanning optimization and probability inequalities, with varying levels of difficulty. FormalML is the first subgoal completion benchmark to combine premise retrieval and complex research-level contexts. Evaluation of state-of-the-art provers highlights persistent limitations in accuracy and efficiency, underscoring the need for more capable LLM-based theorem provers for effective subgoal completion,