ACL2026
Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models
Dadi Guo, Jiayu Liu, Zhiyuan Fan, Zhitao He, Haoran Li, Yuxin Li, Yumeng Wang, Yi R. Fung
被引用 17 次
摘要
Large reasoning models (e.g., R1, o3) have demonstrated remarkable mathematical problem-solving abilities. However, the high reported accuracy of these advanced models on popular datasets and reliance on purely numerical evaluation often mask their true reasoning shortcomings. To address this, we propose leveraging the inherent rigor and methodological complexity of mathematical proofs as a diagnostic tool to expose these hidden failures. Specifically, we introduce the RFMDataset (Reveal Failure Modes), a collection of 200 diverse mathematical proof problems to thoroughly evaluate the performance of advanced models. Our in-depth analysis of their failures uncovers 10 fine-grained error types, which shows fundamental limitations in current large reasoning models: 1) Large reasoning models still have limited capability in generating entirely correct mathematical proofs, with some models solving less than 20% of problems and even making mistakes on fundamental ones; 2) models exhibit a diverse spectrum of reasoning failures, prominently demonstrating the lack of guarantees for the correctness and rigor intermediate reasoning steps; and 3) models show hallucination and incompleteness during the reasoning process. Our findings also reveal that directly prompting models to self-reflect on specific failure modes is insufficient to resolve the current logical dilemmas, necessitating domain knowledge and formal verification. * Equal contribution. Question: Given a triangle ABC with side lengths AB, BC, and AC, prove that AB + BC > AC. Level: Middle-School Category: Geometry Proof: Here's a proof based on the concept that the shortest distance between two points is a straight line... 1. Consider the three points A, B, and C. These three points form the vertices of the triangle ABC. Model Experiment Evaluation Dataset Construction Let : [0, + ∞) → ℝ be a continuous function. For any ∈ [0, 1], we have lim →+∞ ( + ) = 0. Prove that lim →+∞ () may not exist. Here is a math proof question: Question. A student give an answer to this question. Here is his proof: Proof by LLM. And his thinking process: Thinking Process. You are a teacher need to justify whether the student's proof is right. You should examine the proof step by step. Here are possible mistakes: