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

Konstantine Arkoudas; Serafim Batzoglou

cs.LOApr 7, 2026

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

Authors: Konstantine Arkoudas, Serafim Batzoglou

Abstract

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.

Figures & tables

	Input	Output	Content	Expr.	Range	R. Depth	Tasks	Size	Satur.	Verif.
SNLI	NL	MCQA	Common Sense	—	—	—	1	570K	High	✗
MNLI	NL	MCQA	Common Sense	—	—	—	1	433K	High	✗
LogicQA 2.0	NL	MCQA	Common Sense	—	—	—	2	15708	High	✗
Hellaswag	NL	MCQA	Common Sense	—	—	—	1	70K	High	✗
RuleTaker	CNL	Binary	Common Sense	S. Datalog	Low	5	1	500K	High	✗
ProofWriter	CNL	Proof Trees	Common Sense	S. Datalog	Low	5	3	500K	High	✓

Table 1: Qualitative comparison of 33 reasoning datasets. A long dash ( — ) means NA (not applicable). Expr. represents the expressiveness of the underlying logic (when one exists). Range represents the diversity of reasoning mechanisms tested by a benchmark. R. Depth is the maximum reasoning depth required. Satur. is the benchmark’s saturation level. Verif. indicates whether a benchmark programmatically verifies the model’s reasoning. NL: Natural Language; CNL: Controlled Natural Language; COT: Chain of Thought; MCQA: Multiple-Choice Question Answering; PL: Propositional Logic; S. Datalog: Stratified Datalog; PHL: Positive Horn Logic;

\mbox{FOL}_{0}

= propositional logic plus a very small fragment of FOL; EQL: (unconditional) Equational Logic; HOL: Higher-Order Logic.

Figure 1: A radar-chart comparison of ProofGrid and 5 logic-based CNL benchmarks.

Panel of Table 2 — Table 2: Data distribution summaries with inline box-sparklines for the 400 problems in PL-PW1 . Box = IQR (Interquartile Range); red line = median; dot = mean; whiskers = 5–95th.

Model	Overlooked Syntax Errors	Overlooked Semantic Errors	Model	Overlooked Syntax Errors	Overlooked Semantic Errors
hermes-4	2525	245	deepseek-r1-0528	1971	313
llama-3.1-405b	1387	232	deepseek-v3.1	1379	199
deepseek-reasoner	1354	194	gpt-4o	1027	171
gpt-4.1	1077	115	o3-mini	713	316
o4-mini	649	363	mistral-magistral	686	315
deepseek-v3	721	219	o3	318	378

Table 3: Per-model numbers of syntactic and structural or semantic errors detected and repaired by the instrumented proof checker when evaluating PL1-PW proofs, sorted by the total number of errors (from left to right and top to bottom).

Model	Instrumented Accuracy	Strict Accuracy	Model	Instrumented Accuracy	Strict Accuracy
claude-opus-4-5-20251101	0.99 $\;(\pm\>0.01)$	0.93 $\;(\pm\>0.03)$	gemini-3.1-pro-preview	0.99 $\;(\pm\>0.01)$	0.92 $\;(\pm\>0.03)$
gpt-5.2	0.98 $\;(\pm\>0.01)$	0.84 $\;(\pm\>0.04)$	gpt-5.1	0.97 $\;(\pm\>0.02)$	0.78 $\;(\pm\>0.04)$
gemini-2.5-pro	0.94 $\;(\pm\>0.02)$	0.60 $\;(\pm\>0.05)$	gpt-5	0.92 $\;(\pm\>0.03)$	0.62 $\;(\pm\>0.05)$
gemini-3.0-pro-preview	0.92 $\;(\pm\>0.03)$	0.67 $\;(\pm\>0.05)$	claude-sonnet-4.5-ext-thinking	0.88 $\;(\pm\>0.03)$	0.63 $\;(\pm\>0.05)$
grok-4	0.85 $\;(\pm\>0.03)$	0.59 $\;(\pm\>0.05)$	o3	0.80 $\;(\pm\>0.04)$	0.53 $\;(\pm\>0.05)$
deepseek-reasoner	0.76 $\;(\pm\>0.04)$	0.45 $\;(\pm\>0.05)$	deepseek-r1-0528	0.60 $\;(\pm\>0.05)$	0.21 $\;(\pm\>0.04)$

Table 4: PL1-PW proof-writing accuracies from the instrumented proof checker and from the regular (strict) proof checker, with Wilson confidence intervals.

Figure 2: Scatterplot of strict accuracy vs instrumentation deltas across the 24 models.

Figure 3: Distribution of first-error types under the instrumented proof checker.

	Mean	Median	Min	Max	Std	@5	@25	@50	@75	@90	@95
Proof length	30.69	29.0	5	125	13.85	12.0	21.0	29.0	38.0	49.0	55.05

Table 8

Model	Full Task	Guessing Only	Model	Full Task	Guessing Only
gemini-3.1-pro-preview	0.94 $\;(\pm\>0.03)$	0.97 $\;(\pm\>0.02)$	gpt-5.2	0.92 $\;(\pm\>0.03)$	0.95 $\;(\pm\>0.03)$
claude-opus-4-5-20251101	0.92 $\;(\pm\>0.03)$	0.94 $\;(\pm\>0.02)$	gpt-5.1	0.91 $\;(\pm\>0.03)$	0.95 $\;(\pm\>0.03)$
gemini-2.5-pro	0.90 $\;(\pm\>0.03)$	0.94 $\;(\pm\>0.03)$	gemini-3.0-pro-preview	0.89 $\;(\pm\>0.04)$	0.96 $\;(\pm\>0.02)$
claude-sonnet-4.5-ext-thinking	0.89 $\;(\pm\>0.04)$	0.94 $\;(\pm\>0.03)$	gpt-5	0.86 $\;(\pm\>0.04)$	0.92 $\;(\pm\>0.03)$
o3	0.82 $\;(\pm\>0.04)$	0.92 $\;(\pm\>0.03)$	grok-4	0.82 $\;(\pm\>0.04)$	0.88 $\;(\pm\>0.04)$
o4-mini	0.79 $\;(\pm\>0.05)$	0.87 $\;(\pm\>0.04)$	deepseek-reasoner	0.73 $\;(\pm\>0.05)$	0.83 $\;(\pm\>0.04)$

