🔢 自然数游戏的"加密版"：LLM是在推理还是背诵？

> **论文**: 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" - ... 3. 保留所有公理和定义的逻辑结构 4. 让LLM在这个"混淆"的环境中完成证明 **测试目标：** - LLM是否理解自然数的**结构**（如皮亚诺公理）？ - 还是只是记住了定理的名字和证明步骤？ - 在陌生符号下，能否从第一原理出发推理？ --- ## 四、为什么混淆测试有效？ **如果LLM只是背诵：** - 它记得"用add_comm来证明" - 但add_comm被重命名为f₇ - 它就无法调用这个定理 - 证明失败 **如果LLM真正推理：** - 它理解加法交换律的内容 - 即使名字叫f₇，它也能从公理推导出来 - 或者至少知道"这里需要一个交换律" - 证明可以继续 **这就像测试一位数学家：** - 给他一套全新的符号系统 - 看他是否仍然能建立数学理论 - 真正的数学家可以，背诵者不行 --- ## 五、费曼式的判断：理解意味着能在陌生环境中应用 费曼说过： > **"知道一个东西的名字"和"真正理解一个东西"是完全不同的。你可以知道鸟的名字全世界有100万种，但你对鸟一无所知。"** 在数学推理中： > **"知道定理的名字和证明步骤，不等于理解定理。真正的理解意味着：即使所有名字都变了，你仍然能从基本原理出发重建一切。"** 混淆自然数游戏的哲学是：**剥离所有表层记忆，测试深层理解。** - 名字可以变 - 符号可以变 - 但逻辑结构不变 - 真正的推理者能在任何符号系统中工作 --- ## 六、带走的启发 如果你在评估或使用LLM的推理能力，问自己： 1. "我的测试是否区分了'记忆'和'推理'？" 2. "LLM在陌生符号/概念下是否仍然能推导？" 3. "我是否测试了'从第一原理出发'的推理能力？" 4. "评估方法是否足够严格，排除了训练数据污染？" **这篇论文的核心启示：评估AI推理能力，需要设计能排除"记忆作弊"的测试。** 混淆自然数游戏提供了一个优雅的方案：不改变数学内容，只改变表示方式。如果AI仍然能推理，它就是真正理解了。如果不能，它就是高级背诵者。 在AI数学能力突飞猛进的今天，区分"真懂"和"假懂"比以往任何时候都更重要。 #LLMReasoning #FormalMathematics #TheoremProving #Evaluation #LeanProver #FeynmanLearning #智柴AI实验室