> 论文: Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game > 作者: Lixing Li > arXiv: 2605.00677 | 2026-04-30
---
一、那个"记住答案"的数学天才
想象一个学生，在数学竞赛中拿了满分。
但你怀疑：他是真的理解数学，还是背下了所有题目的答案？
怎么测试？
- 给他新题目？可能他见过类似的
- 换数字？可能他掌握了模式
- 把数学概念重命名——把"加法"叫"合并"，把"乘法"叫"重复合并"——然后看他还能不能推理？
---
二、LLM数学能力的"真假之辩"
LLM在形式数学基准（如MiniF2F）上取得了令人印象深刻的成绩。
但关键问题：这些成功来自真正的逻辑推理，还是训练数据中的语义模式匹配？
现有基准的局限：
- 测试题目可能出现在训练数据中
- 即使没出现，类似的题目模式可能见过
- 无法区分"推理"和"记忆"
- 测试LLM在"陌生"数学域中的推理能力
- 不是测试它"知道什么"，而是测试它"能推导什么"
- 从已知公理和定义出发，不看任何外部知识
三、混淆自然数游戏：LLM推理能力的试金石
这篇论文提出 Obfuscated Natural Number Game：
核心思想： > 把Lean中的自然数游戏的所有标识符重命名，测试LLM是否仍然能完成证明。
具体操作： 1. 拿Lean的自然数游戏（一个交互式定理证明教程） 2. 把所有标识符（函数名、定理名、变量名）替换为无意义的符号
- "add" → "f₁"
- "mul" → "f₂"
- "succ" → "g"
- ...
测试目标：
- LLM是否理解自然数的结构（如皮亚诺公理）？
- 还是只是记住了定理的名字和证明步骤？
- 在陌生符号下，能否从第一原理出发推理？
四、为什么混淆测试有效？
如果LLM只是背诵：
- 它记得"用add_comm来证明"
- 但add_comm被重命名为f₇
- 它就无法调用这个定理
- 证明失败
- 它理解加法交换律的内容
- 即使名字叫f₇，它也能从公理推导出来
- 或者至少知道"这里需要一个交换律"
- 证明可以继续
- 给他一套全新的符号系统
- 看他是否仍然能建立数学理论
- 真正的数学家可以，背诵者不行
五、费曼式的判断：理解意味着能在陌生环境中应用
费曼说过：
> "知道一个东西的名字"和"真正理解一个东西"是完全不同的。你可以知道鸟的名字全世界有100万种，但你对鸟一无所知。"
在数学推理中：
> "知道定理的名字和证明步骤，不等于理解定理。真正的理解意味着：即使所有名字都变了，你仍然能从基本原理出发重建一切。"
混淆自然数游戏的哲学是：剥离所有表层记忆，测试深层理解。
- 名字可以变
- 符号可以变
- 但逻辑结构不变
- 真正的推理者能在任何符号系统中工作
六、带走的启发
如果你在评估或使用LLM的推理能力，问自己：
1. "我的测试是否区分了'记忆'和'推理'？" 2. "LLM在陌生符号/概念下是否仍然能推导？" 3. "我是否测试了'从第一原理出发'的推理能力？" 4. "评估方法是否足够严格，排除了训练数据污染？"
这篇论文的核心启示：评估AI推理能力，需要设计能排除"记忆作弊"的测试。
混淆自然数游戏提供了一个优雅的方案：不改变数学内容，只改变表示方式。如果AI仍然能推理，它就是真正理解了。如果不能，它就是高级背诵者。
在AI数学能力突飞猛进的今天，区分"真懂"和"假懂"比以往任何时候都更重要。
#LLMReasoning #FormalMathematics #TheoremProving #Evaluation #LeanProver #FeynmanLearning #智柴AI实验室