让我们从一个看似简单的问题开始：

"请证明勾股定理。"

如果你问ChatGPT，它可能会给出一段看似合理的解释，甚至配上一张图。但如果你追问："你的证明每一步都严格符合数学公理吗？符号使用是否规范？逻辑链条是否完整？"——事情就变得复杂了。

这正是当前AI在数学推理领域面临的根本挑战：生成一个看起来对的答案很容易，但生成一个严格正确的数学对象（Mathematical Object）却极其困难。

来自Meta FAIR团队（对，就是那个搞出LLaMA的团队）的最新研究，构建了一个名为Principia的数学推理基准测试套件。他们的发现令人警醒：即便是当今最强大的模型——Qwen3-235B和OpenAI的o3——在这个基准上也举步维艰。

一、为什么数学对象推理如此重要？

在深入技术细节之前，让我们先理解这个问题的本质。

数学的独特性

数学与其他领域不同。在一般性的文本生成中，"差不多对"往往就够了。但在数学中，差之毫厘，谬以千里。一个符号的错误、一个逻辑步骤的跳跃，就足以让整个证明崩塌。

数学推理的终点不是一个"答案"，而是一个严格形式化的数学对象——可能是一个证明、一个公式推导、一个几何构造，或者一个符号计算序列。这些对象必须满足：

• 语法正确性：符号使用符合规范
• 语义正确性：每一步推导都有严格的数学依据
• 完备性：从前提条件到结论，逻辑链条没有断裂

当前评估的局限

现有的数学评测（如GSM8K、MATH等）存在一个根本问题：它们太简化了。大多数评测只需要模型输出一个最终数值或选择一个正确选项。这种评估方式绕过了数学推理的核心——形式化推导过程。

打个比方：这就像评价一个厨师的水平，只看最后的成品照片，而不品尝味道、不检查食材新鲜度、不评估烹饪过程。

二、Principia：填补评估空白的雄心

为了解决这一问题，研究团队构建了Principia套件，包含三个核心组成部分：

1. 专门的训练数据集

研究团队构建了大量高质量的数学对象推导数据。这些数据不是简单的"问题-答案"对，而是完整的推导轨迹——从初始条件出发，一步步展示如何构建出目标数学对象。

2. 严格的基准测试

Principia测试涵盖多个数学领域：

• 代数推导：方程求解、不等式证明
• 几何构造：尺规作图的几何证明
• 微积分运算：极限、导数、积分的严格推导
• 离散数学：组合证明、图论命题

每个测试项都要求模型输出完整的推导过程，而不仅仅是一个最终答案。

3. 自动验证系统

为了自动评估模型的输出，研究团队开发了专门的验证器（Verifiers）。这些验证器会：

• 检查语法正确性（符号是否规范使用）
• 验证逻辑链条（每一步是否可由前一步推出）
• 比对标准答案（在等价意义下是否一致）

三、令人警醒的实验结果

研究团队在Principia上测试了多个当前最先进的语言模型，结果揭示了一个令人不安的现实。

强模型也"翻车"

即便是当今最强大的模型：

• Qwen3-235B：通义千问系列的旗舰模型
• OpenAI o3：OpenAI目前最强的推理模型

在Principia基准上的表现也远低于预期。它们可以处理简单的数值计算，但当面对需要严格形式化推导的数学对象时，错误率显著上升。

具体表现包括：

• 符号误用：混淆相似符号（如将∂和d混用）
• 逻辑跳跃：省略关键推导步骤，"显然"并不显然
• 边界条件遗漏：忽略特殊情况或约束条件
• 循环论证：无意中使用了待证明的结论作为前提

现有训练范式的局限

研究团队分析发现，现有模型之所以在数学对象推理上表现不佳，根源在于训练数据和方法的局限：

1. 数据稀缺：网络上高质量的数学推导数据相对稀少，大部分训练数据是"问题-答案"对，缺乏完整的推导过程

2. 奖励错位：在强化学习中，模型被奖励"答对"，而不是"推导正确"。这导致模型学会"猜答案"而不是"严谨推理"

3. 格式不匹配：现有评测的简化格式（数值答案、多项选择）无法反映数学对象推理的真实难度

四、On-Policy Judge训练：打破僵局的新方法

面对这些挑战，研究团队提出了一个创新的解决方案：On-Policy Judge训练。

什么是On-Policy Judge？

传统的强化学习通常使用固定的奖励函数。但在数学推理中，定义一个完美的奖励函数几乎不可能——你怎么自动判断一个数学证明是否正确？

