Reasoning language models are trained to produce solutions, not to refuse them, and this bias persists when the problem they are handed is false. Asked to prove a corrupted theorem, a strong model will typically comply and produce a confident derivation of something untrue. We present Euston, an 8B mathematical claim-verification model trained to resist exactly this. Training data were generated with GraphSynth, a probabilistic factor-graph generator that couples attribute-level diversity to decode-time structural masking and span-synchronized verification, yielding 3{,}026 matched true/corrupted statement pairs (6,052 statements) drawn from arXiv papers spanning 2010--2025. We fine-tuned DeepSeek-R1-8B with GRPO under a rule-based, zero-API reward for 189 steps on four H100 GPUs. On a balanced 200-true/200-false held-out split, balanced accuracy rises from 29.50% to 63.75% and the discrimination gap---the difference between the rate of calling false statements false and the rate of calling true statements false moves from -0.5% (z=-0.1) to +27.5% (z=+6.0). Critically, the gain is not purchased with general mathematical ability: AIME 2026 accuracy under official semantics is 65.00% against a 69.17% base, a difference of -4.17% that is not statistically significant, whereas an earlier run of the same recipe on a smaller GraphSynth corpus collapsed to 40.00%. Median response length also falls from 19,217 to 18,296 tokens and the truncation rate from 25.8% to 8.3%, so the improvement does not come from thinking longer. We report the result together with the confounds that bound its interpretation, principally the all-false composition of the official evaluation sets and the low precision implied at realistic error prevalence.
Figures & tables
Component
Setting
Base model
deepseek-ai/DeepSeek-R1-0528-Qwen3-8B (8B, BF16)
Algorithm
GRPO ( verl )
KL loss coefficient
0.001
Entropy coefficient
0
Reward
Rule-based, zero-API; 1.0 iff final \boxed{} casefold-matches label
Learning rate
5×10−6
Table 1: Training configuration. The run consumed roughly 13.8 hours of wall-clock time.
Figure 1: Verdict quality on the balanced held-out split (200 true, 200 false; one pair per source paper). Dashed lines mark chance. The left panel scores unparseable outputs as wrong, the middle panel conditions on a parseable verdict, and the right panel reports the pairwise score over all 200 pairs with ties credited 0.5.
Metric
Base
Euston-pilot
Euston
Balanced accuracy (chance = 50%)
29.50%
56.75%
63.75%
among parseable verdicts only
47.58%
60.05%
63.91%
Discrimination gap
−0.5 pp
+19.0 pp
+27.5 pp
significance
z=−0.1
z=+3.9
z=+6.0
Positive likelihood ratio (LR + )
0.99
1.42
1.53
False-rejection rate on TRUE statements
38.5%
45.5%
51.5%
Table 2: Balanced held-out split: 200 true and 200 false statements, one pair per source paper. The discrimination gap is P(say false∣false)−P(say false∣true) .
Metric
Base
Euston-pilot
Euston
Coverage (pairs given different verdicts)
21%
42%
41%
Accuracy within coverage
40.5%
71.1%
84.1%
Pairwise score, all 200 pairs (ties = 0.5)
48.0%
58.8%
64.0%
Table 3: Pairwise adjudication over 200 matched pairs. Coverage is the fraction of pairs receiving different verdicts for the two members; accuracy within coverage conditions on those pairs.
Figure 2: The capability–discrimination plane. Both training runs move right, acquiring discrimination. Euston-pilot falls off the capability axis; Euston does not. The two runs differ in the volume of generated data they were trained on, not in the optimiser.
Scoring
Base
Euston
Difference
Lower bound (official semantics)
69.17%
65.00%
−4.17 pp, 95% CI [−10.83,+2.50] , n.s.
Upper bound (landed runs only)
89.51%
71.26%
−12.96 pp, 95% CI [−21.91,−4.94] , sig.
Runs dropped
25.8%
8.3%
—
Table 4: AIME 2026 (30 problems, n=4 samples each). The lower bound follows official semantics and scores dropped runs as wrong; the upper bound conditions on runs that landed.
Figure 3: Generation-budget behaviour. Euston improves discrimination while producing shorter outputs than the base model and truncating far less often; Euston-pilot shows the length inflation typical of unregularised RL on reasoning tasks.
Figure 4: The two ablation axes. Left, balanced accuracy on the held-out split; right, the discrimination gap. Hatched bars are the approximate values, reconstructed from the original run logs. Neither axis alone reaches the top of the chart: better negatives without on-policy pressure (Panel B) and on-policy pressure on weaker or fewer negatives (Panel A) both fall short of Euston.
Large language models often solve a theorem forward yet fail to disprove a closely related false one: a falsification gap that supervised fine-tuning does not close and can actively worsen. We frame counterexample generation as constrained witness emission against a deterministic per-theorem Python verifier, and release SymCE, a corpus of 4,707 false undergraduate-algebra and real-analysis conjectures, each paired with executable verifiers. The verifier also serves as the reward function, making SymCE a training environment. Training Qwen3-4B with SFT followed by GRPO under this oracle reveals an imitation trap: counterexample-only SFT collapses true-theorem recognition from 0.27 to 0.00, while RLVR with a sparse outcome-only reward repairs this and exceeds the base, to 0.66. The collapse replicates across four seeds and on Gemma-3-4B. Sparse and dense rewards yield statistically indistinguishable in-domain success yet diverge by 33 points on a held-out calibration probe, a dissociation we trace to the partial-credit term. Our 4B model outperforms every evaluated 7B open-weights math specialist, remains competitive with six frontier commercial APIs, and transfers under unchanged prompting to GSM8K, MATH-500 and MMLU-college-math. A human audit of 177 verifier decisions finds 97.7% accuracy. Code, data, verifier modules and annotations: https://github.com/ce-rlvr/SymCE.
Language models have recently solved open Erdős problems and achieved gold-medal level performance on International Mathematical Olympiad problems. But their solutions, written in natural language, cannot yet be verified by proof assistants. An erroneous reasoning step can invalidate every step that comes after, so it is advantageous to detect errors early. Several methods have been proposed to detect erroneous reasoning quickly based on the features of the forward pass of the language model that performs reasoning. In this work, we study whether the directed Forman curvature of that model's attention graph, a local quantity computed at an edge from the attention weights around it, carries information about a step's correctness. To do so, we evaluate four per-step verifiers on ProcessBench with and without the curvature appended to their input. Appending curvature values improves the overall mean performance of all four verifiers. ReProbe, the verifier that takes every token of a step as input, shows the largest improvement. Adding the curvature increases the time of the language model's forward pass by 18% on average.
Advances in training, post-training, and inference-time methods have enabled frontier reasoning models to win gold medals in math competitions and settle challenging open problems. Gaining trust in the responses of these models requires that natural language proofs be checked for errors. LLM judges are increasingly being adopted to meet the growing demand for evaluating such proofs. While verification is considered easier than generation, what model capability does reliable verification actually require? We systematically evaluate four open-source and two frontier LLMs on datasets of human-graded natural language proofs of competition-level problems. We consider two key metrics: verifier accuracy and self-consistency (the rate of agreement across repeated judgments on the same proof). We observe that smaller open-source models are only up to ~10% behind frontier models in accuracy but they are up to ~25% more inconsistent. Furthermore, we see that verifier accuracy is sensitive to prompt choice across all models. We then demonstrate that the smaller models, in fact, do possess the mathematical capabilities to verify proofs at the level of frontier models, but they struggle to reliably elicit these capabilities with general judging prompts. Through an LLM-guided prompt search, we synthesize an ensemble of specialized prompts that overcome the specific failure modes of smaller models, boosting their performance by up to 9.1% in accuracy and 15.9% in self-consistency. These gains are realized across models and datasets, allowing models like Qwen3.5-35B to perform on par with frontier models such as Gemini 3.1 Pro for proof verification.