1. 项目概述为什么我们需要一个“子目标补全”的评测基准如果你尝试过用Lean、Coq或Isabelle这类交互式定理证明器来形式化一个哪怕只是本科水平的数学定理你大概率会经历一个从雄心勃勃到怀疑人生的过程。你写下一个定理陈述构思好证明的大致轮廓然后开始一行行地填充证明步骤。很快你就会卡在某个看似简单的等式变换或不等式放缩上——你心里清楚“这步显然成立”但要让证明器接受可能需要你显式地调用三四个引理并小心翼翼地处理量词和类型。这个“显然”但机器无法自动跨越的鸿沟就是子目标补全任务要解决的核心问题。传统的定理证明评测比如MiniF2F或ProofNet更像是让模型参加“数学奥林匹克竞赛”给出一道完整的题目要求模型从头到尾生成整个证明。这固然能体现模型的推理能力但离数学家日常的科研工作场景相去甚远。现实中数学家更需要的不是一个能独立解决竞赛题的“天才”而是一个能理解我的证明草图、在我卡壳时帮我填上技术细节的“得力助手”。这就是FormalML基准的出发点它不再追求让模型“无中生有”地创造整个证明而是评估它能否在人类专家设定好的高层框架下高效、准确地完成那些琐碎但关键的中间步骤。FormalML将目光聚焦于机器学习理论这个领域这绝非偶然。一方面机器学习本身的理论研究如优化算法的收敛性分析、泛化误差界的推导正日益依赖严格的数学证明以确保其可靠性。另一方面该领域包含了大量结构化的不等式处理和算法分析其证明步骤既具有典型性又具备足够的复杂度是检验模型“助手”能力的绝佳试验场。通过从两个成熟的Lean 4库Optlib和FoML中提取出4937个具体的子目标问题FormalML首次为“子目标补全”这个任务建立了一个大规模、可复现、且贴近真实研究场景的评测标准。2. 核心思路拆解从“过程式证明”到“声明式子目标”要理解FormalML的构建精髓必须搞懂它解决的一个关键工程难题如何从人类惯写的“过程式”证明脚本中自动抽取出干净、独立的“声明式”子目标在Lean社区为了编写效率很多证明是“过程式”的。你会写一连串的rw重写、simp简化、linarith线性算术等策略tactics这些策略直接操作证明状态一步步将其变形至最终目标。例如一个证明梯度下降单步递减的引理其Lean代码可能是一连串的策略调用。对于人类来说每一行代码通常对应一个清晰的推理步骤比如“应用Lipschitz条件”。但对于机器来说这一行代码执行后证明状态具体变成了什么样它对应的逻辑命题是什么并不直观。FormalML团队设计了一个名为to_theorem的定制化Lean 4策略tactic完美地解决了这个问题。它的工作原理非常巧妙状态快照在运行某一行或连续几行过程式策略之前记录下当前的证明状态所有假设和当前目标。执行与再记录执行这行策略然后在策略执行之后再次记录证明状态。定理合成将“之前”的状态中的所有假设作为新定理的前提hypotheses将“之后”状态中的目标作为新定理的结论goal从而合成出一个全新的、独立的Lean定理。证明关联这个新定理的证明就是最初的那行或那几行过程式策略本身。这个过程相当于把一个动态的、状态转换的过程“冻结”并“物化”为一个静态的、可独立验证的数学命题。图2中的例子清晰地展示了这一点从一行包含repeat rw [dotProduct]; simp [mul_comm]的策略to_theorem提取出了一个关于向量点积和标量乘法交换律的特定不等式子目标。为什么这个设计至关重要它使得评测变得纯粹和公平。评测时我们不再需要让模型去模拟执行过程式策略这涉及到与证明环境的复杂交互而是直接给它一个声明式的定理陈述“已知A, B, C请证明D”以及所有可用的前提本地库和Mathlib中的相关引理。这完美模拟了人类数学家在思考“如何从这个式子推到那个式子”时所面对的逻辑情境。基于to_theoremFormalML通过控制提取的证明片段的长度1行、3行、5行自然地定义了问题的难度等级。只包含一个策略的子目标难度1通常是最直接的代数变形或引理应用而包含多个策略组合的子目标难度3或5则可能涉及更复杂的逻辑结构或中间引理的串联。这种分级让评测不仅能看“总分”还能分析模型在不同认知负荷下的表现。3. 数据集构建深耕机器学习理论的两大支柱FormalML的数据并非凭空生成而是根植于两个正在活跃发展的Lean 4形式化项目Optlib和FoML。这保证了基准中的问题都来源于真实、前沿的机器学习理论研究。3.1 Optlib优化算法的形式化基石Optlib项目旨在形式化一整套经典的一阶优化算法及其收敛性分析。FormalML从中提取的问题覆盖了梯度下降法光滑凸函数下的收敛性证明。次梯度法处理非光滑问题的收敛性。近端梯度下降法用于复合优化问题。Nesterov加速方法证明其达到最优收敛速率。块坐标下降法和交替方向乘子法用于大规模分布式优化。从这些算法的收敛性证明中提取出的子目标大量涉及Lipschitz连续性、强凸性、次梯度不等式等基本概念的应用以及复杂的范数运算和不等式放缩技巧。例如证明梯度下降单步递减f(x_{k1}) ≤ f(x_k) - (α/2) * ‖∇f(x_k)‖^2时中间需要用到梯度Lipschitz性质展开并合并同类项这些步骤都被提取成了独立的子目标。3.2 FoML概率与泛化理论的形式化FoML项目则专注于机器学习理论中另一个核心支柱基于Rademacher复杂度的泛化误差界。FormalML从中提取的问题包括经典概率不等式霍夫丁不等式、伯恩斯坦不等式、本尼特不等式、McDiarmid不等式等。这些不等式是分析算法稳定性和泛化能力的理论基础。期望与矩的相关引理。Rademacher复杂度的定义、性质及其与泛化误差的关联证明。这部分问题对概率论和测度论的知识要求较高涉及随机变量、期望、独立性、有界差等概念的形式化处理。例如证明McDiarmid不等式的过程中需要构造鞅差序列并应用Azuma-Hoeffding不等式其中的每一步条件期望的计算和放缩都可以被提取为具有挑战性的子目标。3.3 数据格式与上下文封装每个提取出的子目标都被精心封装在一个结构化的JSON记录中确保其可独立评测{ “file_path”: “Optlib/GradientMethod.lean” “line_range”: [120, 125] “imports”: [“Mathlib.Analysis.Calculus.Deriv” “Mathlib.Analysis.Convex.Basic”] “theorem_statement”: “∀ (f : E → ℝ) (hf : ConvexOn ℝ univ f) ... f (x - a • ∇f x) ≤ f x - a/2 * ‖∇f x‖ ^ 2” “proof_steps”: “rw [sub_eq_add_neg]; nlinarith [h_lipschitz]” “premises”: [“ConvexOn.subgradient_inequality” “LipschitzWith.norm_sub_le”] }file_path和line_range提供了问题的溯源信息。imports指明了验证该定理所需导入的Mathlib模块这对于构建正确的证明环境至关重要。theorem_statement子目标的正式陈述是模型需要解决的核心。proof_steps原始的、正确的过程式证明步骤。在评测中模型看不到这个字段它仅用于验证模型生成的证明是否正确。premises从本地库和Mathlib中检索出的、与该子目标最相关的引理列表。这模拟了人类证明时需要查阅参考资料的过程是前提检索任务的核心。这种设计使得FormalML不仅仅是一个问题集更是一个完整的、可复现的评测生态系统。4. 评测挑战为什么子目标补全比想象中更难在FormalML论文中作者指出了子目标补全任务对现有基于LLM的证明器构成的三大核心挑战这恰恰也是该基准的价值所在。4.1 复杂证明上下文的理解在竞赛题证明生成中问题的前提和结论通常比较干净、独立。但在一个长篇研究级证明的中间当前需要补全的子目标身处一个高度复杂的上下文中。假设列表h1, h2, ...可能已经积累了十几个其中包含各种复杂的量词、等式、不等式和类型约束。模型必须准确理解所有这些假设的含义及其相互关系才能生成正确的下一步。这要求模型具备强大的上下文理解与整合能力而不仅仅是生成漂亮的推理链。4.2 精准的前提检索这是FormalML区别于以往基准的最大特色之一。在4937个问题中有2049个需要模型从给定的候选前提库包含Mathlib和本地库的引理中找出正确的定理来使用。候选库可能包含10个或20个引理其中混杂着无关或干扰项。实操心得这模拟了真实研究中最耗时的一部分工作——查资料。一个熟练的数学家能快速想起“这里应该用Jensen不等式”或“那个形式很像Cauchy-Schwarz”。对于模型来说这要求它不仅仅会推理还要有一个强大的“数学记忆库”和精准的检索能力。实验发现很多在完整证明生成上表现优秀的模型一旦加入检索任务性能就会显著下降因为它们不擅长从海量知识中 pinpoint 出最关键的那一两条。4.3 效率与“过度思考”的权衡竞赛题往往需要长链条、创造性的推理。而子目标补全尤其是难度等级为1的问题通常只需要一两个直接的策略就能解决。然而一些为竞赛训练出来的“重型”模型在面对简单子目标时容易陷入“过度思考”生成冗长、迂回的自然语言推理Chain-of-Thought CoT最终才输出一个简短的正式证明。这不仅浪费计算资源延长响应时间有时还会因为复杂的中间推理引入错误。 FormalML论文提出了一个新颖的评估指标效率加权准确率EWAKEWAK PassK * (100 / 平均响应长度)。这个指标惩罚那些虽然能解出题但输出异常冗长的模型。实验结果显示一些采用长链思维Long-CoT的模型在FormalML上不仅通过率没有优势EWA得分反而因为生成了大量不必要的token而垫底。这明确提示一个好的“助手”应该简洁、精准而不是炫技。5. 主流证明器在FormalML上的表现与深度分析论文对当前最先进的两大类基于LLM的定理证明器进行了系统评测最佳优先树搜索方法和全证明生成方法。5.1 方法简述与评测设置最佳优先树搜索BFS方法如Reprover、BFS-Prover。这类方法将证明过程建模为状态空间搜索。模型在每一步生成多个可能的后续策略通过一个价值函数评估哪个状态更接近证明完成然后像下棋一样展开搜索树。这种方法与Lean环境交互紧密每一步都要验证搜索效率是瓶颈。全证明生成方法如STP、Goedel-Prover、Leanabell-Prover、DeepSeek-Prover-V2、Kimina-Prover。这类方法让模型直接一次性生成整个证明脚本可能包含多个策略然后交给Lean一次性验证。这减少了交互开销但对模型的规划能力要求极高。评测使用PassK指标即在前K个生成结果中至少有一个能通过Lean验证的比例。对于子目标补全这种期望快速响应的任务论文特别关注低计算预算下的表现如Pass1 Pass4这比看Pass256更有实际意义。5.2 核心结果与发现整体表现远未达到实用化要求在最具实际意义的Pass1指标上表现最好的模型STP也仅为26.96%。这意味着在数学家最希望的“一次生成即成功”的场景下现有模型的可用性很低。即使放宽到Pass32生成32个证明尝试取最好的最高通过率也只在63%左右仍有超过三分之一的问题无法解决。检索能力是分水岭在需要前提检索的子集上模型的性能普遍下降。但DeepSeek-Prover-V2无论是否开启CoT展现了显著的检索优势在提供10个候选前提时Pass32相比无检索设置提升了约10%。论文分析认为这得益于其在海量自然语言推理数据上的训练增强了其通用推理和关联能力使其能更好地从候选列表中识别出有用的引理。“专家迭代”的有效性论文尝试对DeepSeek-Prover-V2和Goedel-Prover-V2在FormalML及相关数据上进行了一轮“专家迭代”训练。具体做法是让模型对大量问题生成多个候选证明自动筛选出正确的证明然后用这些问题正确证明数据对模型进行微调。结果显示微调后的模型在Pass1上取得了超过20个百分点的巨大提升。这强烈表明针对子目标补全任务进行定向训练是大幅提升模型实用性的有效途径。效率对比鲜明在EWA32效率加权准确率指标上STP模型一骑绝尘。它生成的证明通常非常简短直接几乎没有冗余的自然语言推理因此平均响应长度最短同时通过率最高综合效率得分最优。与之相对DeepSeek-Prover-V2 (CoT) 和 Kimina-Prover 等模型虽然可能生成更“人性化”的推理步骤但过长的输出严重拉低了其效率评分。这对于需要快速交互的辅助场景来说是一个重要的权衡考量。5.3 不同领域与难度下的表现差异评测还揭示了模型表现的不均衡性。在优化理论如梯度下降证明和概率论如McDiarmid不等式的不同子领域各模型的表现排名波动很大。例如STP在McDiarmid不等式相关问题上表现突出而DeepSeek-Prover-V2在霍夫丁不等式上更胜一筹。这说明现有模型可能对某些特定类型的数学结构或推理模式存在偏好或短板尚未形成通用的、稳健的证明能力。随着问题难度等级从1增加到5所有模型的性能都出现断崖式下跌。在难度5对应5行原始策略的问题上即使是最优模型Pass128尝试128次的通过率也仅为33%左右。这清晰地表明处理需要多步连贯推理的复杂子目标仍然是当前技术的难点。6. 对研究与实践的启示FormalML的建立初步评测为基于LLM的定理证明研究指明了几个清晰的未来方向任务范式的转变研究社区需要从一味追求“竞赛式”的全证明生成转向更贴近实用的“助手式”子目标补全。这要求模型设计更注重上下文理解、精准检索和高效生成。训练数据的针对性专家迭代实验的成功说明用高质量的子目标补全数据对模型进行微调能显著提升其在此任务上的表现。未来需要构建更大规模、覆盖更广数学领域的子目标补全数据集。检索与推理的深度融合如何让模型像数学家一样在证明过程中动态、精准地调用已知定理是一个关键问题。需要探索比简单提供候选列表更先进的检索增强生成架构。评估指标的完善除了通过率响应时间、证明长度、资源消耗等效率指标对于衡量一个“助手”是否实用至关重要。EWA指标是一个很好的开端。对于一线从事机器学习理论或形式化验证的研究者来说FormalML的出现是一个积极的信号。它意味着AI辅助证明工具正朝着解决真实科研痛点的方向演进。虽然目前模型的性能还不尽如人意但它提供了一个稳定的标尺可以持续追踪进展。也许不久之后我们就能在Lean中写下证明草图然后轻松地对AI说“帮我填上这个sorry。”——而FormalML正是推动我们走向那个未来的重要一步。我个人在尝试复现和使用类似工具时的体会是当前最大的障碍还不是模型的绝对能力而是工作流的整合。如何将这类证明补全模型无缝嵌入到VS Code的Lean插件中如何设计交互界面让数学家能方便地提供草图、查看模型生成的多个候选证明、并快速选择或编辑这些工程体验上的细节将最终决定这项技术能否被广泛采纳。FormalML作为一个基准主要解决了“评估什么”和“如何评估”的问题而“如何交付”则是下一个需要产学研共同攻坚的课题。