最近，OpenAI 的新模型在数学推理上的表现，成了数学圈和 AI 圈同时讨论的话题。很多人用“破防”来形容数学家的反应，其实真正让大家不安的，不是模型能解几道竞赛题，而是它开始进入“证明”这个原本被视为人类智力安全区的领域。这篇文章想从实测和工程角度拆一拆：新模型的数学能力到底该怎么看，数学家为什么会有危机感，以及普通开发者和研究人员该怎么把它接入自己的工作流。

下面按实际落地顺序拆一遍。

1. 这一波模型搅动的不是“算得快”，而是“证明”这件事本身

1.1 为什么数学界反应比普通用户更大

数学界对 AI 辅助其实并不陌生。符号计算、数值模拟、机器学习辅助猜想，这些方向已经存在很多年。数学家早就习惯让计算机帮忙算积分、验证公式、枚举反例。所以“模型能算得比我快”这个事，不会引起太大波澜。

这次讨论明显不同。大家关注的不再是“能不能算出结果”，而是“能不能给出一段像样的证明过程”。当一个模型能按照数学论文的写法，给出定义、引理、推导、结论，而且读起来逻辑连贯，很多人的第一反应不是“方便”，而是“我还能信任哪一步”。

这种反应可以理解。数学证明的价值不只是结论正确，还在于每一步都有据可查。人类读证明时，可以抽查中间环节，也可以尝试构造反例。如果这些工作由一个概率模型完成，那么即使答案看上去完美，你也很难确定它是不是在“一本正经地编造”。

所以我觉得，“破防”不是矫情，而是长期形成的专业判断力在提醒：这里出现了新的不确定性来源。问题是，这种不确定性并不等于模型没有用，而是要求使用者必须有一套新的验证方式。

1.2 从“ChatGPT 会做题”到“模型能写证明”，差在哪

过去我们测试大模型数学能力，更多是抛一道题，看它能不能给出最终数字。这种方式衡量的是“模式匹配”：模型可能见过类似题型，然后按照训练数据里的解法走一遍。

现在的讨论已经不一样了。模型不仅能给最终答案，还能给出结构完整的证明草稿。社区里讨论度很高的 Codex 相关仓库，研究焦点也不只是“模型能不能写代码”，而是能不能在真实工具链里完成多步骤任务，并且这个过程可以被复现、被检验。

这里的关键差异在于：

• 会解题：结果正确，但过程可能乱跳。
• 会写证明：结果正确，过程也像模像样，甚至能引用外部经验。
• 可验证的证明：每一步都能被人类或工具复查，没有隐藏假设。

绝大多数模型目前卡在第三层。它在第二层上的表现已经足以让很多人感到威胁，但真正的研究工作其实需要第三层。理解这个分层，你就不会被“模型能写出漂亮过程”这件事吓住。

2. 想验证一个模型的数学能力，不要只看聊天界面

2.1 先区分“算术强”和“推理强”

很多人看到模型能解微积分、能因式分解、能算出矩阵特征值，就认为它数学很厉害。这其实是把“算术强”和“推理强”混在了一起。

算术能力很大程度上是对大量题目的模式记忆。比如求导、展开、化简，这些规则固定，训练数据里都有类似表达。模型学习到的不是真正的计算规则，而是“在什么上下文里输出什么形式的式子”。大部分情况下它能做对，但遇到不常见的符号约定或异常输入时，就会露出破绽。

推理能力指的是：面对一个没有明显模板的问题，模型能不能根据新定义一步步推导，能不能主动排除反例，能不能在证明中途发现前提不足。

我建议你测试时，不要直接用网上已有的竞赛题。那些题目很可能出现在训练数据里。更好的做法是：

1. 把常见题目换一个符号体系。
2. 改变题目的约束条件。
3. 自己发明一个“新定义”，让模型在陌生规则下推导。

如果模型在这种情况下还能保持逻辑一致，才说明它有一定的推理能力。否则，它只是在“回忆”而不是“思考”。

2.2 构造一套自己能复现的数学测试样例

想验证模型能力，先从小样本开始。不要拿一百道题一次跑完，那样出了问题很难定位。