Table 5: PL1-PC accuracies for the full task and for simple binary classification of proofs as correct/incorrect.

Figure 4: PL1-PC full-task accuracy vs rank.

Figure 5: Lorenz-style curve of model accuracies on the full PL1-PC task.

Figure 6: Types of root errors made by models on PL1-PC .

Figure 7: PL1-PC accuracies for the top 10 models as a function of proof length.

Figure 8: PL1-PC accuracies as a function of proof length for the bottom 14 models.

Model	Full Task	Guessing Only	Model	Full Task	Guessing Only
claude-opus-4-5-20251101	0.65 $\;(\pm\>0.13)$	0.69 $\;(\pm\>0.12)$	gpt-5.2	0.64 $\;(\pm\>0.13)$	0.66 $\;(\pm\>0.13)$
gemini-3.1-pro-preview	0.48 $\;(\pm\>0.13)$	0.52 $\;(\pm\>0.13)$	gpt-5.4	0.44 $\;(\pm\>0.13)$	0.48 $\;(\pm\>0.13)$

Table 6: PL1-PC-c accuracies, for the full task and for simple guessing.

Figure 10: Inferential profile of PL1-PM proofs.

Model	Instrumented Accuracy	Strict Accuracy	Model	Instrumented Accuracy	Strict Accuracy
gemini-3.1-pro-preview	0.98 $\;(\pm\>0.02)$	0.97 $\;(\pm\>0.02)$	gemini-3.0-pro-preview	0.96 $\;(\pm\>0.02)$	0.93 $\;(\pm\>0.03)$
gpt-5.2	0.90 $\;(\pm\>0.03)$	0.82 $\;(\pm\>0.04)$	claude-opus-4-5-20251101	0.89 $\;(\pm\>0.04)$	0.87 $\;(\pm\>0.04)$
gpt-5.1	0.89 $\;(\pm\>0.04)$	0.84 $\;(\pm\>0.04)$	grok-4	0.82 $\;(\pm\>0.04)$	0.68 $\;(\pm\>0.05)$
gemini-2.5-pro	0.81 $\;(\pm\>0.04)$	0.50 $\;(\pm\>0.06)$	gpt-5	0.79 $\;(\pm\>0.05)$	0.64 $\;(\pm\>0.05)$
claude-sonnet-4.5-ext-thinking	0.79 $\;(\pm\>0.05)$	0.70 $\;(\pm\>0.05)$	o3	0.75 $\;(\pm\>0.05)$	0.69 $\;(\pm\>0.05)$
deepseek-reasoner	0.60 $\;(\pm\>0.06)$	0.53 $\;(\pm\>0.06)$	deepseek-r1-0528	0.54 $\;(\pm\>0.06)$	0.37 $\;(\pm\>0.05)$

Table 7: PL1-PM accuracies, using both the instrumented NDL checker and the regular proof checker.

Figure 11: PL1-PM accuracy vs proof length for the top 10 models; variable-width bins with $n\geq 25$ .

Figure 12: PL1-PM accuracy vs proof length for the bottom 14 models; variable-width bins with $n\geq 25$ .

Model	Instrumented Accuracy	Strict Accuracy	Model	Instrumented Accuracy	Strict Accuracy
gpt-5.4	0.38 $\;(\pm\>0.13)$	0.14 $\;(\pm\>0.1)$	gemini-3.1-pro-preview	0.34 $\;(\pm\>0.13)$	0.14 $\;(\pm\>0.1)$
gpt-5.2	0.32 $\;(\pm\>0.13)$	0.28 $\;(\pm\>0.12)$	claude-opus-4-5-20251101	0.06 $\;(\pm\>0.07)$	0.06 $\;(\pm\>0.07)$

Table 8: PL1-PM-c instrumented and strict accuracies.

Model	Instrumented Accuracy	Strict Accuracy	Model	Instrumented Accuracy	Strict Accuracy
claude-opus-4-5-20251101	0.94 $\;(\pm\>0.03)$	0.88 $\;(\pm\>0.05)$	gemini-3.1-pro-preview	0.92 $\;(\pm\>0.04)$	0.89 $\;(\pm\>0.04)$
gpt-5.2	0.93 $\;(\pm\>0.04)$	0.84 $\;(\pm\>0.05)$	gpt-5	0.90 $\;(\pm\>0.04)$	0.79 $\;(\pm\>0.06)$
gemini-3.0-pro-preview	0.89 $\;(\pm\>0.04)$	0.77 $\;(\pm\>0.06)$	gpt-5.1	0.89 $\;(\pm\>0.04)$	0.70 $\;(\pm\>0.06)$
claude-sonnet-4.5-ext-thinking	0.80 $\;(\pm\>0.06)$	0.60 $\;(\pm\>0.07)$	o3	0.77 $\;(\pm\>0.06)$	0.56 $\;(\pm\>0.07)$
gemini-2.5-pro	0.75 $\;(\pm\>0.06)$	0.49 $\;(\pm\>0.07)$	grok-4	0.69 $\;(\pm\>0.06)$	0.55 $\;(\pm\>0.07)$
deepseek-reasoner	0.61 $\;(\pm\>0.07)$	0.31 $\;(\pm\>0.06)$	o4-mini	0.45 $\;(\pm\>0.07)$	0.37 $\;(\pm\>0.07)$

Table 9: PL1-GF accuracies, using both the instrumented and the regular proof checker.