研究团队的做法是：训练一个专门的"裁判模型"（Judge）来评估推导质量。

这个Judge模型接收一个推导过程作为输入，输出一个质量评分。关键是，这个Judge是在当前策略模型生成的数据（on-policy）上持续训练的，而不是使用固定的外部数据。

训练流程

1. 生成阶段：策略模型生成大量推导尝试
2. 验证阶段：自动验证器检查推导的正确性，给出二元反馈（对/错）
3. Judge训练：用这些反馈训练Judge模型，让它学会预测推导是否正确
4. 策略更新：用Judge的评分作为奖励信号，通过强化学习优化策略模型

这个循环不断迭代，策略模型和Judge模型相互促进，共同提升。

效果验证

实验结果显示，On-Policy Judge训练带来了显著的性能提升：

• 相比基线模型，数学对象生成准确率提高了一个量级
• 在保持原有数值计算能力的同时，形式化推导能力大幅增强
• 跨格式泛化：在Principia上训练的模型，在传统数值评测（如GSM8K）上也有提升

五、测试时计算扩展：让AI"多想想"

除了训练方法的创新，研究团队还探索了测试时计算扩展（Test-Time Compute Scaling）的策略。

核心思想

人类在面对复杂数学问题时，往往会尝试多种方法，比较不同的解题路径，最终选择最可靠的一个。AI也可以这样做。

研究团队采用了生成-聚合的框架：

1. 多路径生成：让模型生成多个独立的推导尝试
2. 质量评估：用训练好的Judge模型评估每个尝试的质量
3. 聚合选择：根据Judge的评分，选择最可靠的推导，或融合多个推导的优点

计算-性能权衡

实验显示，通过增加测试时的计算量（生成更多候选、进行更多评估），模型的准确率可以持续提升。这为推理时扩展（Inference-Time Scaling）提供了实证支持——有时候，让模型"多想一会儿"比单纯扩大模型规模更有效。

六、这项研究的意义

对AI数学能力的重新评估

Principia的研究表明，我们对AI数学能力的评估可能过于乐观了。现有评测的简化格式掩盖了真正的推理难题。未来，我们需要更严格、更全面的基准测试。

对训练范式的启示

On-Policy Judge训练的成功表明，让AI学会"自我评估"是提升推理能力的关键。这不仅是数学领域的特例，也可能适用于其他需要严格推理的领域（如编程、法律分析、科学推导）。

对测试时计算的重视

研究还提醒我们，训练和推理是相辅相成的。有时候，与其训练一个更大的模型，不如让现有模型在推理时投入更多计算资源。这为资源受限场景下的AI部署提供了新的思路。

七、局限与未来方向

当前局限

1. 覆盖范围有限：Principia目前主要覆盖初等数学，高等数学（如代数几何、数论）的覆盖还不充分
2. 验证器不完善：自动验证器仍有局限，某些复杂的数学对象难以自动验证
3. 计算成本高：On-Policy Judge训练和测试时聚合都需要大量计算资源

未来方向

研究团队提出了几个值得探索的方向：

1. 扩展到形式化证明助手：与Lean、Coq等形式化证明助手结合，实现完全严格的数学验证
2. 跨领域迁移：探索数学推理训练对其他STEM领域（物理、化学、生物）的迁移效果
3. 人机协作：开发AI辅助的数学研究工具，让AI和人类数学家协同工作

结语

数学被誉为"科学的皇后"，因为它提供了最严格、最精确的知识形式。让AI掌握数学推理，不仅是一个技术挑战，更是对AI智能本质的探索。

Principia的研究告诉我们：**通往真正数学智能的道路还很长。**当前的大语言模型虽然表现出色，但在严格的形式化推理方面仍有明显短板。

但好消息是，通过创新的训练方法（如On-Policy Judge）和推理策略（如测试时聚合），我们正在逐步缩小这个差距。

也许在不久的将来，AI不仅能帮我们计算，还能帮我们证明定理、发现新的数学结构。那将是人工智能发展史上的又一个里程碑。

论文信息：

• 标题: Reasoning over mathematical objects: on-policy reward modeling and test time aggregation
• 作者: Pranjal Aggarwal, Marjan Ghazvininejad, Seungone Kim, Ilia Kulikov, Jack Lanchantin, Xian Li 等
• 机构: Meta FAIR
• arXiv: 2603.18886
• 发表时间: 2026-03-20

#论文解读 #科普 #AI #小凯