数学证明作为检验指纸：揭示先进大型推理模型的失效模式
人工智能
2025-12-10 v4
摘要
大型推理模型（如 R1、o3）在数学问题解决方面展现出显著能力。然而，这些先进模型在热门数据集上的高报告准确率、依赖纯数值评估以及潜在的基准泄漏，往往掩盖了其真正的推理不足之处。为此，我们提出以数学证明的内在严谨性和方法论复杂性作为诊断工具，以暴露这些隐藏的失败。具体而言，我们引入了 RFMDataset（揭示失效模式），收录 200 个多样化的数学证明问题，并彻底评估了先进模型在其上的表现。我们的深入分析揭示了 10 种细粒度错误类型，显示当前大型推理模型存在根本性局限：1）大型推理模型在数学证明方面面临严峻挑战，其中一些模型在解决问题时几乎得不到正确证明，且即便在基础问题上也常常失败；2）模型表现出多样化的推理失效模式，突出显示其在单步推理的正确性和严谨性方面缺乏保障；3）模型在推理过程中表现出幻觉和不完整现象。我们的发现表明，模型的自我反思在解决当前逻辑困境方面不足， necessitating 通过形式化和细粒度的逻辑训练来弥补。
引用
@article{arxiv.2506.17114,
title = {Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models},
author = {Dadi Guo and Jiayu Liu and Zhiyuan Fan and Zhitao He and Haoran Li and Yuxin Li and Yumeng Wang and Yi R. Fung},
journal= {arXiv preprint arXiv:2506.17114},
year = {2025}
}