Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game

📄 arXiv: 2605.00677v1 📥 PDF

作者: Lixing Li

分类: cs.LG

发布日期: 2026-05-01

备注: 4 pages. Accepted as a short paper to the AAAI 2026 Spring Symposium on Machine Learning and Knowledge Engineering for Knowledge-Grounded Semantic Agents (MAKE 2026)

💡 一句话要点

提出建筑推理能力评估方法以解决大型语言模型的推理能力不确定性问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 建筑推理 模糊自然数游戏 自动定理证明 数学推理能力评估

📋 核心要点

  1. 现有大型语言模型在数学推理能力的评估中存在不确定性，难以区分逻辑推理与模式匹配的贡献。
  2. 论文提出了建筑推理的概念，并通过模糊自然数游戏创建了一个闭合环境来评估这一能力。
  3. 实验结果显示，推理模型在模糊化条件下保持准确性，而一般模型则出现性能下降，揭示了模型的鲁棒性差异。

📝 摘要（中文）

尽管大型语言模型在正式数学基准测试中取得了显著成功，但尚不清楚这些结果是否源于真正的逻辑推理或仅仅是对预训练数据的语义模式匹配。本文提出建筑推理的概念，即在陌生数学领域中仅使用局部公理和定义合成正式证明的能力，作为未来自动定理发现AI所需的能力。通过使用模糊自然数游戏作为基准，我们评估了最先进的模型，发现模糊化会增加推理时间，并揭示了模型在鲁棒性上的差异。

🔬 方法详解

问题定义：本文旨在解决大型语言模型在数学推理能力评估中的不确定性，尤其是如何区分逻辑推理与语义模式匹配的贡献。现有方法未能有效评估模型在陌生数学领域的推理能力。

核心思路：论文提出建筑推理的概念，强调在陌生数学领域中仅依赖局部公理和定义进行推理的能力。通过模糊自然数游戏，创建一个零知识的闭合环境，以便更准确地评估模型的推理能力。

技术框架：整体架构包括模糊自然数游戏的设计、模型的评估流程以及性能对比分析。主要模块包括模型输入的模糊化处理、推理过程的监测和结果的准确性评估。

关键创新：最重要的创新点在于通过模糊化处理创建一个闭合环境，使得模型在缺乏语义线索的情况下仍能进行推理。这与现有方法的本质区别在于强调了模型的内在推理能力，而非依赖外部信息。

关键设计：在实验中，使用了不同的模型（如Claude-Sonnet-4.5、GPT-4o等）进行对比，关键参数包括模糊化程度和推理时间的测量，损失函数设计为评估模型在模糊环境下的准确性。

🖼️ 关键图片

fig_0

📊 实验亮点

实验结果显示，推理模型（如DeepSeek-R1、GPT-5、DeepSeek-Prover-V2）在模糊化条件下保持了与原始环境相同的准确性，而一般模型（如Claude-Sonnet-4.5、GPT-4o）则出现了性能下降，表明推理模型在鲁棒性方面具有显著优势。

🎯 应用场景

该研究的潜在应用领域包括自动定理证明、数学教育工具以及智能助手的开发。通过提高模型在陌生领域的推理能力，可以推动数学研究的自动化进程，提升教育工具的智能化水平，具有重要的实际价值和未来影响。

📄 摘要（原文）

While Large Language Models have achieved notable success on formal mathematics benchmarks such as MiniF2F, it remains unclear whether these results stem from genuine logical reasoning or semantic pattern matching against pre-training data. This paper identifies Architectural Reasoning: the ability to synthesize formal proofs using exclusively local axioms and definitions within an alien math domain, as the necessary ability for future automated theorem discovery AI. We use the Obfuscated Natural Number Game, a benchmark to evaluate Architectural Reasoning. By renaming identifiers in the Natural Number Game in Lean 4, we created a zero-knowledge, closed environment. We evaluate state-of-the-art models, finding a universal latency tax where obfuscation increases inference time. The results also reveal a divergence in robustness: while general models (Claude-Sonnet-4.5, GPT-4o) suffer performance degradation, reasoning models (DeepSeek-R1, GPT-5, DeepSeek-Prover-V2) maintain the same accuracy despite the absence of semantic cues. These findings provide a quantitative metric for assessing the true capacity for mathematical reasoning.