我会先构造一个只有五到八条测试用例的小集合，覆盖下面几类：

样例类型	考察能力	通过标准	常见失败
新定义下的性质推导	能否按新规则推理	能根据定义推出基本性质	直接套用旧公式
构造反例	能否否证一个命题	给出具体、可验证的反例	给出模糊的“可能不存在”
证明断点检查	能否识别跳步	明确指出某一步依赖什么	把等价关系写反
长链条推理	多步逻辑稳定性	中间结论前后一致	步骤之间冲突
条件不足判断	能否识别信息缺失	说“无法证明”而不是硬推	强行补充假设

每条样例跑三遍，观察输出是否稳定。数学任务一般建议把温度调低，比如 0 到 0.2。如果你发现同一个题目三次结果差很多，那这个模型在这一类问题上就不可靠。

这里可以写一个非常简单的批量调用思路，不限定具体 API 协议：

import json
import time

samples = [
    {"id": "case1", "prompt": "...", "expected_key": "..."},
    {"id": "case2", "prompt": "...", "expected_key": "..."},
]

def call_model(prompt, temperature=0.1):
    # 这里替换成你的模型调用方式
    pass

results = []
for s in samples:
    for round_idx in range(3):
        resp = call_model(s["prompt"])
        results.append({"id": s["id"], "round": round_idx, "output": resp})
        time.sleep(1)  # 避免请求过密

不要一上来就开大并发。先跑通单条，再看批量。否则一旦接口限流、超时、参数写错，你很难分清是模型问题还是工程问题。

2.3 跑通后的输出怎么判断

判断标准不是“结果对不对”，而是“过程能不能复现”。我会把模型输出拆成四部分：

• 结论：最终断言是什么。
• 关键引理：它用了哪些中间结论。
• 证明步骤：每一步是否逻辑连贯。
• 适用范围：有没有说明前提假设。

然后逐个检查。如果中间用到某个结论，但这个结论既不是公理，也没有被证明，那整个证明就有缺口。即使最终答案正确，也不能算有效推理。

还有一个很实用的测试方法：故意挑刺。你可以在模型给出的证明里找一步看起来可疑的地方，然后告诉模型“这步可能有问题，请重新检查”。看它是认真修订，还是坚持原来的表达，甚至开始自相矛盾。一个真正稳定推理的模型，至少会重新审视关键步骤；一个只会模式拼接的模型，往往会在同样的地方绕圈。

这个过程本身就是“验证分离”的雏形：你不要让模型既当运动员又当裁判，而是把“生成答案”和“检查答案”分成两件事。

3. 真正让数学家焦虑的，是“过程不可见”

3.1 模型给出正确结论，但证明过程可能是“幻觉式严谨”

语言模型的核心机制，是根据上文预测下一个最合适的 token。它没有一套确定的公理系统，也没有一个严格的推理引擎。所谓证明过程，很像一个受过大量数学训练的助理在“模拟严谨”。

这就产生了一个诡异的现象：模型给出的证明，可能整体结构完整，局部却引用了一个不存在的定理，或者把两个不同概念混在一起。你如果不逐行验证，很容易被它的语气说服。

这种问题在学术写作里特别危险。因为数学论文本来就要靠“信任”传递信息：作者写了一个引理，读者不会每次都用形式化工具重新验证。如果模型生成的文本能跳过这种信任，就会在文书中埋下隐蔽错误。

所以，数学家说“过程不可见”，指的不是界面不透明，而是模型内部没有提供一个可以审计的推理路径。你只能看到输出，看不到它为什么走这条路。

3.2 用“验证分离”消化不确定性

既然过程不可见，那解决办法就是不让“过程”停留在模型内部。把模型生成的结果当成一个候选草稿，然后进入独立验证流程。

一个比较实用的流程是：

1. 模型生成证明草稿。
2. 将草稿拆成“结论、前提、中间步骤”三部分。
3. 人为抽查最重要的几个跳转。
4. 用外部工具或反例检查关键断言。
5. 最后再让模型根据检查意见生成修订版。

这里要特别注意：不要直接问模型“这个证明对不对”，因为模型会因为对话惯性而倾向于确认自己生成的内容。更好的提问方式是：

