# Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism

arXiv: https://arxiv.org/abs/2605.12524 · HTML: https://mlsanity.com/paper/2605.12524/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 18 of its 109 references that are in the map.
- First posted on arXiv 7 Apr 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 18 of 18)

- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Think you have Solved Question Answering? Try ARC, the AI2 Reasoning Challenge](https://mlsanity.com/paper/1803.05457/) (2018)
- [GPQA: A Graduate-Level Google-Proof Q&A Benchmark](https://mlsanity.com/paper/2311.12022/) (2023)
- [MMLU-Pro: A More Robust and Challenging Multi-Task Language Understanding Benchmark](https://mlsanity.com/paper/2406.01574/) (2024)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models](https://mlsanity.com/paper/2410.07985/) (2024)
- [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://mlsanity.com/paper/2411.04872/) (2024)
- [ARC-AGI-2: A New Challenge for Frontier AI Reasoning Systems](https://mlsanity.com/paper/2505.11831/) (2025)
- [On the Measure of Intelligence](https://mlsanity.com/paper/1911.01547/) (2019)
- [BIG-Bench Extra Hard](https://mlsanity.com/paper/2502.19187/) (2025)
- [Big-Math: A Large-Scale, High-Quality Math Dataset for Reinforcement Learning in Language Models](https://mlsanity.com/paper/2502.17387/) (2025)
- [ARC Prize 2024: Technical Report](https://mlsanity.com/paper/2412.04604/) (2024)
- [SuperGPQA: Scaling LLM Evaluation across 285 Graduate Disciplines](https://mlsanity.com/paper/2502.14739/) (2025)
- [Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models](https://mlsanity.com/paper/2503.21380/) (2025)
- [The relationship between reasoning and performance in large language models--o3 (mini) thinks harder, not longer](https://mlsanity.com/paper/2502.15631/) (2025)
- [Brains vs. Bytes: Evaluating LLM Proficiency in Olympiad Mathematics](https://mlsanity.com/paper/2504.01995/) (2025)
- [LogicInference: A New Dataset for Teaching Logical Inference to seq2seq Models](https://mlsanity.com/paper/2203.15099/) (2022)
- [Your Reasoning Benchmark May Not Test Reasoning: Revealing Perception Bottleneck in Abstract Reasoning Benchmarks](https://mlsanity.com/paper/2512.21329/) (2025)

## Abstract (arXiv)

We introduce ProofGrid, a benchmark suite for evaluating LLM reasoning through machine-checkable proofs rather than final answers alone. ProofGrid contains 15 tasks spanning proof writing, proof checking, proof masking, and proof gap-filling. Tasks are expressed in minimal formal notation, especially NDL, a compact natural-deduction language that fits in short prompts and supports precise, auditable verification. This yields mechanical, reproducible, and fine-grained evaluation rather than judgments by humans or LLMs. ProofGrid covers a calibrated difficulty spectrum, from foundational reasoning tests to structurally rich challenge tasks that no current model solves, while minimizing reliance on domain knowledge, solver delegation, and long-context artifacts. We also develop a comparative framework for reasoning benchmarks and use it to situate ProofGrid relative to existing work in terms of representation, verification guarantees, and reasoning depth. Methodologically, we introduce an instrumented proof-checking pipeline that tolerates minor surface deviations while locating the first substantive reasoning failure, improving measurement resolution and separating proof planning from low-level execution noise. Using this pipeline, we evaluate a broad range of open and proprietary models. Results show rapid progress but substantial remaining limits: frontier models perform well on several foundational tasks, yet difficult tasks, especially those requiring global combinatorial reasoning or low-level proof synthesis, remain far from solved. We also identify epistemic instability, where models generate flawed proofs yet correctly reject those local inferences in isolation, and formalize this with an Epistemic Stability Index. Finally, we complement accuracy with 2PL IRT analyses, Wright maps, and a normalized task-discrimination measure based on Fisher information.