Elamur Research⌕
☰
home / papers / 2026 / Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models

Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models

Paper · 2026 · Dadi Guo, Jiayu Liu, Zhiyuan Fan et al.

Summary

Popular math benchmarks such as AIME have few items and check only final numerical answers, so the strong scores of large reasoning models can hide flawed reasoning. The authors argue that natural-language proofs are a better diagnostic, because every logical step must hold. They hand-picked 200 proof problems from exams, textbooks, competitions and online media to build RFMDataset. The problems span three education levels, nine subjects and four difficulty grades. In geometry, coordinate and parametric shortcuts are banned so that the tasks keep their intended difficulty. Ten state-of-the-art reasoning models were graded with an LLM-as-a-judge setup, checked against human annotation, and their errors were sorted into a taxonomy of about ten failure modes. Even the strongest model proves fewer than 60% of the problems, and several models also fail easy items. The most common failures are unsound or imprecise individual steps, invented premises and incomplete arguments. Prompting models to watch for these specific errors helps little. The authors conclude that high benchmark accuracy does not imply rigorous reasoning. They suggest targeted domain data and step-level interaction with formal verifiers such as Lean.

Key points

  • RFMDataset composition: 200 proof problems, split into 52 middle-school, 88 high-school and 60 undergraduate items. Each item has a manually assigned difficulty from 1 to 4, and the hardest approach Olympiad level. Code (MIT license) and data (CC license) are at github.com/guodadi/RFMDataset.
  • Overall accuracy: DeepSeek-R1-0120 and Qwen3-235B correctly prove fewer than 20% of problems. The best model, Gemini-2.5-pro-preview-0605, stays at or below 60%.
  • Easy problems: Eight of the ten models score under 60% even at the lowest difficulty level.
  • Failure taxonomy: The fine-grained classification has roughly ten categories, including circular reasoning, over-generalization, invalid construction, transformation errors and logic violations. Ground-truth labels were set by the six authors through a consensus review protocol.
  • Self-reflection and remedies: Self-reflection prompts targeting specific failure modes do not fix the problems. The proposed remedies are training on weak-domain data and agentic, multi-turn verification in Lean with memory of already proven lemmas.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Hong Kong University of Science and TechnologyHong Kong · China142 works · 25,136 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksArts and Humanities · 16,039 worksLanguage and Linguistics · 15,891 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,426 works

Cite

Cite as Dadi Guo, Jiayu Liu, Zhiyuan Fan, Zhitao He, Haoran Li, Yuxin Li, Yumeng Wang and Yi R. Fung. 2026. Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2026.acl-long.582

@inproceedings{guo2026mathematical,
  title = {{Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models}},
  author = {Dadi Guo, Jiayu Liu, Zhiyuan Fan, Zhitao He, Haoran Li, Yuxin Li, Yumeng Wang and Yi R. Fung},
  booktitle = {Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)},
  year = {2026},
  doi = {10.18653/v1/2026.acl-long.582},
  url = {https://doi.org/10.18653/v1/2026.acl-long.582}
}

References