Model	Syntax $R/100L$	Semantic $R/100L$	Total $R/100L$	Model	Syntax $R/100L$	Semantic $R/100L$	Total $R/100L$
gemini-3.1-pro-preview	0.12	0.37	0.49	claude-opus-4-5-20251101	0.20	0.56	0.76
gpt-5	0.42	0.71	1.13	gpt-5.2	0.97	0.47	1.44
gemini-3.0-pro-preview	0.83	1.30	2.13	gpt-5.1	3.10	1.01	4.11
o3	2.64	1.67	4.31	claude-sonnet-4.5-ext-thinking	2.85	1.75	4.60
grok-4	3.31	2.61	5.92	grok-3	5.56	1.74	7.30
o4-mini	6.71	1.11	7.82	gemini-2.5-pro	6.05	1.86	7.91

Table 10: Error repairs made by the instrumented checker per 100 lines of generated proof code.

Figure 15: PL1-GF instrumented model accuracies vs total error repairs per 100 lines.

Figure 16: PL1-GF distribution of first errors.

Figure 17: PL1-GF accuracy vs gapped proof length for the top 12 models

Figure 18: PL1-GF accuracy vs gapped proof length for the bottom 12 models.

Model	Instrumented Accuracy	Strict Accuracy	Model	Instrumented Accuracy	Strict Accuracy
gpt-5.4	0.51 $\;(\pm\>0.13)$	0.51 $\;(\pm\>0.13)$	gpt-5.2	0.35 $\;(\pm\>0.13)$	0.31 $\;(\pm\>0.12)$
gemini-3.1-pro-preview	0.25 $\;(\pm\>0.12)$	0.24 $\;(\pm\>0.11)$	claude-opus-4-5-20251101	0.0 $\;(\pm\>0.04)$	0.0 $\;(\pm\>0.04)$

Table 11: PL1-GF-c instrumented and strict accuracies.

Panel of Table 12 — Table 12: Data distribution summaries for the 200 problems in PW-3 . Box = IQR (Interquartile Range); red line = median; dot = mean; whiskers = 5–95th.

Figure 19: PL2-PW proof-size distributions per model: all proofs (blue) vs correct proofs (green); min–max line, 5–95% band, IQR box, median tick, mean dot.

Figure 20: PL2-PW proof-size median ratios by each model (a higher value means that the all-proofs median is longer than the correct-proofs-only median size).

Model	Instrumented Accuracy	Strict Accuracy	Model	Instrumented Accuracy	Strict Accuracy
gemini-3.1-pro-preview	0.94 $\;(\pm\>0.03)$	0.44 $\;(\pm\>0.07)$	gpt-5.2	0.87 $\;(\pm\>0.05)$	0.12 $\;(\pm\>0.05)$
gpt-5.1	0.82 $\;(\pm\>0.05)$	0.03 $\;(\pm\>0.03)$	gemini-3.0-pro-preview	0.62 $\;(\pm\>0.07)$	0.05 $\;(\pm\>0.03)$
gpt-5	0.41 $\;(\pm\>0.07)$	0.03 $\;(\pm\>0.03)$	o3	0.39 $\;(\pm\>0.07)$	0.06 $\;(\pm\>0.03)$
gemini-2.5-pro	0.36 $\;(\pm\>0.07)$	0.03 $\;(\pm\>0.03)$	grok-4	0.26 $\;(\pm\>0.06)$	0.01 $\;(\pm\>0.02)$
deepseek-reasoner	0.18 $\;(\pm\>0.05)$	0.0 $\;(\pm\>0.01)$	claude-opus-4-5-20251101	0.14 $\;(\pm\>0.05)$	0.1 $\;(\pm\>0.04)$
deepseek-r1-0528	0.09 $\;(\pm\>0.04)$	0.0 $\;(\pm\>0.01)$	claude-sonnet-4.5-ext-thinking	0.08 $\;(\pm\>0.04)$	0.01 $\;(\pm\>0.02)$

Table 13: PL2-PW accuracies from the instrumented proof checker and from the regular (strict) proof checker.

Figure 21: PL2-PW error corrections made by the instrumented checker per model (sorted by total).

Figure 22: PL2-PW error types flagged by the instrumented checker.

Figure 23: PL2-PW accuracies for the top 12 models as a function of problem size.

A_{1}

\neg A_{2}\mbox{

>\Rightarrow,

}\neg A_{1}

A_{2}\mbox{

>\Rightarrow,

}A_{3}

A_{2}\mbox{

>\wedge>

}\neg A_{3}\mbox{

>\vee>

}A_{4}

\neg A_{5}\mbox{

>\wedge>

}A_{3}\mbox{

>\Rightarrow,

}\neg A_{4}

A_{5}\mbox{

>\Rightarrow,

}A_{6}

A_{6}\mbox{

>\wedge>

}\neg A_{7}\mbox{

>\Rightarrow,

}\neg A_{2}\mbox{

>\vee>

}\neg A_{5}

Table 38

Figure 39

Figure 24: The directed acyclic reasoning graph of a proof for a medium-complexity Tseitin-formula problem.

Panel of Figure 25 — Figure 25: The distribution of reasoning depth across all $\textsc{PL}_{3}$ proof-checking problems.

Figure 26: Mean values of key numeric features of PL3-PW problems, organized by problem type.

Model	Instrumented Accuracy	Strict Accuracy	Model	Instrumented Accuracy	Strict Accuracy
gemini-3.1-pro-preview	0.72 $\;(\pm\>0.05)$	0.67 $\;(\pm\>0.05)$	gpt-5.2	0.53 $\;(\pm\>0.06)$	0.49 $\;(\pm\>0.06)$
grok-4	0.48 $\;(\pm\>0.06)$	0.36 $\;(\pm\>0.05)$	gpt-5.1	0.46 $\;(\pm\>0.06)$	0.41 $\;(\pm\>0.06)$
claude-opus-4-5-20251101	0.44 $\;(\pm\>0.06)$	0.41 $\;(\pm\>0.06)$	gemini-3.0-pro-preview	0.38 $\;(\pm\>0.05)$	0.36 $\;(\pm\>0.06)$
gpt-5	0.37 $\;(\pm\>0.05)$	0.33 $\;(\pm\>0.05)$	gemini-2.5-pro	0.33 $\;(\pm\>0.05)$	0.29 $\;(\pm\>0.05)$
o3	0.22 $\;(\pm\>0.05)$	0.19 $\;(\pm\>0.04)$	claude-sonnet-4.5-ext-thinking	0.22 $\;(\pm\>0.05)$	0.19 $\;(\pm\>0.04)$
deepseek-reasoner	0.21 $\;(\pm\>0.05)$	0.08 $\;(\pm\>0.03)$	deepseek-r1-0528	0.13 $\;(\pm\>0.04)$	0.02 $\;(\pm\>0.02)$

