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

Hugging Face Daily Papers Papers
reasoning benchmark llm-evaluation proof-verification natural-deduction formal-notation epistemic-stability

Summary

ProofGrid is a benchmark suite that evaluates LLM reasoning through machine-checkable proofs using minimal formal notation, with tasks in proof writing, checking, and gap-filling, revealing progress and remaining limits including epistemic instability.

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.
Original Article
View Cached Full Text

Cached at: 05/18/26, 06:27 PM

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

Source: https://huggingface.co/papers/2605.12524

Abstract

ProofGrid presents a benchmark suite for evaluating LLM reasoning through machine-checkable proofs, featuring tasks in proof writing and verification with minimal formal notation and a comparative framework for assessing reasoning depth and stability.

We introduce ProofGrid, a benchmark suite for evaluating LLM reasoning throughmachine-checkable proofsrather than final answers alone. ProofGrid contains 15 tasks spanningproof writing,proof checking,proof masking, andproof gap-filling. Tasks are expressed in minimalformal notation, especiallyNDL, a compactnatural-deduction languagethat 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, andreasoning 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 anEpistemic Stability Index. Finally, we complement accuracy with2PL IRT analyses,Wright maps, and a normalized task-discrimination measure based onFisher information.

View arXiv pageView PDFProject pageGitHub2Add to collection

Models citing this paper0

No model linking this paper

Cite arxiv.org/abs/2605.12524 in a model README.md to link it from this page.

Datasets citing this paper0

No dataset linking this paper

Cite arxiv.org/abs/2605.12524 in a dataset README.md to link it from this page.

Spaces citing this paper0

No Space linking this paper

Cite arxiv.org/abs/2605.12524 in a Space README.md to link it from this page.

Collections including this paper0

No Collection including this paper

Add this paper to acollectionto link it from this page.

Similar Articles