评估大语言模型证明器的架构推理能力：混淆自然数游戏的启示

本文通过混淆自然数游戏基准测试，评估大语言模型在零知识环境下的架构推理能力。核心发现：推理模型（如DeepSeek-R1、GPT-5）去除语义线索后仍保持准确率，通用模型性能下降。研究旨在区分模型是依赖语义模式匹配还是真正的逻辑推理能力。

大语言模型在MiniF2F等形式化数学基准上进展显著，但成功源于逻辑推理还是语义模式匹配存疑。研究者提出"架构推理"概念——陌生数学领域仅靠局部公理定义合成证明的能力，这是自动化定理发现AI的核心技能。

基于Lean4自然数游戏构建测试环境，通过重命名所有标识符（类型、函数、定理、变量）形成零知识封闭环境。模型无法依赖预训练数学知识，需仅靠局部公理推理。设计隔离语义模式匹配与架构推理能力，若模型混淆后性能下降则依赖语义记忆，反之则具备架构推理能力。

所有模型面临"延迟税"（推理时间增加）。通用模型（Claude-Sonnet-4.5、GPT-4o）混淆后性能明显下降，依赖语义线索；推理模型（DeepSeek-R1、GPT-5、DeepSeek-Prover-V2）准确率稳定，具备抽象推理能力，不依赖特定领域先验知识。

架构推理含公理理解、策略发现、组合探索、错误恢复四要素，不仅是符号操作。自动化定理发现AI需探索未知数学领域，无预训练语义知识，依赖架构推理构建新理论。

传统基准可能高估模型真实能力（若数据与预训练重叠则靠记忆）；混淆测试有效评估真正推理能力；需探索新领域的应用（科学发现、形式化验证）应选推理模型，即使常规基准分数相近。

Lean4是强大定理证明助手，自然数游戏为交互式教育环境。混淆策略：类型名替换随机字符串、函数操作符用无意义标识符、定理名匿名化、变量名统一生成符号，确保模型无法利用外部知识。

扩展混淆测试到代码合成、逻辑谜题、科学推理；设计更好训练策略（多样化形式化环境训练增强通用推理）；推动人机协作定理发现（推理模型辅助人类探索新数学领域）。