Table 14: PL3-PW proof-writing accuracies with and without automatic syntax repairs.

Figure 27: PL3-PW model accuracy vs. problem type heatmap.

Figure 28: PL3-PW distribution of first errors.

Model	# of Logical Errors	Self-Recognized Proportion	Mean Self-Rated Recognition Difficulty (1-5 Scale)
gemini-2.5-pro	161	100%	1.67
gpt-5	160	100%	1.15
gpt-5.1	122	100%	1.58
gemini-3.0-pro-preview	114	100%	1.26
claude-opus-4-5-20251101	91	100%	1.73
grok-4	82	100%	1.71

Table 15: Proportion of logical errors made by a top-tier model when writing PL3-PW proofs that the model itself recognizes as errors, and average rating of the difficulty/subtlety of these errors, given by the same model, with 1 being trivial and 5 being very complex. Here # of Logical Errors is proof-level: one per incorrect proof; we are not counting all erroneous steps.

Figure 29: Mean values of key numeric features of PL3-PC problems, organized by problem type.

Model	Accuracy	Guessing Only	Model	Accuracy	Guessing Only
gemini-3.1-pro-preview	0.96 $\;(\pm\>0.02)$	0.98 $\;(\pm\>0.02)$	gemini-3.0-pro-preview	0.95 $\;(\pm\>0.03)$	0.96 $\;(\pm\>0.02)$
claude-opus-4-5-20251101	0.93 $\;(\pm\>0.03)$	0.95 $\;(\pm\>0.03)$	gpt-5.1	0.89 $\;(\pm\>0.04)$	0.92 $\;(\pm\>0.03)$
claude-sonnet-4.5-ext-thinking	0.88 $\;(\pm\>0.04)$	0.93 $\;(\pm\>0.03)$	gpt-5	0.87 $\;(\pm\>0.04)$	0.91 $\;(\pm\>0.03)$
grok-4	0.86 $\;(\pm\>0.04)$	0.87 $\;(\pm\>0.04)$	gpt-5.2	0.84 $\;(\pm\>0.04)$	0.88 $\;(\pm\>0.04)$
o3	0.83 $\;(\pm\>0.04)$	0.87 $\;(\pm\>0.04)$	deepseek-r1-0528	0.78 $\;(\pm\>0.05)$	0.82 $\;(\pm\>0.04)$
gemini-2.5-pro	0.76 $\;(\pm\>0.05)$	0.79 $\;(\pm\>0.05)$	deepseek-reasoner	0.72 $\;(\pm\>0.05)$	0.77 $\;(\pm\>0.05)$

Table 16: PL3-PC accuracies and guessing-only accuracies.

Model	Accuracy	Guessing Only	Model	Accuracy	Guessing Only
gemini-3.0-pro-preview	0.91 $\;(\pm\>0.08)$	0.98 $\;(\pm\>0.05)$	gemini-3.1-pro-preview	0.88 $\;(\pm\>0.09)$	1.0 $\;(\pm\>0.03)$
gpt-5.1	0.83 $\;(\pm\>0.1)$	0.98 $\;(\pm\>0.05)$	claude-opus-4-5-20251101	0.75 $\;(\pm\>0.11)$	0.91 $\;(\pm\>0.08)$
gemini-2.5-pro	0.67 $\;(\pm\>0.12)$	0.87 $\;(\pm\>0.09)$	gpt-5.2	0.64 $\;(\pm\>0.13)$	0.91 $\;(\pm\>0.08)$
grok-4	0.6 $\;(\pm\>0.13)$	0.64 $\;(\pm\>0.13)$	gpt-5	0.6 $\;(\pm\>0.13)$	0.81 $\;(\pm\>0.1)$
o3	0.52 $\;(\pm\>0.13)$	0.75 $\;(\pm\>0.11)$	claude-sonnet-4.5-ext-thinking	0.49 $\;(\pm\>0.13)$	0.76 $\;(\pm\>0.11)$
deepseek-r1-0528	0.42 $\;(\pm\>0.13)$	0.62 $\;(\pm\>0.13)$	o3-mini	0.3 $\;(\pm\>0.12)$	0.89 $\;(\pm\>0.09)$

Table 17: PL3-PC accuracies and guessing-only accuracies restricted to the set of incorrect proofs.

Figure 30: PL3-PC accuracy per problem type.

Figure 31: Error distribution across the 4 error types for PL3-PC .

Figure 32: PL3-PC accuracy, excluding De Bruijn problems, as a function of proof length for the top 12 models.

Figure 33: ESI curves for different values of the curvature parameter ( $\gamma$ ). The $x$ -axis is the fraction $|\mbox{Inc\/}_{\mbox{$\mathcal{D}$}_{1}}[\mbox{$\mathcal{D}$}_{2}]|$ $/$ $n$ . — Figure 33: ESI curves for different values of the curvature parameter ( $\gamma$ ). The $x$ -axis is the fraction $|\mbox{Inc\/}_{\mbox{$ \mathcal{D} $}_{1}}[\mbox{$ \mathcal{D} $}_{2}]|$ $/$ $n$ .

Model	ESI	Model	ESI
gemini-2.5-pro	0.27	gpt-5	0.27
gpt-5.1	0.38	gemini-3.0-pro-preview	0.41
claude-opus-4-5-20251101	0.48	grok-4	0.52
o3	0.53	gemini-3.1-pro-preview	0.61
gpt-5.2	0.62

