Source-linked AI summary
Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism
Konstantine Arkoudas, Serafim Batzoglou
TL;DR
Existing benchmarks often assess only final answers, leaving proof validity and the reasoning behind correct answers insufficiently measured. The paper introduces ProofGrid, a machine-checkable proof benchmark with instrumented checking and complementary psychometric analyses, and finds that frontier models perform well on foundational tasks but remain substantially limited on difficult proof reasoning. It also identifies scope boundaries in interpreting general reasoning benchmarks such as ARC.
Problem
Answer-only benchmarks can overlook faulty reasoning and rely on memorized knowledge, limiting assessment of proof validity and abstract reasoning competence.
Method
ProofGrid evaluates proof writing, checking, masking, and gap-filling in minimalist formal systems, using instrumented proof checking and complementary benchmark and psychometric analyses.
Results
Frontier models perform well on several foundational tasks but remain far from solving difficult ProofGrid tasks, while even strong models show a gap between abstract logical planning and fully valid proof execution.
Takeaways & Limitations
Machine-checkable proof evaluation exposes reasoning and execution limitations that answer accuracy alone can miss.
Takeaways & Limitations
ARC’s claim to measure general fluid intelligence lacks empirical validation, and leading ARC systems often use neuro-symbolic pipelines rather than end-to-end prediction.
Abstract
from arXiv · showhide
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.
1 Introduction
ProofGrid addresses the limits of answer-only reasoning benchmarks by requiring machine-checkable proofs in minimalist formal languages. It spans calibrated proof tasks and analyses designed to distinguish abstract reasoning competence, formal execution, and model reliability.
- Motivation: Answer-only benchmarks can reward correct results reached through spurious reasoning while overlooking the proof validity required in mathematics.This creates a mismatch between benchmark success and mathematical standards of justification.
- Benchmark design: ProofGrid evaluates proof writing, checking, masking, and gap-filling using machine-checkable proofs in minimalist formal languages, especially NDL.These tasks probe generation, verification, error localization, and structural reconstruction.
- Benchmark design: ProofGrid minimizes reliance on memorized knowledge and solver delegation by expressing problems in uninterpreted symbolic logic and excluding readily algorithmic tasks.This is intended to make performance a cleaner gauge of fluid reasoning competence.
- Results: 99.5% pass@1 on AIME did not translate to strong ProofGrid performance: o4-mini placed in the bottom half of 24 models and often scored below half of o3’s absolute score.For PL3-PW, o4-mini scored 6% compared with o3’s 22%.
- Benchmark design: Its task suite combines foundational tests, difficult tasks not yet solved by the strongest models, and frontier challenges with substantial remaining headroom.The calibrated spectrum is intended to support both baseline assessment and discrimination among capable systems.
- Analyses: The paper extends evaluation with epistemic-stability and calibration analyses, a benchmark-comparison framework, and task-discrimination measures based on IRT and Fisher information.It also documents self-contradictory explanations, verdict reversals, and other reasoning pathologies.
2 Related Work
Existing reasoning benchmarks often evaluate only final answers, leaving the validity and basis of models’ reasoning unverified. Related work also raises concerns about ceiling saturation, crystallized-knowledge confounds, and incomplete evidence for broad intelligence claims.
- Answer-based evaluation: Outcome-based benchmarks judge correctness without requiring logically valid supporting arguments, so they do not directly test the reasoning process.This limitation applies across logical, mathematical, and broader reasoning benchmarks.
- Answer-based evaluation: Final-answer evaluation can reward memorization, pattern matching, heuristic shortcuts, or statistical artifacts instead of sound reasoning.Guessproofness constraints provide only partial defenses because they do not verify whether the answer was reached for the right reasons.
- Diagnostic scope: Mathematical benchmarks also favor models with extensive crystallized mathematical knowledge, which can confound attempts to assess reasoning ability.Training corpora may contain textbooks, proofs, tutorials, problem banks, and related mathematical material.
- Benchmark constructs: Formal proof-oriented evaluation makes deduction explicit and verifiable by allowing the logical structure and validity of conclusions to be traced to premises.This contrasts with benchmarks that provide no proofs or other reasoning artifacts, making reasoning depth impossible to measure.
- Diagnostic scope: Many benchmarks conflate domain knowledge, reading comprehension, cultural context, and symbolic manipulation, producing a coarse-grained signal about reasoning.Their outcomes therefore reflect multiple cognitive demands rather than a narrowly isolated reasoning capability.
- Benchmark constructs: Visual reasoning benchmarks such as ARC target perceptual or visuospatial abstraction, while claims that ARC measures general fluid intelligence lack empirical correlation evidence.The cited discussion identifies an open empirical question concerning relationships with gF, g, or Gf.
4 Proof Masking
Proof masking asks models to reconstruct missing proof structure under implicit constraints, testing meta-reasoning beyond straightforward proof execution. The task exposes substantial differences in model ability, with instrumentation separating substantive failures from surface-format errors.
- Task definition: The task is harder than a conventional CSP because its constraints are implicit, heterogeneous, and distributed across proof syntax and semantics.Difficulty comes from delayed constraint revelation and maintaining globally consistent commitments, not merely searching a large solution space.
- Task definition: Proof masking reconstructs missing conclusions, assumptions, and rule applications so a partial natural-deduction proof becomes coherent.It tests whether models can infer symbolic structure and reason about reasoning itself.
- Evaluation: An instrumented checker improves measured performance by tolerating minor surface deviations such as omitted outer parentheses.Without instrumentation, performance often drops because many detected errors are innocuous formatting deviations.
- Evaluation: DI = 0.38, meaning models differ by about 38 percentage points in average accuracy on PL1-PM.This large spread indicates strong discrimination among ability levels.
- Results: PL1-PM remains demanding despite short proofs: the median is 25 lines, and most top-model performance declines as proof length increases.The decline is gentle for the top four models, but proof length still affects performance.
5 Proof Gaps
Proof-gap performance depends strongly on synthesis demands, proof structure, and problem size, while instrumentation separates logical competence from surface-form errors. Even strong models remain challenged by larger or structurally demanding gaps.
- Discriminability: 37.5% DI on PL1-GF indicates a very large accuracy spread across models, including statistically significant differences among elite systems.The gap-filling task strongly separates models, with significant deltas reported between several top-tier systems.
- Error profiles: Pearson correlation between gap-filling accuracy and normalized error-repair density is -0.82, showing that more repairable errors generally accompany worse performance.DeepSeek R1-0528 is an exception, approaching 50% accuracy despite many mostly syntactic repairs.
- Instrumentation: Instrumented checking significantly raises most PL1-PW and PL2-PW accuracies, but helps little for the eight worst models.The checker is designed to overlook minor errors and decouple formal precision from logical competence; repair rate remains strongly negatively correlated with accuracy.
- Proof synthesis: Gap filling is often harder than proof writing, with Gemini 2.5 Pro showing a 19-point difference between the two tasks.Gap filling spans locally short completions to gaps requiring nearly an entire proof, and it demands reasoning about proof skeletons and assumption scope.
- Scaling: Problem-size scaling produces near-zero accuracy for many models around 40 lines, whereas stronger models decline more gradually.The steepness of collapse differs substantially across systems, with weaker models dominated by parsing and syntax failures.
8 A Quantitative Measure of Epistemic Stability
The paper defines epistemic stability by comparing model outputs across compatible judgments and shows that the measure is asymmetric and reference-distribution dependent. The section also reports severe instability among top models and contrasts this analysis with proof-writing difficulty in Hilbert systems.
- Defining epistemic stability: Epistemic constraints capture when one model judgment obligates or precludes another judgment on a compatible problem.Positive obligations encode required consistency; negative obligations record outputs ruled out by earlier judgments.
- Defining epistemic stability: ESI measures the fraction of D2 judgments not precluded by any judgment in D1, making the quantity inherently asymmetric.The normalization is by |D2| because the two directional measures have different units of analysis.
- Empirical findings: Top-tier models show severe epistemic instability, with even GPT-5.2 exhibiting a nearly 40% chance of self-inconsistency.The section computes this result from model-generated proofs and entailment judgments.
- Defining epistemic stability: Epistemic stability depends on the chosen reference distribution, with generic and error-triggered variants measuring different phenomena.The reported error-triggered values are 0.14 for Gemini 3.1 and 0.38 for GPT-5.2.
- Proof-writing results: PL4-PW exposes a separate formal-control challenge: Hilbert proof writing is difficult, and challenge-set success remains extremely low.Gemini 3.1 solved 6/50 PL4-PW-c problems, GPT-5.2 solved 3, Gemini 3 solved 1, and all other evaluated models solved none.
- Proof-writing results: PL4-PW accuracy falls rapidly with problem size, while correct proofs are generally shorter than all generated proofs.The lenient-mode DI is 0.13, and proof-size distributions show narrower, left-shifted correct-proof distributions for most models.
10 Conclusions
PROOFGRID evaluates reasoning through machine-checkable proofs rather than answer accuracy alone, providing a fine-grained diagnostic of inference integrity. The results show rapid progress alongside persistent limits in formal execution, especially on difficult structured problems, while motivating proof-based evaluation as models enter scientific and mathematical workflows.
- Conclusions: PROOFGRID assesses LLM reasoning through rigorous, machine-checkable proof construction and analysis rather than final answers alone.The benchmark is intended to provide more precise and fine-grained evaluation of inference integrity.
- Conclusions: Frontier models have rapidly improved on foundational tasks, but difficult structurally rich problems still expose major limitations.The paper describes substantial progress in less than a year while reporting hard limits as reasoning difficulty increases.
- Conclusions: Models show partial reasoning competence yet often lack procedural grounding and cognitive control for rigorously executing formally constrained strategies.They may identify valid conclusion structure while failing to suppress invalid operations or obey deterministic formal rules.
- Conclusions: Proof-based evaluation reveals the structure of current reasoning systems, including the gap between semantic fluency and formal control.The authors characterize PROOFGRID as a diagnostic instrument rather than merely a stricter grading scheme.
- Conclusions: The benchmark’s formal notation supports precise checking, explicit proof structure, and separation of logical organization from proof search.NDL is presented as declarative and natural-deduction-like, with explicit assumptions and scopes.
- Conclusions: The authors acknowledge that PROOFGRID measures deployment and generalization of learned reasoning strategies rather than tabula-rasa fluid intelligence.Pretraining can provide proof templates, symbolic manipulation patterns, and deductive concepts.
- Conclusions: PROOFGRID targets operational symbolic inference ability rather than ordinary human performance, while current models remain far from robust hard reasoners.The paper compares current systems with mature methods such as resolution and Knuth-Bendix completion.
11 Limitations
ProofGrid’s scope and reported comparisons have important boundaries: it targets minimally formal logical reasoning, emphasizes accuracy over efficiency, omits several expressive reasoning domains, and reflects a time-sensitive model snapshot.
- ProofGrid tests logical reasoning in minimally formal languages, so its results may not fully generalize to natural-language reasoning contexts.
- Its metrics focus on accuracy rather than efficiency, leaving differences in test-time compute and resource requirements unmeasured.
- The current propositional and equational tasks do not cover quantification, variable binding, or more expressive semantic structures.
- Reported model-family rankings are a time-bound snapshot that may change substantially as newer reasoning systems become available.
- Despite these limitations, ProofGrid provides insights into progress and remaining challenges in evaluating logical reasoning in AI systems.
A NDL
NDL is a compact formal language for natural-deduction proofs, designed to represent standard proofs while supporting precise interpreter-based checking that exposes reasoning errors.
- NDL is expressive enough to represent standard natural-deduction proofs, yet simple enough to admit precise interpreter-based semantics.
- NDL is deliberately unforgiving, exposing reasoning errors rather than hiding them behind informal prose.
- Checking a proof evaluates it in an assumption base and returns either a unique conclusion or a relevant error message.The interpreter takes a proof and assumption base as inputs; the initial assumption base is empty and assertions add named premises.
- Core NDL proofs comprise rule applications, conditional proofs, and compositions, with compositions passing earlier conclusions forward as reusable lemmas.Rule applications use built-in inference rules, while conditional proofs evaluate a body under an added hypothesis.
- Conclusion annotations enforce alignment between a proof’s intended result and the result produced by evaluation without adding inferential power.
- NDL’s formal semantics are implemented by the interpreter, whose definition is presented in Figure 48.
B.2 Modeling and ICCs
The 2PL IRT framework models each item’s success probability from respondent ability, item difficulty, and discrimination, then uses Fisher information to compare task discrimination across ability bands.
- The 2PL model assigns each item a probability of correct response determined by latent ability, discrimination, and difficulty.Its response function is P(Yj = 1 | θ, aj, bj) = σ(aj(θ − bj)).
- Item difficulty shifts an item characteristic curve horizontally, while discrimination controls its slope and sensitivity to nearby ability differences.Higher ability raises success probability at fixed difficulty, while higher difficulty lowers it at fixed ability.
- IRT interpretation assumes unidimensionality and conditional independence, but shared hidden structure and problem types can threaten those assumptions in ProofGrid tasks.The appendix notes that PL3-PW performance depends nontrivially on problem type and that item dependence is common in related or duplicated items.
- The normalized discrimination analysis averages task information over a target ability band, making discrimination a band-specific quantity.The numerical implementation averages over a fine uniform grid, and high information throughout the band indicates stronger discrimination there.
- Mean information per item removes the trivial advantage of longer tasks but remains mainly comparative rather than intrinsically interpretable.
B.5 PL1-PM IRT model
For PL1-PM, IRT abilities preserve the accuracy ranking except where tied accuracies are separated, while the Wright map and information curve reveal where the task discriminates across ability levels.
- IRT abilities from PL1-PM induce the same ranking as accuracies, except that tied GPT-5 and Claude Sonnet 4.5 extended-thinking scores become strictly ordered.GPT-5’s estimated latent ability is slightly lower despite identical accuracies.
- The PL1-PM Wright map places models and item difficulties on a common θ scale spanning approximately -2.32 to 2.14.
- Items clustered near an ability value correspond to higher task information there, with PL1-PM especially sensitive near θ = 0.
- PL1-PM is one of the few ProofGrid tasks with good discrimination in the lower half of the ability scale, with ST (−2, 0.2) = 0.63.
B.6 PL3-PC IRT model
The PL3-PC IRT analysis shows strong measurement coverage across the broad and mid-ability ranges, but less stable discrimination at the extremes. Model rankings can also reflect difficulty profiles rather than simply the number of problems solved.
- Task coverage: PL3-PC covers many nearby difficulty levels, with its densest item mass from θ ≈−0.45 to θ ≈0.49.Coverage extends through θ ≈0.73 and 0.96, while the extreme tails are thinner.
- Interpretation: Gemini 3 ranks ahead of Gemini 3.1, and GPT-5 ranks ahead of Claude Sonnet 4.5 with extended thinking, likely because of differing problem-difficulty profiles.The passage attributes these rankings to the difficulty profiles rather than the sheer number of problems solved.
- Discrimination: ST (−0.7, 0.7) = 0.93, indicating exceptionally strong discrimination across the mid-tier ability band.For weaker models, discrimination is 0.81 in (−0.5, 0) but drops to 0.21 in (−1.9, −0.6).
B.7 Type-indexed PL3-PW IRT models
Type-indexed PL3-PW IRT analyses show that different problem families target different ability ranges. Tseitin-formula and relativized-pigeonhole tasks are especially effective for discriminating elite models, while PL4-PW provides a broader ability-scale view.
- Wright maps: The PL3-PW Tseitin-formula Wright map places models and items on a shared θ scale spanning −0.72 to 3.12.The map is presented as a model-item comparison for this problem family.
- PL3-PW problem families: Tseitin-formula problems discriminate top-tier models strongly, with ST (0.9, 3.1) = 0.845, but are ineffective for lower- and mid-tier discrimination.The corresponding relativized-pigeonhole score is ST (0.9, 3.0) = 0.823.
- PL3-PW problem families: Relativized-pigeonhole problems show a similar concentration of discrimination in the elite ability range.Their normalized discrimination score is reported over Θ = (0.9, 3.0).
- PL4-PW: PL4-PW ability estimates are shown alongside its task-information curve over the observed ability range.The figure notes low information for models with ability θ < 0.
- PL4-PW: PL4-PW has normalized discrimination ST (0.5, 3.2) = 0.7 for models roughly at or above the 83rd percentile.The task is described as effective primarily for elite-model discrimination.
C.1 Data Generation for PL1
PL1 problems are generated as constrained random logical ASTs, with additional normalization and solver-based checks to control validity and duplicates. Proof-generation and corruption procedures support proof-checking tasks with detailed inference certificates.
- Problem generation: PL1 premises and goals are generated randomly as ASTs by recursively expanding logical operators or atoms up to a maximum depth.The generation process is designed to produce structured formal arguments rather than relying on domain knowledge.
- Problem constraints: Generated problems require distinct formulas, logical entailment, necessary premises, contained goal atoms, and consistent premises and negated goals.These constraints target nondegenerate arguments with meaningful premise-goal structure.
- Problem constraints: A SAT solver enforces logical entailment, premise necessity, and consistency constraints during generation.The solver is used specifically for constraints 2, 3, and 5.
- Deduplication: Duplicate problems are limited by comparing universally quantified, alpha-equivalent normal forms after sorting and conjoining premises.Alpha-equivalence treats problems as identical up to renaming bound variables.
- Proof generation: The Athena theorem prover uses backward and forward heuristics and produces fully detailed low-level proof certificates.Some proofs are deliberately corrupted by changing inference forms or arguments or removing subproof steps.
C.2 Result Archives
ProofGrid releases one YAML result archive per task, containing problem metadata, model outputs, evaluation results, and related run information. Records use task-local indices and structured fields to connect each problem with model-specific outcomes and checker diagnostics.
- Archive organization: Result archives are released for all 15 PROOFGRID tasks as one YAML file per task.The archives document the benchmark’s task-level experimental results.
- Archive contents: YAML files contain problem descriptions, metadata, model identifiers, timestamps, raw and processed outputs, and partial usage or reasoning information.The exact fields available vary across runs.
- Record structure: Each result dictionary has a task-local numeric index that uniquely identifies a problem and its associated results.IRT references such as “item 28” therefore refer to the record with the corresponding index in that task’s YAML file.
- Record structure: A result record typically links the problem, metadata, and a results dictionary containing one model-specific result dictionary for each of 24 model identifiers.Model-specific records include API timestamps, raw outputs, and processed or evaluated outputs.
- Evaluation diagnostics: Checker diagnostics can identify an incorrect result, its error type and step, the offending rule, missing formulas, and structural fixes.The example records an incorrect proof with errorType notInAB at step 7 and a missing formula B.
C.3 Result Timeline and Interaction Protocol
Experiments ran from April 2025 through March 2026 using provider APIs, single-call prompting, task-specific formats, and model-dependent decoding settings. The protocol excluded external tools and aggregation methods, while reporting Wilson confidence intervals for accuracy estimates.
- Timeline and interaction protocol: Experiments ran from April 2025 through March 2026, with API-call distribution summarized in Figure 53.All systems were queried as plain language models without external tools, retrieval, web search, or agent tooling.
- Prompt and output structure: Each task used its own prompt, typically with several in-context examples, and most tasks required JSON outputs.PL1 gap filling instead produced labeled GAP-i textual segments that the pipeline reconstructed into complete proofs for automatic checking.
- Uncertainty reporting: Accuracy tables report point estimates with 95% Wilson confidence intervals computed from binary item-level outcomes.The observed accuracy is k/n, while the reported uncertainty reflects finite sample size; parenthetical values are rounded Wilson half-widths.
- Experimental documentation: Provider routing and model identifiers were documented alongside task-family input/output structures and decoding policies.Tables 34–37 summarize provider routing, the 24-model set, prompt/output structure, and decoding, reasoning, and token-budget policies.
- Decoding and reasoning settings: Decoding controls varied by model and provider rather than following one uniform policy.GPT-5 and o-series models used Responses API reasoning settings, GPT-4o and GPT-4.1 used Chat Completions temperatures, and other providers used distinct controls or defaults.
- Decoding and reasoning settings: Proof checking used low temperature, whereas proof writing used moderate temperature because the former is judgment-oriented and the latter searches over proof trajectories.For GPT-4o and GPT-4.1, the task-level temperatures were 0.01 for proof checking and 0.6 for proof writing.
C.8 Batching, Partial Results, and Failure Policy
Batching and reruns were handled flexibly across models, while malformed, incomplete, and failed outputs remained explicitly represented under a defined denominator policy.
- Batching: Only Anthropic models were run in batch mode, with serial fill-ins used to complete missing items or rerun failures.Batched outputs were matched to problems using explicit custom identifiers rather than positional order.
- Partial results: Malformed outputs were preserved through raw outputs, explicit flags, or task-specific parse-failure markers.Proof-checking tasks also recorded explicit API-call failures, and malformed or missing outputs remained visible in released files.
- Failure handling: Rerun needs varied across models, with difficult tasks producing budget exhaustion, malformed answers, API failures, or refusals for some reasoning-oriented systems.Grok-4 was especially difficult, while some advanced GPT models often declined to answer the hardest problems.
- Denominator policy: Server-side nonresponses were removed from the denominator, but incomplete or ill-formed responses counted as answers.When possible, invalid or partial results were postprocessed or rerun.
C.9 Evaluation
Performance was computed through deterministic, task-specific evaluation pipelines rather than directly from raw model outputs.
- Deterministic evaluation: Each task used a deterministic evaluation pipeline whose operational details were described for individual tasks and released in the Github code base.The pipeline forms part of the experimental design rather than serving only as post hoc output processing.
C.10 Reasoning Metadata in the Released Result Files
Released result files contain reasoning metadata for only a subset of runs, with availability varying across providers and task families.
- Available metadata: Reasoning metadata included provider usage summaries, extracted reasoning summaries, stored thinking traces, and provider stop reasons.Coverage was limited rather than universal across the reported runs.
- Coverage limitations: Metadata was common in several proof-checking runs and subsets of masking, gap-filling, and equational results, but less common for Gemini, xAI, and some OpenRouter-backed models.Provider and task coverage therefore constrains cross-run comparisons based on these fields.