“请把这个证明中最容易站不住脚的三步单独列出来，并说明每一步依赖什么前提。”

这样更容易暴露信息缺口。你也可以让模型把“我假设了什么”列成清单，然后由人来判断这些假设是否成立。

如果你在搭建验证环境，可能会用到检索或向量模型来查找资料。这时候要注意，embedding 和 reranker 这类模型，和生成模型是不同的体系。有些推理框架对大语言模型支持很好，但对 embedding 和 reranker 的支持不完整，甚至无法直接启动。搭建前先确认框架版本和模型架构，别默认能直接跑。

3.3 典型报错与排查顺序：从输入到输出，再到环境依赖

不管你是用 API 还是本地部署，都会遇到模型表现不佳的情况。先别急着换参数，按这个顺序排查：

优先级	检查点	具体动作
1	输入	题目是否有歧义？条件是否完整？符号是否冲突？
2	上下文	是否超过模型上下文长度？论文片段是否被截断？
3	采样参数	temperature 是否过高？max_tokens 是否不够？
4	模型版本	是同一个模型吗？量化版本是否导致推理能力下降？
5	部署环境	框架是否支持该模型？资源是否不足？API 是否超时？

一个常见坑是：模型第一步概率很高，到了第十步却因为上下文太长开始忘掉前提。这时候把温度调到 0 也没用，应该拆分问题，让模型先证明一个小引理，再进入主证明。

另一个常见坑是：本地部署了一个量化版本，感觉模型“变笨了”。数学推理对精度很敏感，8bit 有时候还好，更低的量化可能让复杂推理明显退化。如果只是学习，默认配置够用；如果要验证论文级证明，就要单独确认部署方式和精度。

4. 从“破防”到“接入”：数学研究的新工作流

4.1 把模型当“第二轮审稿人”

我自己最喜欢的用法，不是让模型直接给答案，而是让它扮演一个“苛刻的读者”。

比如你写好了一段证明，可以让模型读一遍，然后问它：

“如果你是这个证明的审稿人，你会卡在哪一步？哪些地方需要补充解释？”

这个问题比“这个证明对不对”有效得多。模型即使没有判断最终正确性的能力，也能发现语言层面的模糊、结构上的跳跃和缺少前置条件的地方。

这个过程相当于把模型当成第二轮审稿人。第一轮是作者自己，第二轮是人类同事，第三轮是期刊审稿人。模型可以作为第二轮的补充，帮你把粗糙的草稿打磨得更完整。但你不能让它当最终裁决者，因为它没有长期记忆，也没有稳定的公理体系。

4.2 本地部署与 API 调用的边界

在新模型刚出来的时候，很多人都会纠结：是用 API 还是本地部署。我的建议是分阶段看。

场景	推荐方式	原因
快速验证模型能力	API	版本新、部署快、适合一次性测试
频繁跑批量实验	API + 缓存	节省本地资源，但要注意成本和配额
涉及未公开数据	本地部署	数据不出内网，隐私更可控
调试和二次开发	本地部署	可以方便修改推理参数和流程

如果你使用的是兼容 API，还要特别注意协议差异。不同服务商虽然都宣称兼容 OpenAI API，但字段命名、超时行为、返回结构可能不一样。测试时先打印完整返回结果，不要只读取某个字段。

4.3 生产环境里的参数、超时和资源控制

一旦进入正式流程，就要考虑一个真实生产问题：请求一定会失败，模型一定会偶尔抽风。所以你必须给批量任务设计失败重试和日志记录。

几个关键参数可以参考：

参数	推荐范围	说明
temperature	0 ~ 0.2	数学任务要低，减少随机性
max_tokens	1024 ~ 4096	根据题目复杂度和输出长度调整
timeout	30s ~ 120s	长证明可能耗时较长
retries	2 ~ 3 次	网络抖动和临时错误可重试
并发	1 ~ 5 起始	不要刚上线就拉满

配置示例：

{
  "temperature": 0.1,
  "max_tokens": 2048,
  "timeout": 60,
  "retries": 3,
  "concurrency": 3,
  "output_dir": "./results"
}