Table 18: Epistemic stability values for PL3-PW proofs relative to individual entailment judgments for the 9 models of Table 15 . A model’s ESI value can be understood as the probability that a randomly chosen PL3-PW proof written by the model is consistent with the model’s individual entailment judgments. Ideally, all of these values would be 1.

Panel of Figure 34 — Figure 34: Problem size distributions for PL4-PW (left) and PL4-PW-c (right).

Formula Feature	Mean	Max
Size	20.97	52
Atoms	8.24	19
Negations	7.17	23
Conjunctions	0.00	0
Disjunctions	0.00	0
Conditionals	5.55	15

Table 19: PL4-PW Problem Statistics. Size = total number of nodes across all formulas; Atoms = number of propositional variables; Negations, Conjunctions, Disjunctions, Conditionals, Biconditionals = counts of respective logical connectives.

Model	Strict	Lenient	Model	Strict	Lenient
gemini-3.1-pro-preview	0.55 ( $\pm$ 0.04)	0.71 ( $\pm$ 0.03)	gpt-5.2	0.26 ( $\pm$ 0.03)	0.39 ( $\pm$ 0.03)
gemini-3.0-pro-preview	0.20 ( $\pm$ 0.03)	0.23 ( $\pm$ 0.03)	grok-4	0.10 ( $\pm$ 0.02)	0.16 ( $\pm$ 0.03)
claude-opus-4-5-20251101	0.14 ( $\pm$ 0.02)	0.14 ( $\pm$ 0.02)	deepseek-reasoner	0.12 ( $\pm$ 0.02)	0.14 ( $\pm$ 0.02)
gpt-5	0.11 ( $\pm$ 0.02)	0.14 ( $\pm$ 0.02)	gpt-5.1	0.07 ( $\pm$ 0.02)	0.14 ( $\pm$ 0.02)
gemini-2.5-pro	0.08 ( $\pm$ 0.02)	0.12 ( $\pm$ 0.02)	o3	0.06 ( $\pm$ 0.02)	0.12 ( $\pm$ 0.02)
claude-sonnet-4.5-ext-thinking	0.12 ( $\pm$ 0.02)	0.12 ( $\pm$ 0.02)	deepseek-r1-0528	0.09 ( $\pm$ 0.02)	0.10 ( $\pm$ 0.02)

Table 20: PL4-PW accuracies in strict and lenient modes. Top accuracies in both modes are shown in bold.

Model	Accuracy
gemini-3.1-pro-preview	0.12
gpt-5.2	0.06
gemini-3.0-pro-preview	0.02
grok-4	0.00
claude-opus-4-5-20251101	0.00
deepseek-reasoner	0.00

Table 21: PL4-PW-c accuracies for top-performing models.

Model	Number of Proof Steps
	$\varphi_{1}$	$\varphi_{2}$	$\varphi_{3}$	$\varphi_{4}$	$\varphi_{5}$
gemini-3.1-pro-preview	9	25	19	55	59
gpt-5.2	25	25	19	-	-
gemini-3.0-pro-preview	-	25	19	-	-
grok-4	-	-	-	-	-
claude-opus-4-5-20251101	-	25	19	-	-

Table 22: Performance of leading models on 5 simple tautologies in PL4-PW . The number of steps of a successful proof is shown for each model and formula; a dash indicates failure to produce a correct proof.

Figure 35: The distribution of error types in PL4-PW under lenient proof checking, for the first error that caused a proof failure (or the failure to return a proof).

Figure 36: PL4-PW accuracy as a function of problem size.

Figure 37: PL4-PW proof-size distributions per model: all proofs (blue) vs correct proofs (green); min–max line, 5–95% band, IQR box, median tick, mean dot.

Model	Avg $\ell/\ell_{\min}$ (C)	Avg $\ell/\ell_{\min}$ (I)	Ratio (I/C)
grok-3	1.00	0.93	0.93
deepseek-v3.1	1.00	0.98	0.98
claude-sonnet-4-20250514	1.00	0.94	0.94
hermes-4	1.00	0.82	0.82
o3-mini	1.03	0.62	0.60
o3	1.03	1.01	0.98

Table 23: Proof length ratio analysis on

\textsc{PL}_{4}

-PW problems of moderate difficulty (problems with

\geq 3

correct and

\geq 3

incorrect proofs among models). For each model we show mean

\ell/\ell_{\min}

ratios, where

\ell

is proof length and

\ell_{\min}

is the length of the shortest correct proof for that problem. C (I) = correct (incorrect) proofs. Rows are ranked by avg(C), lower is better.

Figure 38: Pairwise proof similarity between models on $\textsc{PL}_{4}$ -PW problems. Models are grouped by hierarchical clustering based on fingerprint similarity. Yellow indicates higher similarity; dark blue indicates lower similarity.

$s$	$=$	$s_{0}$
	$=$	$s_{1}$	by $\cdots$
	$=$	$s_{2}$	by $\cdots$
	$\vdots$	$\vdots$	$\vdots$
	$=$	$s_{n}$	by $\cdots$

Table 65

