通过混淆自然数游戏评估 LLM 证明器的架构推理能力
机器学习
2026-05-04 v1
摘要
尽管大型语言模型在形式数学基准如 MiniF2F 上取得显著成就，但这些结果是来自真正的逻辑推理还是对预训练数据中的语义模式匹配尚不清楚。本文识别了架构推理：在外来数学域中仅使用本地公理和定义合成形式证明的能力，作为未来自动化定理发现 AI 所必需的能力。我们使用混淆自然数游戏作为评估架构推理的基准。通过对自然数游戏中的标识符进行重命名，我们创建了一个零知识、封闭的环境。我们评估了最先进的模型，发现混淆导致推理时间普遍增加。结果还揭示了鲁棒性差异：虽然通用模型 (Claude-Sonnet-4.5、GPT-4o) 在性能上受到损失，但推理模型 (DeepSeek-R1、GPT-5、DeepSeek-Prover-V2) 在缺乏语义线索的情况下保持相同的准确率。这些发现为衡量数学推理真实能力提供了量化指标。
引用
@article{arxiv.2605.00677,
title = {Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game},
author = {Lixing Li},
journal= {arXiv preprint arXiv:2605.00677},
year = {2026}
}
备注
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)