构建首个机器学习理论的子目标补全基准，评估大模型填补证明漏洞能力
FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory
- 从机器学习基础理论中提取4937个需补全的证明目标
- 现有大模型在复杂证明上下文中准确率与效率仍不足
- 适合研究形式化证明、大模型辅助数学推理的学者
大型语言模型（LLMs）在形式化定理证明方面取得显著进展，但其作为数学家实用助手、补全复杂证明中缺失步骤的能力仍待探索。我们将此问题定义为子目标补全任务，即让大模型填补人类提供证明草图中未解决的短而非平凡的证明义务。为此，我们引入FormalML，一个基于机器学习基础理论的Lean 4基准。通过将过程式证明转换为声明式形式的转换策略，我们提取了4937个涵盖优化与概率不等式的题目，难度各异。FormalML是首个结合前提检索与复杂研究级上下文的子目标补全基准。对前沿证明器的评估揭示了在准确性与效率上的持续局限，凸显了提升大模型形式化证明能力以实现有效子目标补全的迫切需求。
原文摘要 · Abstract (English)
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,
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。