$s$	$=$	$g(\mbox{$ \color[rgb]{1,0,0}\underline{{\color[rgb]{0,0,0}h(c,a,c)}}\color[rgb]{0,0,0} $},h(a,c,a))$
	$=$	$g(\mbox{$ \color[rgb]{0,0,1}\underline{{\color[rgb]{0,0,0}h(a,a,f_{4}(f_{1}(c)))}}\color[rgb]{0,0,0} $},\mbox{$ \color[rgb]{1,0,0}\underline{{\color[rgb]{0,0,0}h(a,c,a)}}\color[rgb]{0,0,0} $})$	by $E_{1}$
	$=$	$g(\mbox{$ \color[rgb]{1,0,0}\underline{{\color[rgb]{0,0,0}h(a,a,f_{4}(f_{1}(c)))}}\color[rgb]{0,0,0} $},\mbox{$ \color[rgb]{0,0,1}\underline{{\color[rgb]{0,0,0}g_{2}(a,c)}}\color[rgb]{0,0,0} $})$	by $E_{2}$
	$=$	$g(\mbox{$ \color[rgb]{0,0,1}\underline{{\color[rgb]{0,0,0}g_{1}(\mbox{\mbox{ $\color[rgb]{1,0,0}\underline{{\color[rgb]{0,0,0}f_{2}(f_{4}(a))}}\color[rgb]{0,0,0}$ }},f_{4}(e))}}\color[rgb]{0,0,0} $},g_{2}(a,c))$	by $E_{3}$
	$=$	$g(g_{1}(\mbox{$ \color[rgb]{0,0,1}\underline{{\color[rgb]{0,0,0}\mbox{ $\color[rgb]{1,0,0}\underline{{\color[rgb]{0,0,0}g(f_{3}(a),f_{2}(e))}}\color[rgb]{0,0,0}$ }}}\color[rgb]{0,0,0} $},\mbox{$ \color[rgb]{1,0,0}\underline{{\color[rgb]{0,0,0}f_{4}(e)}}\color[rgb]{0,0,0} $}),g_{2}(a,c))$	by $E_{4}$
	$=$	$g(g_{1}(\mbox{$ \color[rgb]{0,0,1}\underline{{\color[rgb]{0,0,0}g_{4}(f_{1}(f_{5}(f_{3}(a))),d)}}\color[rgb]{0,0,0} $},\mbox{$ \color[rgb]{0,0,1}\underline{{\color[rgb]{0,0,0}e}}\color[rgb]{0,0,0} $}),g_{2}(a,c))$	by $E_{5},E_{6}$

Table 66

$\vdots$	$\vdots$	$\vdots$
$=$	$r(h(e,e,c),g(c,b),g(\mbox{$ \color[rgb]{1,0,0}\underline{{\color[rgb]{0,0,0}f_{4}(f_{3}(b))}}\color[rgb]{0,0,0} $},a),g(f_{2}(a),g_{1}(a,c)))$	by $E_{2},E_{3}$
$=$	$r(h(e,e,c),g(c,b),g(\mbox{$ \color[rgb]{0,0,1}\underline{{\color[rgb]{0,0,0}f_{2}(g(b,f_{4}(e)))}}\color[rgb]{0,0,0} $},a),g(f_{2}(a),g_{1}(a,c)))$	by $E_{4},E_{5}$

Table 67

Model	L1	L2	L3	Model	L1	L2	L3
gemini-3.1-pro-preview	0.98 $\;(\pm\>0.02)$	0.93 $\;(\pm\>0.04)$	0.93 $\;(\pm\>0.04)$	gpt-5.1	0.90 $\;(\pm\>0.04)$	0.81 $\;(\pm\>0.05)$	0.76 $\;(\pm\>0.06)$
gpt-5.2	0.97 $\;(\pm\>0.03)$	0.82 $\;(\pm\>0.05)$	0.75 $\;(\pm\>0.06)$	gemini-3.0-pro-preview	0.98 $\;(\pm\>0.02)$	0.76 $\;(\pm\>0.06)$	0.74 $\;(\pm\>0.06)$
claude-opus-4-5-20251101	0.99 $\;(\pm\>0.02)$	0.74 $\;(\pm\>0.06)$	0.71 $\;(\pm\>0.06)$	gpt-5	0.95 $\;(\pm\>0.03)$	0.77 $\;(\pm\>0.06)$	0.69 $\;(\pm\>0.06)$
o3	0.88 $\;(\pm\>0.05)$	0.69 $\;(\pm\>0.06)$	0.58 $\;(\pm\>0.07)$	grok-4	0.90 $\;(\pm\>0.04)$	0.67 $\;(\pm\>0.06)$	0.56 $\;(\pm\>0.07)$
claude-sonnet-4.5-ext-thinking	0.97 $\;(\pm\>0.03)$	0.64 $\;(\pm\>0.07)$	0.56 $\;(\pm\>0.07)$	deepseek-reasoner	0.89 $\;(\pm\>0.04)$	0.62 $\;(\pm\>0.07)$	0.53 $\;(\pm\>0.07)$
gemini-2.5-pro	0.87 $\;(\pm\>0.05)$	0.56 $\;(\pm\>0.07)$	0.52 $\;(\pm\>0.07)$	o4-mini	0.69 $\;(\pm\>0.06)$	0.62 $\;(\pm\>0.07)$	0.43 $\;(\pm\>0.07)$

Table 26: Equational proof-checking accuracies at 3 levels of detail.

Figure 39: Level-2 error distribution for equational proof checking.

Model	PLA	SLA	Model	PLA	SLA
gpt-5.2	0.94 $\;(\pm\>0.03)$	0.99 $\;(\pm\>0.02)$	gpt-5.1	0.92 $\;(\pm\>0.04)$	0.99 $\;(\pm\>0.02)$
gemini-3.1-pro-preview	0.79 $\;(\pm\>0.06)$	0.98 $\;(\pm\>0.02)$	gemini-2.5-pro	0.78 $\;(\pm\>0.06)$	0.98 $\;(\pm\>0.02)$
gpt-5	0.77 $\;(\pm\>0.06)$	0.98 $\;(\pm\>0.02)$	claude-opus-4-5-20251101	0.70 $\;(\pm\>0.06)$	0.97 $\;(\pm\>0.03)$
gemini-3.0-pro-preview	0.69 $\;(\pm\>0.06)$	0.97 $\;(\pm\>0.03)$	o3	0.67 $\;(\pm\>0.06)$	0.96 $\;(\pm\>0.03)$
claude-sonnet-4.5-ext-thinking	0.62 $\;(\pm\>0.07)$	0.96 $\;(\pm\>0.03)$	grok-4	0.60 $\;(\pm\>0.07)$	0.94 $\;(\pm\>0.03)$
deepseek-reasoner	0.44 $\;(\pm\>0.07)$	0.54 $\;(\pm\>0.07)$	o3-mini	0.39 $\;(\pm\>0.07)$	0.83 $\;(\pm\>0.05)$

Table 27: EQ-ER performance; PLA = Proof-Level Accuracy, SLA = Step-Level Accuracy.