这里最容易被忽略的是输出命名。批量跑数学题时，每道题可能有多个版本、多轮修订。如果输出文件没有清晰的命名规则，后续很难回溯问题。我一般会把“题目 ID + 模型版本 + 采样轮次 + 时间戳”拼进文件名，这样即使某次结果很奇怪，也能快速定位到当时的输入和参数。

5. 数学家真正需要补的技能，不是写提示词

5.1 理解模型的概率本质，比背诵提示词更重要

网上有很多提示词模板，看起来能让你“调教”模型给出更好的数学答案。但如果你不理解模型本质，换一个问题、换一个模型，模板可能就失效了。

我理解模型的方式很简单：它是一个根据前文预测下一个词的大规模概率系统。它不是数学软件，也不等于形式化证明工具。你让它证明一个定理，它做的事情是在高维空间中“拼出”一段看起来合理的推导。

所以真正要掌握的技能是“如何让模型暴露推理过程”，而不是“如何让它输出一个漂亮结果”。你可以要求它把每一步推理写完整，要求它显式列出假设，要求它在不确定时表明不确定性。

好的提示词往往是这样的：

“请逐步推理。每一步都要说明你使用了哪个定义或定理。如果你遇到不确定的地方，直接说明，不要跳过。最后列出这个证明成立的前提条件。”

这个提示词的核心不是“指导模型”，而是“逼迫模型把内部不确定性暴露出来”。这样你才有机会审查。

5.2 建立“人工验证闭环”

长期使用 AI 辅助数学研究，不能只靠“模型结果 + 肉眼判断”。最好建立一个明确的验证闭环。

一个可落地的闭环是：

1. 模型生成候选证明。
2. 人工抽取三个关键断言。
3. 分别验证这三个断言是否成立。
4. 把验证结果回传给模型，要求修订。
5. 重复直到找不到新的反例或断点。

在这个闭环里，模型负责效率，人类负责判断。你不需要阻止模型犯错，因为犯错的成本可以通过验证环节控制。你真正需要阻止的，是“未经验证就把模型输出当作结论”。

5.3 适合长期投入的方向：验证器、形式化证明、协同工具

如果你真的对“模型 + 数学”感兴趣，而不是只想吃瓜，我建议往三个方向投入。

第一个方向是给模型生成的内容做验证器。你可以写一个小工具，自动检查证明文本里的名词引用，或者用符号计算库验证某个具体结论。这类工具不需要多复杂，但能极大提高检查效率。

第二个方向是学习形式化证明。Lean、Coq、Isabelle 这些工具可以让证明变成机器可验证的步骤。如果模型生成的自然语言证明能被翻译成形式化证明，那就真正进入了“可审计推理”的范畴。这条路门槛不低，但值得关注。

第三个方向是把模型当成“数学实验员”。让模型快速跑大量例子，寻找模式和反例，然后再由人类证明这些观察是否成立。这个方向不追求让模型一步到位，而是让它成为你的计算助手。

这些方向都不需要你“放弃数学直觉”。相反，它们要求你更精确地表达直觉，更清楚地区分“猜测”和“证明”。

6. 写在最后：危机感会留下什么

回到最初的“破防”情绪。我觉得它不会持续太久，也不会毫无意义。它会让一部分人认真思考：当模型能写出看似合理的证明时，我们如何维持学术生产中的严谨性？

答案不是关掉模型，也不是无条件信任模型，而是建立更清晰的验证边界。

我个人更建议先把单任务跑稳，再考虑批量和接口。先看输出质量和稳定性，再开高并发。先有验证方案，再谈 AI 辅助。这比一味追求“最新模型”更重要。

踩过几次之后我发现，很多问题不是模型能力不够，而是前置环境和输入材料没有处理干净。你给模型一个有歧义的问题，它就会给你一个看似肯定但实际模糊的答案。你让它在不合适的上下文长度下强行推导，它就会在长链条中丢失线索。

这些都不是“模型要替代数学家”的证据，而是说明：工具越强，使用者的判断标准越要清晰。数学家真正要守住的，不是“只有人类会证明”的幻觉，而是“每一步都经得起质问”的底线。