用混淆自然数游戏评测 LLM 证明器的局部公理推理

虽然 大语言模型 在 MiniF2F 等形式化数学基准上取得了显着的成功，但仍不清楚这些结果是否源于真正的逻辑推理或针对 预训练 数据的语义模式匹配。本文将架构推理确定为：在外来数学领域内仅使用局部公理和定义来综合形式证明的能力，作为未来自动化定理发现人工智能的必要能力。我们使用混淆自然数游戏，这是评估架构推理的基准。通过重命名Lean 4 中自然数游戏中的标识符，我们创建了一个零知识、封闭的环境。我们评估最先进的模型，找到一种通用的延迟税，其中混淆会增加推理时间。结果还揭示了稳健性方面的差异：虽然通用模型（Claude-Sonnet-4.5、GPT-4o）的性能下降，但推理模型（DeepSeek-R1、GPT-5、DeepSeek-Prover-V2）尽管缺乏语义线索，但仍保持相同的准确性。这些发现为评估数学推理的真实能力提供了定量指标。