Figure 40: Normalized distribution of step-level ER errors.

Panel of Table 28 — Table 28: Data distribution summaries with inline box–sparklines for the gap-filling task slice of $\textsc{EQ}_{1}$ . Box = IQR (Interquartile Range); red line = median; dot = mean; whiskers = 5–95th.

Model	Proofs Written	Model	Proofs Written
deepseek-v3.1	43	deepseek-v3	44
o4-mini	49	deepseek-r1-0528	63
deepseek-reasoner	67	o3-mini	86
grok-4	104	o3	104
gpt-5.1	105	gemini-2.5-pro	111
gpt-5	114	claude-opus-4-5-20251101	129

Table 29: Number of nonempty proof completions written for the gap-filling task.

Figure 41: Completion length distribution by model (using boxplots and log scale).

Model	Accuracy	Model	Accuracy
gemini-3.1-pro-preview	0.82 $\;(\pm\>0.05)$	gemini-3.0-pro-preview	0.62 $\;(\pm\>0.07)$
gpt-5.2	0.61 $\;(\pm\>0.07)$	gpt-5	0.49 $\;(\pm\>0.07)$
gpt-5.1	0.49 $\;(\pm\>0.07)$	grok-4	0.48 $\;(\pm\>0.07)$
claude-opus-4-5-20251101	0.41 $\;(\pm\>0.07)$	gemini-2.5-pro	0.40 $\;(\pm\>0.07)$
o3	0.32 $\;(\pm\>0.06)$	deepseek-reasoner	0.27 $\;(\pm\>0.06)$
claude-sonnet-4.5-ext-thinking	0.18 $\;(\pm\>0.05)$	claude-opus-4-20250514	0.17 $\;(\pm\>0.05)$

Table 30: Gap-Filling accuracies.

Figure 43: Prevalence of errors of different types in the gap-filling task.

Figure 44: Gap-filling accuracy for the top 10 models as a function of gap size.

Figure 45: Gap-filling accuracy for the top 10 models as a function of equational theory size.

Figure 46: Consolidated accuracy heat map for gap filling, as a function of gap length and equational theory size.

Figure 47: Gap-filling calibration errors across all models (bin-level and overall ECE).

Appendix figures & tables12 assets

Supplementary material from the paper’s appendix.

Appendix

$\alpha\backslash(\theta-b_{j})$	$-3$	$-2$	$-1$	$-0.5$	$0$	$0.5$	$1$	$2$	$3$
$0.2$	0.354	0.401	0.450	0.475	0.500	0.525	0.550	0.599	0.646
$0.5$	0.182	0.269	0.378	0.438	0.500	0.562	0.622	0.731	0.818
$1$	0.047	0.119	0.269	0.378	0.500	0.622	0.731	0.881	0.953
$2$	0.002	0.018	0.119	0.269	0.500	0.731	0.881	0.982	0.998
$3$	0.000	0.002	0.047	0.182	0.500	0.818	0.953	0.998	1.0

Appendix

Table 31: Success probabilities under the 2PL model,

p=\sigma\!\bigl(\alpha(\theta-b_{j})\bigr)

, for several values of the discrimination parameter

\alpha

and the margin

\theta-b_{j}

. As the margin increases, the probability of success rises; larger values of

\alpha

make this rise steeper.

Figure 49: Three ICCs for three sample PL2-PW problems.

Figure 50: Fisher information of a task item as a function of different $a$ (discrimination) values.

Model	Ability $\theta$	Model	Ability $\theta$
gemini-3.1-pro-preview	2.141	gemini-3.0-pro-preview	1.429
gpt-5.2	1.114	claude-opus-4-5-20251101	1.035
gpt-5.1	1.004	grok-4	0.756
gemini-2.5-pro	0.709	claude-sonnet-4.5-ext-thinking	0.624
gpt-5	0.613	o3	0.506
deepseek-reasoner	0.176	deepseek-r1-0528	0.076

Appendix

Table 32: PL1-PM

\theta

parameters estimated from the task results.

Figure 51: The task-information curve of proof masking over the entire observed ability range.

Model	Ability $\theta$	Model	Ability $\theta$
gemini-3.0-pro-preview	1.577	gemini-3.1-pro-preview	1.491
claude-opus-4-5-20251101	1.167	gpt-5.1	0.902
gpt-5	0.814	claude-sonnet-4.5-ext-thinking	0.803
grok-4	0.747	gpt-5.2	0.609
o3	0.606	deepseek-r1-0528	0.489
gemini-2.5-pro	0.404	deepseek-reasoner	0.358

Appendix

Table 33: Model

\theta

parameters estimated from PL3-PC results.

Figure 52: Ability parameters estimated from PL4-PW results, alongside the task-information curve of Hilbert proof-writing over the observed ability range. Information is low for models of ability $\theta<0$ .

Family	Representative models	Primary API path	Batch mode	Default timeout
OpenAI reasoning models	gpt-5 , gpt-5.1 , gpt-5.2 , o3 , o3-mini , o4-mini	OpenAI Responses API in serial mode; OpenAI batch API available in the codebase	Serial in the reported runs	30 minutes
OpenAI chat models	gpt-4o , gpt-4.1	OpenAI Chat Completions API	Serial in the reported runs	30 minutes
Anthropic Claude models	claude-sonnet-4-20250514 , claude-sonnet-4.5 , claude-opus-4-20250514 , claude-opus-4.5	Anthropic Messages API in serial mode; Anthropic Message Batches in batch mode	Batch used in the reported runs, with serial fill-ins	30 minutes
Google Gemini models	gemini-2.5-pro , gemini-3-pro-preview , gemini-3.1-pro-preview	Google genai client, generate_content	Serial in the reported runs	30 minutes
DeepSeek models	deepseek-v3 , deepseek-v3.1 , deepseek-r1 , deepseek-reasoner	DeepSeek chat-completions-compatible API	No separate batch wrapper in the main benchmark path	30 minutes
xAI models	grok-3 , grok-4 , grok-4.20	xAI chat-completions-compatible API	No separate batch wrapper in the main benchmark path	30 minutes