56 references, 19 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Aida Amini, Saadia Gabriel, Shanchuan Lin, Rik Koncel-Kedziorski, Yejin Choi, and Hannaneh Hajishirzi. 2019. Mathqa: Towards interpretable math word problem solving with operation-based formalisms. In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computation…
  2. Anthropic. 2025. Claude 3.7 sonnet system card. Technical report, Anthropic. find
  3. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. 2023. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. CoRR, abs/2302.12433.
  4. Mislav Balunovi’c, Jasper Dekoninck, Nikola Jo-vanovi’c, Ivo Petrov, and Martin T. Vechev. 2025. Mathconstruct: Challenging llm reasoning with constructive proofs. ArXiv, abs/2502.10197. — [arXiv:2502.10197](https://arxiv.org/abs/2502.10197) find
  5. Johan Boye and Birger Moell. 2025a. Large language models and mathematical reasoning failures. Preprint, arXiv:2502.11574. find
  6. Johan Boye and Birger Moell. 2025b. Large language models and mathematical reasoning failures. Preprint, arXiv:2502.11574. find
  7. Yuri Chervonyi, Trieu H Trinh, Miroslav Olšák, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Vikas Verma, Quoc V Le, and Thang Luong. 2025. Gold-medalist performance in solving olympiad geometry with alphageometry2. arXiv preprint arXiv:2502.03544. find
  8. Jiewen Hu, Thomas (Hanwen) Zhu, and Sean Welleck. 2024. minictx: Neural theorem proving with (long-)contexts. ArXiv, abs/2408.03350. find
  9. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. 2021. Training verifiers to solve math word problems. CoRR, abs/2110.14168.
  10. Kaixuan Huang, Jiacheng Guo, Zihao Li, Xiang Ji, Jiawei Ge, Wenzhe Li, Yingqing Guo, Tianle Cai, Hui Yuan, Runzhe Wang, Yue Wu, Ming Yin, Shange Tang, Yangsibo Huang, Chi Jin, Xinyun Chen, Chiyuan Zhang, and Mengdi Wang. 2025. Math-perturb: Benchmarking llms’ math reasoning abilities against hard pe… find
  11. DeepSeek-AI, Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, Xiaokang Zhang, Xingkai Yu, Yu Wu, Z. F. Wu, Zhibin Gou, Zhihong Shao, Zhuoshu Li, Ziyi Gao, and 181 others. 2025. Deepseek-r1: Incentivizing reasoning capability in ll…
  12. Jasper Dekoninck, Ivo Petrov, Kristian Minchev, Mislav Balunovic, Martin T. Vechev, Miroslav Marinov, Maria Drencheva, Lyuba Konova, Milen Shumanov, Kaloyan Tsvetkov, Nikolay Drenchev, Lazar Todorov, Kalina Nikolova, Nikolay Georgiev, Vanesa Kalinkova, and Margulan Ismoldayev. 2025. The open proof c…
  13. Zhiyuan Fan, Weinong Wang, Xing Wu, and Debing Zhang. 2025. Sedareval: Automated evaluation using self-adaptive rubrics. arXiv preprint arXiv:2501.15595. find
  14. Google DeepMind. 2025. Gemini 2.5 pro overview. https://deepmind.google/technologies/ gemini/pro/. ↗
  15. Timothy Gowers. Why are LLMs not better at finding proofs. find
  16. Jiawei Gu, Xuhui Jiang, Zhichao Shi, Hexiang Tan, Xuehao Zhai, Chengjin Xu, Wei Li, Yinghan Shen, Shengjie Ma, Honghao Liu, Saizhuo Wang, Kun Zhang, Yuanzhuo Wang, Wen Gao, Lionel Ni, and Jian Guo. 2025. A survey on llm-as-a-judge. Preprint, arXiv:2411.15594. find
  17. Qi He, Cheng Qian, Xiusi Chen, Bingxiang He, Yi R. Fung, and Heng Ji. 2025a. Veri-r1: Toward precise and faithful claim verification via online reinforcement learning. Preprint, arXiv:2510.01932. find
  18. Zhitao He, Zongwei Lyu, Dazhong Chen, Dadi Guo, and Yi R. Fung. 2025b. Matp-bench: Can mllm be a good automated theorem prover for multimodal problems? Preprint, arXiv:2506.06034. — [arXiv:2506.06034](https://arxiv.org/abs/2506.06034) find
  19. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. Measuring mathematical problem solving with the MATH dataset. In Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIPS Datasets an…
  20. Yichen Huang and Lin F. Yang. 2025. Gemini 2.5 pro capable of winning gold at imo 2025. find
  21. Maxwell Jia. 2025. Aime 2024 dataset. https://huggingface.co/datasets/Maxwell-Jia/ AIME_2024. ↗
  22. American Invitational Mathematics Examination 2024, 30 items. find
  23. Yuhua Jiang, Yuwen Xiong, Yufeng Yuan, Chao Xin, Wenyuan Xu, Yu Yue, Qianchuan Zhao, and Lin Yan. 2025. Pag: Multi-turn reinforced llm self-correction with policy as generative verifier. arXiv preprint arXiv:2506.10406.
  24. Yinghui Li, Jiayi Kuang, Haojing Huang, Zhikun Xu, Xinnian Liang, Yi Yu, Wenlian Lu, Yangning Li, Xiaoyu Tan, Chao Qu, Ying Shen, Hai-Tao Zheng, and Philip S. Yu. 2025. One example shown, many concepts known! counterexample-driven conceptual reasoning in mathematical llms. ArXiv, abs/2502.10454. — [arXiv:2502.10454](https://arxiv.org/abs/2502.10454) find
  25. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, and Qun Liu. 2023. FIMO: A challenge formal dataset for automated theorem proving. CoRR, abs/2309.04295. find
  26. Hanmeng Liu, Zhizhang Fu, Mengru Ding, Ruoxi Ning, Chaoli Zhang, Xiaozhang Liu, and Yue Zhang. 2025a. Logical reasoning in large language models: A survey. Preprint, arXiv:2502.09100.
  27. Jiayu Liu, Cheng Qian, Zhaochen Su, Qing Zong, Shijue Huang, Bingxiang He, and Yi R. Fung. 2025b. Cost-bench: Evaluating multi-turn cost-optimal planning and adaptation in dynamic environments for LLM tool-use agents. CoRR, abs/2511.02734. — [arXiv:2511.02734](https://arxiv.org/abs/2511.02734) find
  28. Jiayu Liu, Junhao Tang, Hanwen Wang, Baixuan Xu, Haochen Shi, Weiqi Wang, and Yangqiu Song. 2024. Gprooft: A multi-dimension multi-round fact checking framework based on claim fact extraction. In The Seventh Fact Extraction and VERification Workshop, page 118. find
  29. Jiayu Liu, Qing Zong, Weiqi Wang, and Yangqiu Song. 2025c. Revisiting epistemic markers in confidence estimation: Can markers accurately reflect large language models’ uncertainty? In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers), pa…
  30. B W Matthews. 1975. Matthews, b.: Comparison of the predicted and observed secondary structure of t4 phage lysozyme. biochimica et biophysica acta (bba)-protein structure 405(2), 442-451. Biochimica et Biophysica Acta, 405(2):442–451. find
  31. Naoto Onda, Kazumi Kasaura, Yuta Oriike, Masaya Taniguchi, Akiyoshi Sannai, and Sho Sonoda. 2025. Leanconjecturer: Automatic generation of mathematical conjectures for theorem proving. arXiv preprint arXiv:2506.22005. find
  32. OpenAI, :, Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, Alex Iftimie, Alex Karpenko, Alex Tachard Passos, Alexander Neitz, Alexander Prokofiev, Alexander Wei, Allison Tam, and 244 others. 2024. Openai o1 sy…
  33. OpenAI. 2025a. Gpt-5 system card. Accessed: 2025-10-07. find
  34. OpenAI. 2025b. Openai o3 and o4-mini system card. Technical report, OpenAI. find
  35. OpenCompass Team. 2025. find
  36. Aime 2025 dataset. https://huggingface.co/datasets/ opencompass/AIME2025. ↗
  37. American Invitational Mathematics Examination 2025, 30 items. find
  38. Ivo Petrov, Jasper Dekoninck, Lyuben Baltadzhiev, Maria Drencheva, Kristian Minchev, Mislav Balunović, Nikola Jovanović, and Martin Vechev. 2025. Proof or bluff? evaluating llms on 2025 usa math olympiad. Preprint, arXiv:2503.21934. find
  39. Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. 2025. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinfo…
  40. ByteDance Seed, Yufeng Yuan, Yu Yue, Mingxuan Wang, Xiaochen Zuo, Jiaze Chen, Lin Yan, Wenyuan Xu, Chi Zhang, Xin Liu, and 1 others. 2025. Seed-thinking-v1. 5: Advancing superb reasoning models with reinforcement learning. arXiv preprint arXiv:2504.13914.
  41. Jiayi Sheng, Luna Lyu, Jikai Jin, Tony Xia, Alex Gu, James Zou, and Pan Lu. 2025. Solving inequality proofs with large language models. ArXiv, abs/2506.07927. — [arXiv:2506.07927](https://arxiv.org/abs/2506.07927) find
  42. Kimi Team, Angang Du, Bofei Gao, Bowei Xing, Changjiu Jiang, Cheng Chen, Cheng Li, Chenjun Xiao, Chenzhuang Du, Chonghua Liao, Chuning Tang, Congcong Wang, Dehao Zhang, Enming Yuan, Enzhe Lu, Fengxiang Tang, Flood Sung, Guangda Wei, Guokun Lai, and 75 others. 2025. Kimi k1.5: Scaling reinforcement l…
  43. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxc’e, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, and 21 others. 2025a. Kimina-prover previ… find
  44. Rui Wang, Qihan Lin, Jiayu Liu, Qing Zong, Tianshi Zheng, Weiqi Wang, and Yangqiu Song. 2025b. Prospect theory fails for llms: Revealing instability of decision-making under epistemic uncertainty. Preprint, arXiv:2508.08992. — [arXiv:2508.08992](https://arxiv.org/abs/2508.08992) find
  45. Ruida Wang, Yuxin Li, Yi R. Fung, and Tong Zhang. 2025c. Let’s reason formally: Natural-formal hybrid reasoning enhances llm’s math capability. Preprint, arXiv:2505.23703.
  46. Ruida Wang, Rui Pan, Yuxin Li, Jipeng Zhang, Yizhen Jia, Shizhe Diao, Renjie Pi, Junjie Hu, and Tong Zhang. 2025d. Ma-lot: Model-collaboration lean-based long chain-of-thought reasoning enhances formal theorem proving. arXiv preprint arXiv:2503.03205.
  47. Yumeng Wang, Zhiyuan Fan, Jiayu Liu, and Yi R. Fung. 2025e. Diversity-enhanced reasoning for subjective questions. find
  48. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hanna Hajishirzi, Yejin Choi, and Kyunghyun Cho. 2021. Naturalproofs: Mathematical theorem proving in natural language. In Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIPS Datasets and Benchmarks 2021, Dec… find
  49. Zhaopan Xu, Pengfei Zhou, Jiaxin Ai, Wangbo Zhao, Kai Wang, Xiaojiang Peng, Wenqi Shao, Hongxun Yao, and Kaipeng Zhang. 2025. Mpbench: A comprehensive multimodal reasoning benchmark for process errors identification. Preprint, arXiv:2503.12505. find
  50. An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, Chujie Zheng, Dayiheng Liu, Fan Zhou, Fei Huang, Feng Hu, Hao Ge, Haoran Wei, Huan Lin, Jialong Tang, and 41 others. 2025. Qwen3 technical report.
  51. Jie Zhang, Cezara Petrui, Kristina Nikolić, and Florian Tramèr. 2025a. Realmath: A continuous benchmark for evaluating language models on research-level mathematics. arXiv preprint arXiv:2505.12575. — [arXiv:2505.12575](https://arxiv.org/abs/2505.12575) find
  52. Ziyin Zhang, Jiahao Xu, Zhiwei He, Tian Liang, Qiuzhi Liu, Yansi Li, Linfeng Song, Zhen-Pu Liang, Zhuosheng Zhang, Rui Wang, Zhaopeng Tu, Haitao Mi, and Dong Yu. 2025b. Deeptheorem: Advancing llm reasoning for theorem proving through natural language and reinforcement learning. ArXiv, abs/2505.23754… — [arXiv:2505.23754](https://arxiv.org/abs/2505.23754) find
  53. Chujie Zheng, Zhenru Zhang, Beichen Zhang, Runji Lin, Keming Lu, Bowen Yu, Dayiheng Liu, Jingren Zhou, and Junyang Lin. 2024. Processbench: Identifying process errors in mathematical reasoning. arXiv preprint arXiv:2412.06559.
  54. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2022. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. Open-Review.net.
  55. Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric P. Xing, Hao Zhang, Joseph E. Gonzalez, and Ion Stoica. 2023. Judging llm-as-a-judge with mt-bench and chatbot arena. Preprint, arXiv:2306.05685.
  56. Qing Zong, Jiayu Liu, Tianshi Zheng, Chunyang Li, Baixuan Xu, Haochen Shi, Weiqi Wang, Zhaowei Wang, Chunkit Chan, and Yangqiu Song. 2025. Critical: Can critique help LLM uncertainty or confidence calibration? CoRR, abs/2510.24505. — [arXiv:2510.24505](https://arxiv.org/abs/2510.24505) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/guo-2026-mathematical-proof-as-litmus-test/