Appendix

Table 34: Provider routing used. Model identifiers follow the naming scheme used in this paper; our public release artifacts expose the underlying provider identifiers as well.

ID used in this article	Queried model id	Run window
OpenAI
gpt-5	gpt-5	Aug. 2025–Mar. 2026
gpt-5.1	gpt-5.1	Nov. 2025–Mar. 2026
gpt-5.2	gpt-5.2	Dec. 2025–Mar. 2026
o3-mini	o3-mini	Apr. 2025–Mar. 2026
o4-mini	o4-mini	Apr. 2025–Mar. 2026

Appendix

Table 35: The 24-model set reported in the paper, shown under the paper naming scheme together with the exact queried model identifiers and the observed run windows in the released archives.

Task	Prompt style	Required output format
NDL/ $\mbox{\rm NDL}_{0}$ proof writing ( $\textsc{PL}_{1}$ , $\textsc{PL}_{2}$ , $\textsc{PL}_{3}$ )	Few-shot	JSON dictionary containing at least a proof and a description/explanation of the proof reasoning
Hilbert proof writing ( $\textsc{PL}_{4}$ )	Few shot	JSON dictionary containing a Hilbert proof and a short description
Proof checking	Few-shot	JSON dictionary containing a Boolean verdict and structured error information
Mask filling	Few-shot	JSON dictionary specifying the model’s mask assignments
Gap filling	Few-shot	Free text containing one block per gap
Equational reasoning	Few shot	Structured JSON output (including confidence levels for EQ-GF )

Appendix

Table 36: Prompt/input and output structure by task family.

Model group	Serial-mode policy	Batch-mode policy	Notes
gpt-5 , gpt-5.1	Responses API; temperature not set; reasoning effort high ; max_output_tokens =72K	Not used for the reported results	JSON-constrained tasks use the Responses-API text-format JSON path
gpt-5.2	Responses API; temperature not set; reasoning effort high ; automatic extra-thinking budget of 64K on tasks that expose it; max_output_tokens =112K	Not used for the reported results	Used with the larger GPT-5 token budget path
OpenAI o-series ( o3 , o3-mini , o4-mini )	Responses API; temperature not set; reasoning effort high ; max_output_tokens =72K	Not used for the reported results	The reported o-series results were effectively serial
claude-sonnet- 4.5-ext- thinking	Anthropic Messages API; temperature omitted when thinking is enabled; thinking budget 12K; max_tokens =21,333	Anthropic Message Batches; thinking budget 16K; max_tokens =64K	Explicit extended thinking; stop reason is recorded when available in serial mode
claude-opus- 4.5	Anthropic Messages API; temperature omitted when thinking is enabled; thinking budget 12K; max_tokens =21,333	Anthropic Message Batches; max_tokens =64K; effective thinking budget 32K after buffer reservation	Explicit extended thinking in both serial and batch paths
claude-sonnet- 420250514	Anthropic Messages API; task temperature; no explicit thinking; max_tokens =21,333	Anthropic Message Batches; no explicit thinking; max_tokens =64K	No extended thinking in the reported runs

Appendix

Table 37: Compact summary of the main decoding, reasoning, and token-budget policies.

LLM Evaluation

Large language model evaluation measures what models can do, how reliably they do it, and whether benchmark scores predict real-world performance.

See all 2,408 papers

X-RAY: Mapping LLM Reasoning Capability via Formalized and Calibrated Probes
Mar 5, 2026Tianxi Gao, Yufan Cai, Yusi Yuan +1Structured Reasoning in Language Models Reasoning Evaluation
National University of Singapore, Singapore
LGMT: Logic-Grounded Metamorphic Testing for Evaluating the Reasoning Reliability of LLMs
May 12, 2026Zenghui Zhou, Man Li, Xiaoke Fang +3LLM Evaluation Automated Software Testing
School of Automation Science and Electrical Engineering, Beihang University, Xueyuan Road, Haidian District, Beijing, 100191, China
Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning
Sep 29, 2026Qili Zhang, Qianren Mao, Hanze Cai +11Logical Reasoning RL for Language Model Reasoning
Zhongguancun Laboratory · Beihang University · Nanyang Technological University +1

Mar 5, 2026J/K move · Enter open · S save

X-RAY: Mapping LLM Reasoning Capability via Formalized and Calibrated Probes

Tianxi Gao, Yufan Cai, Yusi Yuan, Jin Song Dong

National University of Singapore, Singapore

Structured Reasoning in Language Models Reasoning Evaluation LLM Reasoning Implicit Reasoning in Language Models Scientific Reasoning in Language Models

Open paper AskPDF arXiv

Large language models (LLMs) achieve promising performance, yet their ability to reason remains poorly understood. Existing evaluations largely emphasize task-level accuracy, often conflating pattern matching with reasoning capability. We present X-RAY, an explainable reasoning analysis system that maps the LLM reasoning capability using calibrated, formally verified probes. We model reasoning capability as a function of extractable structure, operationalized through formal properties such as constraint interaction, reasoning depth, and solution-space geometry. X-Ray generates probes via formal tools with controlled structural variations, enabling precise isolation of incremental structural information through formal calibration and verification. We evaluate state-of-the-art LLMs on problems ranging from junior-level to advanced in mathematics, physics, and chemistry. Our analysis reveals a systematic asymmetry in LLM reasoning: models are relatively robust to constraint refinement, where additional conditions shrink an existing solution space, but degrade sharply under solution-space restructuring, where modifications alter the underlying structural form of the solution manifold. Moreover, calibrated formal probes differentiate models that appear indistinguishable on standard benchmarks and reveal failure modes that are structurally interpretable rather than opaque. Beyond evaluation, our framework is contamination-free and supports the training and testing of reasoning models.

Abstract

LLM Evaluation

Explore similar work

X-RAY: Mapping LLM Reasoning Capability via Formalized and Calibrated Probes

LGMT: Logic-Grounded Metamorphic Testing for Evaluating the Reasoning Reliability of LLMs

Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning