基于定理级符号验证器的反例生成：模仿学习为何失效，强化学习如何修复

# Counterexample Generation via Per-Theorem Symbolic Verifiers:When Imitation Hurts and Reinforcement Repairs
Source: [https://arxiv.org/html/2610.02444](https://arxiv.org/html/2610.02444)
Omar Farouk Zouak††thanks:Corresponding author:omar\.zouak@ensia\.edu\.dzHoussam Eddine BoukhalfaAffiliation:National School of Artificial Intelligence, Algiers, AlgeriaSoumaya LakehalAffiliation:National School of Artificial Intelligence, Algiers, AlgeriaShiv KatiyarAffiliation:University of Birmingham, United KingdomSamia Nefti\-MezianiAffiliation:University of Birmingham, United Kingdom

###### Abstract

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 releaseSymCE, 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, makingSymCEa 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](https://github.com/ce-rlvr/SymCE)\.

## 1Introduction

Large Language Models \(LLMs\) excel at forward mathematical derivation, but struggle significantly with inverse reasoning and generating counterexamples to false claims\. Recent benchmarks demonstrate that even frontier models fail at falsification tasks they can easily forward\-solve\([Sinha et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib2);[Li et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib1)\)\. Furthermore, standard imitation learning \(SFT\) often exacerbates this by inducing format\-biases rather than true logical reasoning\([Shao et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib21)\)\.

The natural fix is to train counterexample generation directly, but two obstacles have so far prevented this from becoming a primary objective\. First, large\-scale counterexample data is scarce: the only widely cited counterexample benchmark, COUNTERMATH, contains 1,216 problems, and its evaluation is mediated by an LLM judge\. Second, supervised fine\-tuning \(SFT\) on counterexamples appears insufficient\. Counterexample\-only training data contains, by construction, only false statements, and we show below that imitation\-only training transfers this distribution shift into the policy: a model trained purely to emit counterexamples loses the ability to recognise true statements, and confidently fabricates witnesses on theorems that are in fact true\.

We attack both obstacles together\. We buildSymCE, a deterministic, large\-scale counterexample environment, by hypothesis\-dropping over 6,748 undergraduate\-level theorems and generating, for each\(theorem\_id, dropped\_hypothesis\)pair, an independent Python verifier module that returns one boolean per remaining hypothesis and one for the negated conclusion\. The pipeline retains 4,707 records\. Evaluation is fully symbolic: the policy emits a one line Python expression, and the verifier returns a boolean tuple\. Because the verifier runs in tens of milliseconds, the same substrate serves as the reward function during reinforcement learning, soSymCEis a training environment and not only a benchmark\.

We use this environment to train Qwen3\-4B\([Qwen Team, 2025](https://arxiv.org/html/2610.02444#bib.bib25)\)with SFT followed by GRPO under two reward shapes and to evaluate against five 7B open\-weights math specialists, six commercial\-API frontier models, and four external mathematics benchmarks\.*In doing so, we uncover a pathology*: imitation\-only training on counterexamples collapses the policy’s ability to recognise true theorems, and only verifier\-grounded RL with an outcome\-only reward repairs it\. Partial\-credit dense rewards yield equal in\-domain success but do not restore calibration; a dissociation that, to our knowledge, has not been previously isolated\.

#### Contributions\.

We make four main contributions\.\(C1\) The Imitation Trap Pathology\.We isolate a calibration failure mode in counterexample\-only supervised fine\-tuning: Pass@1 on true theorems collapses from 0\.27 to 0\.00 under the training prompt style, because the policy learns the output*form*of a counterexample without the negated\-conclusion constraint\. The collapse reproduces in all four training seeds and on a second model family\.\(C2\) Verifier\-Grounded RLVR for Falsification\.We demonstrate that Reinforcement Learning with Verifiable Rewards \(RLVR\), guided by a deterministic symbolic execution interface, repairs this pathology\. Furthermore, we show that the partial\-credit reward term that is the natural dense shaping for this task structure preserves logical calibration markedly worse than an outcome\-only reward, and we identify the mechanism\.\(C3\) Strong Empirical Performance & Transfer\.Our Qwen3\-4B RLVR model achieves 0\.49±\\pm0\.02 Pass@1 on in\-domain falsification across four seeds, outperforming all evaluated 7B open\-weights math specialists and remaining competitive with frontier APIs, while demonstrating strong zero\-shot transfer to standard forward\-math tasks \(MATH\-500, GSM8K\)\.\(C4\)SymCE: A Deterministic Falsification Environment\.To enable this training, we introduce and release a programmatically verifiable corpus of 4,707 false algebraic conjectures with per\-theorem executable verifiers, moving beyond the noisy LLM\-as\-a\-judge paradigm\.

## 2Related Work

#### Counterexample and falsification benchmarks\.

The closest comparable resource for counterexample reasoning is COUNTERMATH\([Li et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib1)\), a 1,216\-problem benchmark of university\-level counterexample\-driven proofs evaluated with an LLM\-as\-judge protocol; the largest frontier model reported in that work achieves an F1 of 60\.1\. REFUTE\([Sinha et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib2)\)measures counterexample success on algorithmic problems and reports a sharp asymmetry between forward solution rates \(around 48 %\) and counterexample success \(below 9 %\) for the same models\. The most directly related training resource isLearning to Disprove\([Li et al\., 2026](https://arxiv.org/html/2610.02444#bib.bib3)\), which constructs roughly 575K hypothesis\-dropping mutations of Lean 4 Mathlib theorems and uses Lean tactic checks as the verification signal\. Our dataset is smaller than[Li et al\.](https://arxiv.org/html/2610.02444#bib.bib3)’s but uses a Python\-verifier substrate that is more faithful to the algebraic and real\-analytic structures evaluated, runs in tens of milliseconds rather than seconds, and is paired with the witness\-schema interface of §[3\.2](https://arxiv.org/html/2610.02444#S3.SS2)\. The Alchemy line of AST\-mutation work\([Wu et al\., 2024](https://arxiv.org/html/2610.02444#bib.bib4)\)focuses on generating valid mutated*true*theorems for automated theorem proving and is complementary rather than competing\.

#### Verifiable\-reward reinforcement learning for mathematics\.

RLVR with GRPO has become the dominant post\-training paradigm for forward mathematical reasoning, anchored by DeepSeek\-R1\([Guo et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib5)\)and adopted in PRIME\([Cui et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib6)\)and Eurus\([Yuan et al\., 2024](https://arxiv.org/html/2610.02444#bib.bib7)\)\. While recent studies debate whether RLVR installs new reasoning or merely elicits latent capabilities via format adaptation\([Shao et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib21)\), our out\-of\-distribution transfer results \(§[6\.5](https://arxiv.org/html/2610.02444#S6.SS5)\) suggest falsification training installs fundamentally transferable inverse\-reasoning skills\.

#### Process supervision and symbolic verifiers\.

Process reward models \(PRMs\), introduced for mathematical reasoning by[Lightman et al\. \(2024\)](https://arxiv.org/html/2610.02444#bib.bib24)and extended by Math\-Shepherd\([Wang et al\., 2023](https://arxiv.org/html/2610.02444#bib.bib8)\), and the FOVER pipeline\([Kamoi et al\., 2026](https://arxiv.org/html/2610.02444#bib.bib9)\), which mines step\-level labels from Z3 and Isabelle traces, supply dense supervision at the step level for forward proving\. Our per\-theorem verifier sits between an outcome reward model and a PRM: it returns one boolean per remaining hypothesis and one for the negated conclusion, which gives the reward function \(Eq\.[1](https://arxiv.org/html/2610.02444#S3.E1)\) a structured, audited signal without the human\-annotation cost of a learned PRM\. PRL\([Yao et al\., 2026](https://arxiv.org/html/2610.02444#bib.bib26)\)and self\-rewarding correction\([Xiong et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib27)\)bear directly on where such an intermediate signal sits; our boolean tuple differs from both in being externally grounded and non\-learned, which is what lets §[6\.3](https://arxiv.org/html/2610.02444#S6.SS3)attribute a behavioural change to one term of the aggregation\. SymPy and Z3\([Meurer et al\., 2017](https://arxiv.org/html/2610.02444#bib.bib10);[De Moura and Bjørner, 2008](https://arxiv.org/html/2610.02444#bib.bib11)\)provide the underlying verification primitives\.

#### The hallucination tax\.

A growing literature describes a calibration pathology induced by standard imitation\-style training: TreeCut\([Ouyang, 2025](https://arxiv.org/html/2610.02444#bib.bib12)\)demonstrates that LLMs continue to fabricate answers when problems are systematically modified to remove a critical constraint; SUM\([Song et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib13)\)and related work report refusal\-rate collapses of roughly 80 % under standard rejection\-sampling fine\-tuning on unanswerable\-math benchmarks\. Our imitation\-trap finding \(§[6\.2](https://arxiv.org/html/2610.02444#S6.SS2)\) is the cleanest measurement of this pathology in the counterexample\-generation setting we are aware of, and the first to localise the mechanism, via the reason taxonomy of §[6\.3](https://arxiv.org/html/2610.02444#S6.SS3), to the partial\-credit term of the reward function\.

## 3Dataset and Verification Environment

We frame counterexample generation as a constrained generation task: given a false conjecture of the form “ifH1∧⋯∧HkH\_\{1\}\\wedge\\cdots\\wedge H\_\{k\}thenQQ”, output a witnesswwsuch that all remaining hypotheses hold andQQfails onww\. Our environment is built around three design choices: a per\-theorem Python verifier compiled once and reused across all rollouts, a structured witness\-schema interface that constrains the policy’s output shape, and a conclusion\-weighted dense reward whose sparse counterpart we use for ablation\.

### 3\.1Source theorems and hypothesis dropping

We collected 6,748 unique undergraduate\-level mathematical theorems spanning six subdomains \(Group, Ring, Field and Number Theory, Linear Algebra and Real Analysis\)\. Each theorem is stored in a structured form with explicithypothesesandconclusionfields\. To construct false conjectures we drop one hypothesis at a time, giving 18,262 candidates\. Removing a hypothesis does not guarantee the result is false or even well\-posed — the hypothesis may be redundant or merely clarificatory — so we apply an LLM\-driven filter \(Gemini 3\.1 Pro\): the teacher must classify the mutated theorem as well\-posed and non\-trivial, emit a valid Python verifier, and propose a counterexample that evaluates toTrueon that verifier without execution errors, with up to 5 retries under error\-trace feedback\. The teacher produces a verifier for 12,376 candidates; gating then distils these to 4,707 verifier\-backed records over 3,485 unique theorems, of which 4,700 carry a witness schema \(§[3\.2](https://arxiv.org/html/2610.02444#S3.SS2)\)\. We report per\-subdomain counts in Table[1](https://arxiv.org/html/2610.02444#S3.T1)\.

A sandboxed subprocess imports the verifier dynamically, builds the witness\-evaluation namespace, evaluates the policy’s witness expression string in that namespace, and callsconditions\(witness\), which returns a list of booleans, one per remaining hypothesis followed by one for the negated conclusion\. The policy and the oracle share*no code paths*beyond Python’seval; the verifier is fixed at the start of training and reused across all rollouts for that conjecture\.

This is a deliberate departure from prior counterexample\-evaluation pipelines: COUNTERMATH\([Li et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib1)\)relies on an LLM\-as\-judge protocol, andLearning to Disprove\([Li et al\., 2026](https://arxiv.org/html/2610.02444#bib.bib3)\)relies on a Lean tactic check\. A Python module evaluated against a witness expression is intermediate: it is symbolic and decidable for the subdomains we target, fast \(§[3\.5](https://arxiv.org/html/2610.02444#S3.SS5)\), and reproducible\.

### 3\.2Witness\-schema interface

We attach to each prompt a one\-linewitness schema: a short Python\-shape description of an acceptable witness\. Schemas are generated post\-hoc by reading the verifier module and its canonical witness with a second teacher model \(DeepSeek\) and asking for a single\-sentence description of the expected Python object shape, with one or two concrete examples\. Sample schemas are shown in Appendix[H](https://arxiv.org/html/2610.02444#A8)\.

Schemas are merged into the user prompt\. We view this as a small but load\-bearing methodological contribution: a structural prior on the output shape, generated automatically from the verifier and a canonical witness, is what allows for the practical RLVR effectiveness without altering either the reward function or the verifier\.

### 3\.3Split construction

We construct three splits with per\-domain stratified sampling and a fixed seed \(42\): the held\-out test set \(n=201\), the SFT split \(n=1,000\), and the RLVR prompt set \(n=3,506\)\. Table[1](https://arxiv.org/html/2610.02444#S3.T1)summarises the splits\.

### 3\.4Reward function

The per\-rollout reward computed by the oracle is

r=\\displaystyle r=α⋅shypnhyp\+β⋅q¬\+γ⋅𝟏​\[format ok\]\\displaystyle\\alpha\\cdot\\frac\{s\_\{\\text\{hyp\}\}\}\{n\_\{\\text\{hyp\}\}\}\+\\beta\\cdot q\_\{\\neg\}\+\\gamma\\cdot\\mathbf\{1\}\[\\text\{format ok\}\]\(1\)−δ⋅𝟏\[gave up on false\]\\displaystyle\{\\displaystyle\-\}\\delta\\cdot\\mathbf\{1\}\[\\text\{gave up on false\}\]−ε⋅\(1−𝟏\[parse ok\]\),\\displaystyle\{\\displaystyle\-\}\\varepsilon\\cdot\(1\-\\mathbf\{1\}\[\\text\{parse ok\}\]\)\\,,whereshyp=∑i=1nhypconditions​\[i\]s\_\{\\text\{hyp\}\}=\\sum\_\{i=1\}^\{n\_\{\\text\{hyp\}\}\}\\texttt\{conditions\}\[i\]counts satisfied hypotheses,q¬=conditions​\[neg\_q\_index\]∈\{0,1\}q\_\{\\neg\}=\\texttt\{conditions\}\[\\texttt\{neg\\\_q\\\_index\}\]\\in\\\{0,1\\\}is the negated\-conclusion indicator, and the format / parse flags come from the structural and witness\-evaluation checks\. The penaltyδ\\deltaapplies when the policy emits the literal sentinelNONE\. Every training conjecture is false, so this is always a give\-up signal\.

#### Dense and sparse variants\.

We study two reward shapes\.Dense:α=0\.25,β=0\.65,γ=0\.10,δ=0\.30,ε=1\.00\\alpha\{=\}0\.25,\\beta\{=\}0\.65,\\gamma\{=\}0\.10,\\delta\{=\}0\.30,\\varepsilon\{=\}1\.00, range approximately\[−1,\+1\]\[\-1,\+1\]\.Sparse:α=γ=δ=0,β=ε=1\\alpha\{=\}\\gamma\{=\}\\delta\{=\}0,\\beta\{=\}\\varepsilon\{=\}1, range\{−1,0,\+1\}\\\{\-1,0,\+1\\\}\. The same SFT checkpoint is used as the reference policy for both\.

#### Conclusion\-weighting bound\.

A structural property of Eq\. \([1](https://arxiv.org/html/2610.02444#S3.E1)\) under dense weights is that any successful, formatting\-compliant rollout \(𝟏​\[format ok\]=𝟏​\[parse ok\]=1\\mathbf\{1\}\[\\text\{format ok\}\]=\\mathbf\{1\}\[\\text\{parse ok\}\]=1and𝟏​\[gave up on false\]=0\\mathbf\{1\}\[\\text\{gave up on false\}\]=0\) that falls into the “hypothesis\-only” failure mode \(shyp=nhyps\_\{\\text\{hyp\}\}=n\_\{\\text\{hyp\}\},q¬=0q\_\{\\neg\}=0\) is strictly dominated by any valid rollout that successfully negates the conclusion \(q¬=1q\_\{\\neg\}=1\):

rhyp\-only=α\+γ<β\+γ≤rneg\-Q\.r\_\{\\text\{hyp\-only\}\}\\;=\\;\\alpha\+\\gamma\\;<\\;\\beta\+\\gamma\\;\\leq\\;r\_\{\\text\{neg\-Q\}\}\.This structurally precludes the “all hypotheses satisfied but conclusion asserted true” failure mode that affects naïve formulations\([Li et al\., 2026](https://arxiv.org/html/2610.02444#bib.bib3)\)\.

### 3\.5Verifier audit and operational measurements

The verifiers are produced by a teacher model \(Gemini 3\.1 Pro\) and therefore must be audited before they can support a reward signal\. We audit the accept/reject*decision*on real policy outputs rather than the verifier source\. The generated verifiers decide conditions with heuristics and finite simplifications that are theoretically incomplete yet correct on the instances that arise, so a judgement on the source is slow to make and largely subjective; the decision is also the quantity the reward signal actually depends on\. This audit replaces a hand\-curated unit\-test suite over the verifier modules, which we abandoned for that reason\. We sampled 177 model\-generated witnesses from the held\-out test split across seeds and training configurations \(101 accepted by the verifier and 76 rejected\) and had an author with graduate\-level training in the relevant areas judge independently whether each is genuinely a valid counterexample\. Of the accepted, 99/101 were confirmed valid \(false\-accept rate 2\.0 %\); of the rejected, 74/76 were confirmed invalid, for 97\.7 % decision accuracy\.*No case was traced to an incorrect verifier module*, and we found no evidence of reward hacking through verifier acceptance\. A single study thus speaks to verifier trustworthiness, hypothesis\-drop label noise, reward hacking and witness\-schema quality at once\. Composition and the four disputed decisions are in Appendix[B](https://arxiv.org/html/2610.02444#A2); the annotations are released\.

Operationally, the sandbox is fast enough to support RLVR at our budget: across the held\-out test set with each record’s canonical witness fed through the oracle, the median wall\-clock per call is 132 ms, p95 145 ms, and the maximum 326 ms\. No test record approached the eight\-second sandbox timeout\.

Table 1:Domain\-stratified*allocation*of the strict pool: the 2,389 records whose teacher\-generated canonical witness passes its own verifier at generation time\. Rounding the split targets and one oracle\-gating drop move three records from SFT and test into the RLVR prompt set, so the*final*split sizes are SFT 1,000, test 201, and RLVR1,188\+2,318=3,5061\{,\}188\+2\{,\}318=3\{,\}506; the 2,318 loose records have a working verifier but no oracle\-confirmed canonical witness\. Pipeline total: 4,707 records over 3,485 unique theorems; canonical\-witness positive\-reward rate 0\.98\.#### Theorem\-truth probe\.

We construct an auxiliary set of 347*true*theorems drawn from the same theorem source\. The model is asked to classify whether the provided theorem is true or false\.

## 4Training Setup

We train Qwen3\-4B\([Qwen Team, 2025](https://arxiv.org/html/2610.02444#bib.bib25)\)\(unsloth/Qwen3\-4B\) using Supervised Fine\-Tuning \(SFT\) followed by Group Relative Policy Optimization \(GRPO\)\([Shao et al\., 2024](https://arxiv.org/html/2610.02444#bib.bib14)\)\. SFT is performed over 2–3 epochs with a cosine learning rate schedule \(Appendix[A](https://arxiv.org/html/2610.02444#A1)\)\. For RLVR, we initialise from the SFT adapter and train for 4 epochs \(≈\\approx1,752 steps\) using a KL penalty of0\.020\.02against the SFT reference policy\. During RLVR, we sampleG=4G=4rollouts per prompt using vLLM\([Kwon et al\., 2023](https://arxiv.org/html/2610.02444#bib.bib23)\)to maintain high\-throughput generation\. Both training stages use LoRA\([Hu et al\., 2022](https://arxiv.org/html/2610.02444#bib.bib22)\)\(rank 16, applied to all attention and MLP modules\) and bfloat16 precision\.

Notably, our entire pipeline is highly computationally accessible: training executes on a single NVIDIA RTX 5090 \(32 GB\) consumer GPU, with SFT completing in under five minutes and each RLVR run taking approximately nine hours\. Full hyperparameters, optimizer configurations, and prompt templates are detailed in Appendix[A](https://arxiv.org/html/2610.02444#A1)\.

## 5Experimental Setup

### 5\.1Models

We report four model variants from this work: the unmodifiedQwen3\-4B base,SFTcheckpoint, and two RLVR checkpointsRLVR\-dense\(Eq\.[1](https://arxiv.org/html/2610.02444#S3.E1)dense weights\) andRLVR\-sparse\(sparse weights\)\. For external context we evaluate five open\-weights 7B math\-specialised models, Abel\-7B\-002, DeepSeek\-Math\-7B\-RL, Eurus\-2\-7B\-PRIME, MAmmoTH2\-7B\-Plus and Qwen2\.5\-Math\-7B\-Instruct\([Shao et al\., 2024](https://arxiv.org/html/2610.02444#bib.bib14);[Yang et al\., 2024](https://arxiv.org/html/2610.02444#bib.bib15);[Cui et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib6);[Yue et al\., 2024](https://arxiv.org/html/2610.02444#bib.bib16)\), and six frontier commercial APIs from the DeepSeek and Gemini families\. Per\-model breakdowns of the external comparators are deferred to Appendix[G](https://arxiv.org/html/2610.02444#A7); in the main paper we summarise them as a best\-7B row and a frontier\-API range\. For the cross\-family replication of §[6\.6](https://arxiv.org/html/2610.02444#S6.SS6)we repeat the pipeline on Gemma\-3\-4B\.

### 5\.2Benchmarks

Counterexample \(in\-domain, n=201\)\.Our held\-out test split \(§[3\.3](https://arxiv.org/html/2610.02444#S3.SS3)\), stratified by domain\. The strict scoring criterion isq¬=1∧shyp=nhypq\_\{\\neg\}\{=\}1\\wedge s\_\{\\text\{hyp\}\}\{=\}n\_\{\\text\{hyp\}\}; we also report the relaxedconclusion\-passrateq¬=1q\_\{\\neg\}\{=\}1\.

Theorem\-truth \(n=347\)\.The model is considered correct iff it recognises the theorem as true\. We evaluate two prompt styles:SymCE\-prompt \(the same prompt style as training\) andtruth\-classify\(an explicit true/false question\)\.

A response counts as correct only when the model commits to an answer\. Permissive extraction inflates untrained baselines substantially; Appendix[C](https://arxiv.org/html/2610.02444#A3)reports both readings and validates the rule\.

External math benchmarks\.GSM8K \(n=1319\), MATH\-500 \(n=500\), MMLU\-college\-math \(n=100\), AIME\-2024 \(n=30\)\([Cobbe et al\., 2021](https://arxiv.org/html/2610.02444#bib.bib17);[Hendrycks et al\., 2021b](https://arxiv.org/html/2610.02444#bib.bib18);[Hendrycks et al\., 2021a](https://arxiv.org/html/2610.02444#bib.bib19)\)\. All four models useidenticalprompting \(standard chain\-of\-thought\); our SFT and RLVR splits containnoexamples from these benchmarks and no training on their answer\-extraction formats\.

### 5\.3Decoding and metrics

We evaluate under two decoding regimes:greedy\(temperature 0,n=1n\{=\}1\) andsampled\(temperature 0\.7, top\-pp1\.0,n=8n\{=\}8\)\. Pass@kkfork∈\{1,3,5,8\}k\\in\\\{1,3,5,8\\\}is computed with the unbiased estimator of[Chen et al\. \(2021\)](https://arxiv.org/html/2610.02444#bib.bib20); greedy Pass@1 is reported as the headline number throughout\. 95 % confidence intervals are percentile bootstrap intervals over problem ids with 10,000 resamples \(the unbiased Pass@kkestimator is applied per problembeforeresampling\)\. Paired deltas \(model A minus model B\) bootstrap over the per\-problem Pass@kkdifferences\. All scripts are released\.

## 6Results

### 6\.1Counterexample generation

Table 2:In\-domain counterexample benchmark \(n=201\), reference seed 42\. Greedy Pass@1 is the headline metric; 95 % bootstrap CIs in brackets\.Conclusion\-passis the relaxed criterionq¬=1q\_\{\\neg\}\{=\}1of §[5\.2](https://arxiv.org/html/2610.02444#S5.SS2)\. Four\-seed means for the trained variants are in Table[5](https://arxiv.org/html/2610.02444#S6.T5)\.aRange across six DeepSeek/Gemini frontier APIs\. The full per\-model open\-weights table is in Appendix[G](https://arxiv.org/html/2610.02444#A7)\.Table[2](https://arxiv.org/html/2610.02444#S6.T2)summarises the main result on the reference seed\. Counterexample\-only SFT lifts greedy Pass@1 modestly above the Qwen3\-4B base \(0\.30→\\to0\.35; 95 % CI on the paired delta\[−0\.030,\+0\.119\]\[\-0\.030,\+0\.119\]\), entirely consistent with no statistically significant gain at this sample size\. Continuing with verifier\-grounded RL, regardless of reward shape, yields a substantial further gain to 0\.50 \[0\.43, 0\.57\] \(paired delta versus the base\+0\.199\+0\.199\[\+0\.13, \+0\.27\]\)\. Across four seeds the RLVR variants reach 0\.49±\\pm0\.02 \(dense\) and 0\.46±\\pm0\.03 \(sparse\) against an unchanged base of 0\.30 \(Table[5](https://arxiv.org/html/2610.02444#S6.T5)\)\.

Three points are worth emphasising\. First, our 4B RLVR model exceeds every 7B math\-specialist open\-weights model we evaluated \(full table in Appendix[G](https://arxiv.org/html/2610.02444#A7)\); the best 7B baseline \(Eurus\-2\-7B\-PRIME at 0\.30\) is statistically indistinguishable from our untrained 4B base \(paired CI\[−0\.075,\+0\.065\]\[\-0\.075,\+0\.065\]\), which isolates the gain to the training method rather than parameter count, and is consistent with the forward/falsification asymmetry reported by[Sinha et al\. \(2025\)](https://arxiv.org/html/2610.02444#bib.bib2)\. Second, the gain holds in expectation under sampled decoding: RLVR Pass@8 is 0\.68, versus 0\.57 for the best 7B baseline and 0\.49 for the base\. Third, our 4B RLVR model falls inside the range of greedy Pass@1 measured for six commercial frontier APIs \(0\.42–0\.58\); only one of the six APIs outperforms it\. This supports the claim that a 4B model can be made competitive with frontier APIs on this task by training rather than by scale\. RLVR also roughly doubles the rate at which the policy negates the conclusion \(0\.30→\\to0\.61\); the 0\.11 that separates this from Pass@1 is rollouts that negate the conclusion but violate a remaining hypothesis\.

### 6\.2The imitation trap

Table 3:Theorem\-truth probe \(n=347\), reference seed 42\. Pass@1 \(greedy\) = fraction of*true*theorems correctly recognised as true, under the answer\-extraction rules of §[5\.2](https://arxiv.org/html/2610.02444#S5.SS2)\. Four\-seed means are in Table[5](https://arxiv.org/html/2610.02444#S6.T5)\. The base column is conservative: on 62 % of items the base states no verdict at all, exhausting the token budget mid\-reasoning, and it assertsFALSEon only 2\.6 %\. SFT reverses this, assertingFALSEfor 70 % of*true*theorems\. Four\-seed spread for both columns is in Table[5](https://arxiv.org/html/2610.02444#S6.T5)\.A true theorem from the theorem\-truth probe\.*Continuous convergence theorem*\(Real Analysis\): if a sequence of continuous functions satisfies the required convergence assumptions, the limit function is continuous\.SFT output\.Counterexample:X=\[0,1\]X=\[0,1\],fn​\(x\)=xnf\_\{n\}\(x\)=x^\{n\}, andf⁡\(x\)=\{0x<1,1x=1\.f\(x\)=\\begin\{cases\}0&x<1,\\\\ 1&x=1\.\\end\{cases\}The theorem is true\. SFT proposes the classical sequencefn​\(x\)=xnf\_\{n\}\(x\)=x^\{n\}anyway, a construction that violates the convergence assumption it would need\. RLVR\-dense abstains; RLVR\-sparse recognises the theorem as true and emitsNONE\.

Figure 1:The imitation trap on one item\. Appendix[F](https://arxiv.org/html/2610.02444#A6)gives the symmetric sparse\-reward failure: a false conjecture the dense model disproves and the sparse model wrongly abstains on\.Table[3](https://arxiv.org/html/2610.02444#S6.T3)presents what we view as the central scientific finding of this work\. Counterexample\-only SFT collapses the model’s ability to recognise true theorems\. Under the counterexample\-emit prompt format used throughout training, Pass@1 drops from 0\.27 \(base\) to 0\.00 \(SFT\) on all true theorems, in every seed we ran\. The collapse is also visible under an explicit true/false classification prompt \(0\.36→\\to0\.21\), and there it takes a particularly stark form: where the base model mostly declines to commit, the supervised\-only model actively asserts that 70 % of true theorems are false\. The base model retains genuine calibration; the supervised\-only model does not\. Figure[1](https://arxiv.org/html/2610.02444#S6.F1)shows one such item\.

Continuing from the same SFT adapter, verifier\-grounded RL with asparseoutcome\-only reward repairs and exceeds the base under both prompt styles \(0\.65 and 0\.84 respectively\)\. The dense reward also repairs the more demandingSymCE\-prompt probe, but only to just above the base \(0\.34 against 0\.27\), where sparse reaches 0\.65\. The dense and sparse variants are statistically indistinguishable on the in\-distribution counterexample benchmark of §[6\.1](https://arxiv.org/html/2610.02444#S6.SS1)\(Table[2](https://arxiv.org/html/2610.02444#S6.T2)\) but differ by 31 percentage points on this probe on the reference seed, and by 33±\\pm8 points across four seeds\. Appendix[E](https://arxiv.org/html/2610.02444#A5)shows the dissociation is larger still on the subset of true theorems whose mutations were never seen in training, so it is not a memorisation artefact\.

This dissociation, equal in\-distribution Pass@1 with a large out\-of\-distribution gap, is interpretable as evidence that the two reward shapes induce qualitatively different policies despite producing the same counterexample\-generation performance\. We give the mechanism in §[6\.3](https://arxiv.org/html/2610.02444#S6.SS3)\.

### 6\.3Why it happens: a reason\-taxonomy analysis

Figure 2:Per\-sample outcome distribution on the counterexample benchmark \(greedy, n=201\)\. The oracle assigns each rollout exactly one outcome:*success*\(q¬=1q\_\{\\neg\}\{=\}1and all hypotheses satisfied\),*¬\\negQ only*\(q¬=1q\_\{\\neg\}\{=\}1but not all hypotheses\),*abstain*\(theNONEsentinel on a false conjecture\),*hyp\-only*\(all hypotheses satisfied butq¬=0q\_\{\\neg\}\{=\}0, so the policy asserts the false conjecture is true\),*partial*,*parse error*and*no tag*\. The released records carry these as the codessuccess,neg\_q\_only,none\_on\_false,hyp\_only,partial,oracle\_parse\_errorandno\_tag\.We exploit the structured reward to label every test rollout with one of seven mutually exclusiveoutcomes\(Figure[2](https://arxiv.org/html/2610.02444#S6.F2)\)\. Three observations explain the imitation trap\.

SFT trades format errors for logical errors\.The base model rarely emits the trained format at all: 55 % of its rollouts carry no tag\. SFT solves this, but the corresponding mass does not move uniformly into success; instead, the hyp\-only category, in which the policy satisfies the remaining hypotheses but asserts the false conclusion is true, rises from 1 % to 31 %\. The supervised\-only model learned the*form*of a counterexample without learning the calibration: it confidently emits objects that fail the negated\-conclusion check\.

Sparse RL re\-learns abstention\.The abstention rate is 0 % under SFT, 2 % under dense RL, and 10 % under sparse RL\. The sparse reward yields equal score for emitting a wrong witness and emittingNONE, so any rollout the policy is uncertain about is funnelled into abstention; under the dense reward, the partial\-credit termα⋅\(shyp/nhyp\)\\alpha\\cdot\(s\_\{\\text\{hyp\}\}/n\_\{\\text\{hyp\}\}\)makes “try and partially succeed” strictly better than “abstain”\. This is the causal mechanism for the 31\-percentage\-point gap of Table[3](https://arxiv.org/html/2610.02444#S6.T3)\.

Identical success rates hide diverging failure modes\.While dense and sparse RL achieve nearly identical success fractions \(0\.502 vs 0\.497\), dense rewards push the remaining probability mass into over\-eager hyp\-only errors, whereas sparse rewards push it into abstention\.

We conclude that when a verifier yields a structured boolean tuple, an outcome\-only aggregator preserves calibration better than partial credit\. Rewarding satisfaction of some but not all hypotheses actively trains over\-eager counterexample emission\. The claim is specific to that term rather than to dense rewards in general, and our dense reward is not a strawman: its conclusion weighting \(β=0\.65\>α=0\.25\\beta\{=\}0\.65\>\\alpha\{=\}0\.25\) provably precludes the naive hypothesis\-only dominance failure \(§[3\.4](https://arxiv.org/html/2610.02444#S3.SS4)\), and it was selected after exploring several dense variants\.

### 6\.4Cross\-domain consistency

Figure 3:Per\-domain counterexample Pass@1 \(greedy\) with 95 % bootstrap CIs\. Annotations on top: number of test items per domain\. The largestabsolutegain is on LinearAlgebra \(\+0\.30\); the most striking result is on RealAnalysis, where RLVR\-sparse gains \+0\.23 absolute despite the domain being only 6\.7 % of the RLVR training distribution\.Figure[3](https://arxiv.org/html/2610.02444#S6.F3)stratifies the main result by domain\. Both RLVR variants improve on the base in every domain, with no sign of domain collapse or narrow specialisation\. The largest relative gain is on Real Analysis \(0\.23→\\to0\.46\), despite it being the smallest slice of the RLVR training set at 6\.7 %\. This is the inverse of what an over\-fitting model would do, and is consistent with the policy learning a transferable skill rather than a domain\-conditional shortcut\.

Dense and sparse 95 % CIs overlap in almost every domain, supporting the in\-distribution equivalence of §[6\.1](https://arxiv.org/html/2610.02444#S6.SS1)per\-domain rather than as an aggregation artefact\.

### 6\.5Out\-of\-domain transfer

Table 4:Out\-of\-domain transfer under standard chain\-of\-thought prompting \(greedy, Pass@1\), mean±\\pmsd over all four training seeds\. Identical prompt template across all four models; our SFT/RLVR pipeline contains no examples or answer\-format training from these benchmarks\.Table[4](https://arxiv.org/html/2610.02444#S6.T4)measures transfer to four standard mathematical\-reasoning benchmarks\. Training improves on the base everywhere, with sparse and dense comparable\. All four models are evaluated under identical chain\-of\-thought prompting, and our SFT and RLVR data contain no GSM8K, MATH, MMLU or AIME examples and no training on their answer\-extraction formats, so the improvements are attributable to transfer rather than to format adaptation in the training pipeline\.

Part of the MATH\-500 jump is nonetheless format adaptation: the base scores 0\.13 largely because it does not follow the answer\-extraction template, which SFT installs\. GSM8K isolates the reasoning gain, because there the base already formats answers correctly \(0\.83\), yet RLVR still reaches 0\.88 under the identical prompt while SFT alone does not improve on the base at all \(0\.82±\\pm0\.03\)\. The transfer therefore arrives with the reinforcement stage, not the imitation stage\.

We interpret these results as supporting the broader narrative motivated in the introduction: counterexample\-style supervision is a fundamental component of mathematical reasoning that conventional pre\-training under\-installs, rather than a narrow side\-skill\.

### 6\.6Robustness across seeds and model families

Table 5:Robustness of the headline findings\.SymCEPass@kkis the counterexample benchmark \(n=201\); the two Truth rows are the theorem\-truth probe \(n=347\) under the two prompt styles of §[5\.2](https://arxiv.org/html/2610.02444#S5.SS2)\. Qwen3\-4B seeds are 42, 19, 31 and 64; the base is training\-seed independent\. Bold marks the best value in a row\.Table[5](https://arxiv.org/html/2610.02444#S6.T5)repeats the pipeline with three further seeds and on a second model family; per\-seed values are in Appendix[D](https://arxiv.org/html/2610.02444#A4)\. The imitation trap is not a seed artefact: counterexample\-only SFT scores exactly 0\.00 on theSymCE\-prompt probe in all four Qwen seeds\. The sparse\-over\-dense calibration gap on that probe is positive in every seed, at\+0\.33±0\.08\+0\.33\\pm 0\.08\. In\-domain success stays within noise between the two reward shapes, dense ahead by 0\.02 on average, consistent in sign but far inside the test\-set bootstrap width\. And the phenomenon crosses model families: on Gemma\-3\-4B the collapse is more total still, from 0\.49 to 0\.01 under explicit classification and from 0\.40 to 0\.00 on theSymCE\-prompt probe, with both RLVR variants restoring classification above the base\. It replicates on a second Gemma seed \(24\): the same two probes fall from 0\.49 to 0\.00 and from 0\.40 to 0\.00, and dense RLVR restores classification to 0\.54\.

Ontruth\-classifythe sparse advantage is smaller and less consistent: sparse leads dense by0\.04±0\.150\.04\\pm 0\.15, positive in three seeds and negative in seed 64\. We therefore restrict the sparse\-over\-dense calibration claim to the probe that shares the training prompt style, where it holds in every seed\. Appendix[F](https://arxiv.org/html/2610.02444#A6)gives worked examples of both failure modes\.

## 7Discussion

#### This is not generic catastrophic forgetting\.

A natural reading of §[6\.2](https://arxiv.org/html/2610.02444#S6.SS2)is that counterexample\-only SFT simply induces forgetting, and that standard mitigations such as replay are the appropriate control\. Four properties argue otherwise\. The failure isselective: after SFT, general mathematical competence improves substantially \(MATH\-500 0\.13→\\to0\.55, Table[4](https://arxiv.org/html/2610.02444#S6.T4)\) while true\-theorem recognition falls to 0\.00, which is closer to the hallucination tax\([Ouyang, 2025](https://arxiv.org/html/2610.02444#bib.bib12);[Song et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib13)\)than to forgetting\. The repairexceedsthe baseline \(0\.27→\\to0\.66\), which recovering previously seen behaviour does not predict\. It occurs withzero true theorems in training, purely by changing the reward’s treatment of abstention; a replay baseline would alter that distribution and dissolve the phenomenon, so the controlled comparison is dense versus sparse, which holds data and initialisation fixed and still differs by 33 points\. Finally the mechanism islocalisedto a specific behavioural shift \(§[6\.3](https://arxiv.org/html/2610.02444#S6.SS3)\), and generic forgetting offers no account of why two reward shapes on the same checkpoint should differ at all\.

#### Why sparse generalises better on calibration\.

The mechanism in §[6\.3](https://arxiv.org/html/2610.02444#S6.SS3)is interpretable\. Under the dense reward, the partial\-credit termα⋅\(shyp/nhyp\)\\alpha\\cdot\(s\_\{\\text\{hyp\}\}/n\_\{\\text\{hyp\}\}\)guarantees a positive reward whenever the policy satisfies at least one remaining hypothesis, even when it asserts the \(false\) conclusion is true\. This actively trains the policy toalways emit a counterexample expression: doing so on a false conjecture yields up toα\+γ=0\.35\\alpha\+\\gamma=0\.35and never less thanγ=0\.10\\gamma=0\.10when the witness parses, much better than the−0\.20\-0\.20of abstention\. Sparse rewards remove this incentive: the policy is rewarded only for correctly negating the conclusion, and abstention is no worse than a wrong witness\. The behavioural consequence is the higher abstention rate on the in\-distribution test set \(10 % vs 2 %\) and, crucially, the preservation of abstention as a viable action when the policy is shown atruetheorem at test time\. The dense reward does not preserve this; the partial\-credit term is in tension with calibration\.

We conjecture this generalises to other settings where \(i\) the reward signal already returns a structured boolean tuple, and \(ii\) the failure mode of interest is the policy answering when it should abstain, rather than failing to produce well\-formed output\. Whether this conjecture survives at scale is left to future work\.

#### Deterministic verification beats LLM\-as\-judge where the verification problem is decidable\.

The verifier substrate is reproducible, fast \(median 132 ms\), audited end\-to\-end at 97\.7 % decision accuracy over 177 human\-checked verifier decisions, and immune to judge\-model drift\. We would add that this shifts, rather than removes, the dependence on a language model: an LLM\-as\-judge protocol incurs stochastic error at every evaluation, whereas construction\-time LLM dependence is frozen once and can be audited once, which is what §[3\.5](https://arxiv.org/html/2610.02444#S3.SS5)does\. Its scope is bounded by what is decidable in Python with SymPy/Z3; for the algebraic subdomains in this paper this is sufficient\. Where the verification problem is decidable a deterministic verifier is the stronger choice; LLM\-judging, as used by COUNTERMATH\([Li et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib1)\), remains necessary for domains that fall outside it\.

#### Counterexample reasoning as a fundamental capability\.

The cross\-domain consistency of §[6\.4](https://arxiv.org/html/2610.02444#S6.SS4)and the out\-of\-domain transfer of §[6\.5](https://arxiv.org/html/2610.02444#S6.SS5)together support a stronger reading of the contribution: training on structured falsification improves general mathematical reasoning, not only disproof\. The Real Analysis result \(6\.7 % training share,\+\+0\.23 absolute gain\) and the\+\+52 percentage\-point gain on MATH\-500 under unchanged prompting are the strongest evidence for this reading\. The literature on the “hallucination tax”\([Song et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib13)\)predicts that standard imitation\-only training degrades calibration; the present results suggest that verifier\-grounded RL with an outcome\-only reward avoids that pathology and installs a transferable inverse\-reasoning skill\.

## 8Conclusion

We have presentedSymCE, a deterministic, large\-scale dataset and verification environment for counterexample generation on undergraduate algebra and real analysis, and used it to identify and explain an*imitation trap*: supervised fine\-tuning on counterexample\-only data collapses the policy’s ability to recognise true theorems, and verifier\-grounded reinforcement learning with a sparse outcome\-only reward repairs and exceeds the original calibration where a partial\-credit dense reward does not\. The collapse reproduces in every training seed and on a second model family\. A Qwen3\-4B model trained this way exceeds every 7B open\-weights math specialist we evaluated on the in\-domain benchmark, remains competitive with frontier commercial APIs, and transfers under unchanged prompting to GSM8K, MATH\-500 and MMLU\-college\-math, evidence that counterexample reasoning is a fundamental, under\-installed skill rather than a narrow specialisation\. We release the dataset, the verifier modules, the human\-audit annotations, the witness\-schema generator, and the full evaluation pipeline, and we view extension to topology and higher\-order logic, broader mutation strategies, larger scales and alternative RL algorithms, and integration with a Lean back\-end as the natural next steps\.

## Limitations

#### Scale, parameterisation and RL algorithm\.

Every trained variant here is a 4B model adapted with LoRA and optimised with GRPO, so three axes remain untested: substantially larger scales, full\-parameter fine\-tuning, and alternative RL algorithms\. Full fine\-tuning with GRPO rollouts was not feasible on our compute \(a single RTX 5090, 32 GB\), so we cannot separate properties of the environment from properties of GRPO\. Two observations mitigate the concern that the findings are adapter artefacts: they replicate across four seeds and a second model family under the same adapter configuration, including an exact 0\.00 collapse in all six SFT runs, and the mechanism we identify operates at the level of the optimisation objective rather than the parameterisation\. The scaling question is the most important one we leave open\.

#### Verifier scope\.

Our substrate is Python with SymPy and Z3\. This suffices for the six subdomains we evaluate but not for topology, general higher\-order logic, or claims whose verification reduces to undecidable fragments\. A Lean backend, or continuous\-FOL extensions for metric spaces, is a natural follow\-up\.

#### Audit scope\.

The 177\-decision study of §[3\.5](https://arxiv.org/html/2610.02444#S3.SS5)was annotated by a single author, so we report no inter\-annotator agreement, and 177 decisions bound the pipeline’s error rate only coarsely\. A larger, independently annotated audit would support stronger claims about the full verifier collection\.

#### Mutation strategy and scope of the resource claim\.

We mutate only by dropping a single hypothesis\. This was deliberate: it gives every false conjecture a known, attributable cause of falsity, which is what makes the per\-hypothesis boolean interface and the outcome taxonomy possible\. Conclusion mutation, multi\-hypothesis dropping and AST\-level mutation\([Wu et al\., 2024](https://arxiv.org/html/2610.02444#bib.bib4)\)would enrich the distribution but complicate attribution, and remain unexplored\.SymCEshould accordingly be read as a deterministic falsification environment rather than a benchmark spanning the full space of mathematical fallacies\.

#### No COUNTERMATH cross\-evaluation\.

Cross\-evaluation on COUNTERMATH\([Li et al\., 2025](https://arxiv.org/html/2610.02444#bib.bib1)\)would compare our models against the published frontier on a benchmark with broader domain coverage\. The authors do not release the test labels or evaluation scripts, and predicted outputs must be submitted for LLM\-judged scoring on their side, which diverges from this paper’s focus on open, deterministic verification\. We leave this for future work\.

#### Teacher model dependence\.

The verifiers are generated by a single teacher model \(Gemini 3\.1 Pro\) and the witness schemas by a second \(DeepSeek\)\. Although the audit found no verifier\-logic errors, the pipeline retains a dependence on teacher output quality\. Multi\-model consensus generation, in which several teachers must agree on a verifier before it enters the corpus, is a valuable extension we have not implemented\.

## Ethics and Risk Considerations

The work studies counterexample generation for undergraduate\-level algebraic and real\-analysis theorems, using LLM\-generated Python verifiers and a hypothesis\-dropping mutation pipeline\. The artefacts produced \(SymCE, a dataset of false mathematical conjectures, per\-theorem verifier modules, and a small 4B model specialised for falsifying such conjectures\) do not present obvious dual\-use risks beyond those general to research on LLM mathematical reasoning\. Per\-artefact licences are listed in Appendix[I](https://arxiv.org/html/2610.02444#A9)\. The dataset contains no human\-derived data, no personal information, and no naturally occurring text from which PII could be derived; the trained models are released for research use and are not deployed in any user\-facing setting; and the methodology does not enable capabilities that meaningfully extend beyond existing open\-source mathematical reasoning models\.

## Acknowledgements

We gratefully acknowledgeSukai Labsand its CEO, Ahmed Sedouki, for believing in this research and providing access to the NVIDIA RTX 5090 \(32 GB\) GPU on which all training and evaluation runs in this paper were performed\. We also thank the ACL ARR reviewers and the action editor, whose requests for multi\-seed replication, a second model family, and a stronger verifier audit shaped the evidence reported here\.

## References

- Chenet al\.\(2021\)M\. Chen, J\. Tworek, H\. Jun, Q\. Yuan, H\. P\. de Oliveira Pinto, J\. Kaplan, H\. Edwards, Y\. Burda, N\. Joseph, G\. Brockman, A\. Ray, R\. Puri, G\. Krueger, M\. Petrov, H\. Khlaaf, G\. Sastry, P\. Mishkin, B\. Chan, S\. Gray, N\. Ryder, M\. Pavlov, A\. Power, L\. Kaiser, M\. Bavarian, C\. Winter, P\. Tillet, F\. P\. Such, D\. Cummings, M\. Plappert, F\. Chantzis, E\. Barnes, A\. Herbert\-Voss, W\. H\. Guss, A\. Nichol, A\. Paino, N\. Tezak, J\. Tang, I\. Babuschkin, S\. Balaji, S\. Jain, W\. Saunders, C\. Hesse, A\. N\. Carr, J\. Leike, J\. Achiam, V\. Misra, E\. Morikawa, A\. Radford, M\. Knight, M\. Brundage, M\. Murati, K\. Mayer, P\. Welinder, B\. McGrew, D\. Amodei, S\. McCandlish, I\. Sutskever, and W\. ZarembaEvaluating large language models trained on code\.arXiv preprint arXiv:2107\.03374\.Cited by:[§5\.3](https://arxiv.org/html/2610.02444#S5.SS3.p1.1)\.
- Cobbeet al\.\(2021\)K\. Cobbe, V\. Kosaraju, M\. Bavarian, M\. Chen, H\. Jun, L\. Kaiser, M\. Plappert, J\. Tworek, J\. Hilton, R\. Nakano, C\. Hesse, and J\. SchulmanTraining verifiers to solve math word problems\.arXiv preprint arXiv:2110\.14168\.Cited by:[§5\.2](https://arxiv.org/html/2610.02444#S5.SS2.p4.1)\.
- Cuiet al\.\(2025\)G\. Cui, L\. Yuan, Z\. Wang, H\. Wang, Y\. Zhang, J\. Chen, W\. Li, B\. He, Y\. Fan, T\. Yu, Q\. Xu, W\. Chen, J\. Yuan, H\. Chen, K\. Zhang, X\. Lv, S\. Wang, Y\. Yao, X\. Han, H\. Peng, Y\. Cheng, Z\. Liu, M\. Sun, B\. Zhou, and N\. DingProcess reinforcement through implicit rewards\.arXiv preprint arXiv:2502\.01456\.Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px2.p1.1),[§5\.1](https://arxiv.org/html/2610.02444#S5.SS1.p1.1)\.
- De Moura and Bjørner \(2008\)L\. De Moura and N\. BjørnerZ3: an efficient smt solver\.InTools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008,pp\. 337–340\.Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px3.p1.1)\.
- Guoet al\.\(2025\)D\. Guo, D\. Yang, H\. Zhang, J\. Song, P\. Wang, Q\. Zhu, R\. Xu, R\. Zhang, S\. Ma, X\. Bi, X\. Zhang, X\. Yu, Y\. Wu, Z\. F\. Wu, Z\. Gou, Z\. Shao, Z\. Li, Z\. Gao, A\. Liu, B\. Xue, B\. Wang, B\. Wu, B\. Feng, C\. Lu, C\. Zhao, C\. Deng, C\. Ruan, D\. Dai, D\. Chen, D\. Ji, E\. Li, F\. Lin, F\. Dai, F\. Luo, G\. Hao, G\. Chen, G\. Li, H\. Zhang, H\. Xu, H\. Ding, H\. Gao, H\. Qu, H\. Li, J\. Guo, J\. Li, J\. Chen, J\. Yuan, J\. Tu, J\. Qiu, J\. Li, J\. L\. Cai, J\. Ni, J\. Liang, J\. Chen, K\. Dong, K\. Hu, K\. You, K\. Gao, K\. Guan, K\. Huang, K\. Yu, L\. Wang, L\. Zhang, L\. Zhao, L\. Wang, L\. Zhang, L\. Xu, L\. Xia, M\. Zhang, M\. Zhang, M\. Tang, M\. Zhou, M\. Li, M\. Wang, M\. Li, N\. Tian, P\. Huang, P\. Zhang, Q\. Wang, Q\. Chen, Q\. Du, R\. Ge, R\. Zhang, R\. Pan, R\. Wang, R\. J\. Chen, R\. L\. Jin, R\. Chen, S\. Lu, S\. Zhou, S\. Chen, S\. Ye, S\. Wang, S\. Yu, S\. Zhou, S\. Pan, S\. S\. Li, S\. Zhou, S\. Wu, T\. Yun, T\. Pei, T\. Sun, T\. Wang, W\. Zeng, W\. Liu, W\. Liang, W\. Gao, W\. Yu, W\. Zhang, W\. L\. Xiao, W\. An, X\. Liu, X\. Wang, X\. Chen, X\. Nie, X\. Cheng, X\. Liu, X\. Xie, X\. Liu, X\. Yang, X\. Li, X\. Su, X\. Lin, X\. Q\. Li, X\. Jin, X\. Shen, X\. Chen, X\. Sun, X\. Wang, X\. Song, X\. Zhou, X\. Wang, X\. Shan, Y\. K\. Li, Y\. Q\. Wang, Y\. X\. Wei, Y\. Zhang, Y\. Xu, Y\. Li, Y\. Zhao, Y\. Sun, Y\. Wang, Y\. Yu, Y\. Zhang, Y\. Shi, Y\. Xiong, Y\. He, Y\. Piao, Y\. Wang, Y\. Tan, Y\. Ma, Y\. Liu, Y\. Guo, Y\. Ou, Y\. Wang, Y\. Gong, Y\. Zou, Y\. He, Y\. Xiong, Y\. Luo, Y\. You, Y\. Liu, Y\. Zhou, Y\. X\. Zhu, Y\. Huang, Y\. Li, Y\. Zheng, Y\. Zhu, Y\. Ma, Y\. Tang, Y\. Zha, Y\. Yan, Z\. Z\. Ren, Z\. Ren, Z\. Sha, Z\. Fu, Z\. Xu, Z\. Xie, Z\. Zhang, Z\. Hao, Z\. Ma, Z\. Yan, Z\. Wu, Z\. Gu, Z\. Zhu, Z\. Liu, Z\. Li, Z\. Xie, Z\. Song, Z\. Pan, Z\. Huang, Z\. Xu, Z\. Zhang, and Z\. ZhangDeepSeek\-r1 incentivizes reasoning in llms through reinforcement learning\.Nature645\(8081\),pp\. 633–638\.External Links:[Document](https://dx.doi.org/10.1038/s41586-025-09422-z),ISSN 1476\-4687,[Link](https://doi.org/10.1038/s41586-025-09422-z)Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px2.p1.1)\.
- Hendryckset al\.\(2021a\)D\. Hendrycks, C\. Burns, S\. Basart, A\. Zou, M\. Mazeika, D\. Song, and J\. SteinhardtMeasuring massive multitask language understanding\.InInternational Conference on Learning Representations,Cited by:[§5\.2](https://arxiv.org/html/2610.02444#S5.SS2.p4.1)\.
- Hendryckset al\.\(2021b\)D\. Hendrycks, C\. Burns, S\. Kadavath, A\. Arora, S\. Basart, E\. Tang, D\. Song, and J\. SteinhardtMeasuring mathematical problem solving with the math dataset\.NeurIPS\.Cited by:[§5\.2](https://arxiv.org/html/2610.02444#S5.SS2.p4.1)\.
- Huet al\.\(2022\)E\. J\. Hu, Y\. Shen, P\. Wallis, Z\. Allen\-Zhu, Y\. Li, S\. Wang, L\. Wang, and W\. ChenLoRA: low\-rank adaptation of large language models\.InInternational Conference on Learning Representations,Cited by:[§4](https://arxiv.org/html/2610.02444#S4.p1.1)\.
- Kamoiet al\.\(2026\)R\. Kamoi, Y\. Zhang, N\. Zhang, S\. S\. S\. Das, R\. H\. Zhang, W\. Yin, and R\. ZhangEfficient prm training data synthesis via formal verification\.InFindings of the Association for Computational Linguistics: ACL 2026,Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px3.p1.1)\.
- Kwonet al\.\(2023\)W\. Kwon, Z\. Li, S\. Zhuang, Y\. Sheng, L\. Zheng, C\. H\. Yu, J\. E\. Gonzalez, H\. Zhang, and I\. StoicaEfficient memory management for large language model serving with PagedAttention\.InProceedings of the 29th Symposium on Operating Systems Principles,Cited by:[§4](https://arxiv.org/html/2610.02444#S4.p1.1)\.
- Liet al\.\(2025\)Y\. Li, J\. Kuang, H\. Huang, Z\. Xu, X\. Liang, Y\. Yu, W\. Lu, Y\. Li, X\. Tan, C\. Qu, Y\. Shen, H\. Zheng, and P\. S\. YuOne example shown, many concepts known\!: counterexample\-driven conceptual reasoning in mathematical llms\.InProceedings of the 42nd International Conference on Machine Learning,ICML’25\.Cited by:[§1](https://arxiv.org/html/2610.02444#S1.p1.1),[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px1.p1.1),[§3\.1](https://arxiv.org/html/2610.02444#S3.SS1.p3.1),[§7](https://arxiv.org/html/2610.02444#S7.SS0.SSS0.Px3.p1.1),[No COUNTERMATH cross\-evaluation\.](https://arxiv.org/html/2610.02444#Sx1.SS0.SSS0.Px5.p1.1)\.
- Liet al\.\(2026\)Z\. Li, Z\. Li, K\. Yang, X\. Ma, and Z\. SuLearning to disprove: formal counterexample generation with large language models\.arXiv preprint arXiv:2603\.19514\.Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px1.p1.1),[§3\.1](https://arxiv.org/html/2610.02444#S3.SS1.p3.1),[§3\.4](https://arxiv.org/html/2610.02444#S3.SS4.SSS0.Px2.p1.2)\.
- Lightmanet al\.\(2024\)H\. Lightman, V\. Kosaraju, Y\. Burda, H\. Edwards, B\. Baker, T\. Lee, J\. Leike, J\. Schulman, I\. Sutskever, and K\. CobbeLet’s verify step by step\.InInternational Conference on Learning Representations,Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px3.p1.1)\.
- Meureret al\.\(2017\)A\. Meurer, C\. P\. Smith, M\. Paprocki, O\. Čertík, S\. B\. Kirpichev, M\. Rocklin, A\. Kumar, S\. Ivanov, J\. K\. Moore, S\. Singh, T\. Rathnayake, S\. Vig, B\. E\. Granger, R\. P\. Muller, F\. Bonazzi, H\. Gupta, S\. Vats, F\. Johansson, F\. Pedregosa, M\. J\. Curry, A\. R\. Terrel, Š\. Roučka, A\. Saboo, I\. Fernando, S\. Kulal, R\. Cimrman, and A\. ScopatzSymPy: symbolic computing in python\.PeerJ Computer Science3,pp\. e103\.External Links:ISSN 2376\-5992,[Link](https://doi.org/10.7717/peerj-cs.103),[Document](https://dx.doi.org/10.7717/peerj-cs.103)Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px3.p1.1)\.
- Ouyang \(2025\)J\. OuyangTreeCut: a synthetic unanswerable math word problem dataset for llm hallucination evaluation\.arXiv preprint arXiv:2502\.13442\.Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px4.p1.1),[§7](https://arxiv.org/html/2610.02444#S7.SS0.SSS0.Px1.p1.1)\.
- Qwen Team \(2025\)Qwen TeamQwen3 technical report\.External Links:2505\.09388Cited by:[§1](https://arxiv.org/html/2610.02444#S1.p4.1),[§4](https://arxiv.org/html/2610.02444#S4.p1.1)\.
- Shaoet al\.\(2025\)R\. Shao, S\. Li, R\. Xin, S\. Geng, Y\. Wang, S\. Oh, S\. Du, N\. Lambert, S\. Min, R\. Krishna, Y\. Tsvetkov, H\. Hajishirzi, P\. Koh, and L\. ZettlemoyerSpurious rewards: rethinking training signals in rlvr\.External Links:2506\.10947,[Document](https://dx.doi.org/10.48550/arXiv.2506.10947)Cited by:[§1](https://arxiv.org/html/2610.02444#S1.p1.1),[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px2.p1.1)\.
- Shaoet al\.\(2024\)Z\. Shao, P\. Wang, Q\. Zhu, R\. Xu, J\. Song, X\. Bi, H\. Zhang, M\. Zhang, Y\. K\. Li, Y\. Wu, and D\. GuoDeepSeekMath: pushing the limits of mathematical reasoning in open language models\.arXiv preprint arXiv:2402\.03300\.Cited by:[§4](https://arxiv.org/html/2610.02444#S4.p1.1),[§5\.1](https://arxiv.org/html/2610.02444#S5.SS1.p1.1)\.
- Sinhaet al\.\(2025\)S\. Sinha, S\. Goel, P\. Kumaraguru, J\. Geiping, M\. Bethge, and A\. PrabhuCan language models falsify? evaluating algorithmic reasoning with counterexample creation\.External Links:2502\.19414,[Link](https://arxiv.org/abs/2502.19414)Cited by:[§1](https://arxiv.org/html/2610.02444#S1.p1.1),[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px1.p1.1),[§6\.1](https://arxiv.org/html/2610.02444#S6.SS1.p2.1)\.
- Songet al\.\(2025\)L\. Song, T\. Shi, and J\. ZhaoThe hallucination tax of reinforcement finetuning\.arXiv preprint arXiv:2505\.13988\.Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px4.p1.1),[§7](https://arxiv.org/html/2610.02444#S7.SS0.SSS0.Px1.p1.1),[§7](https://arxiv.org/html/2610.02444#S7.SS0.SSS0.Px4.p1.1)\.
- Wanget al\.\(2023\)P\. Wang, L\. Li, Z\. Shao, R\. X\. Xu, D\. Dai, Y\. Li, D\. Chen, Y\. Wu, and Z\. SuiMath\-shepherd: verify and reinforce llms step\-by\-step in mathematical reasoning\.arXiv preprint arXiv:2312\.08935\.Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px3.p1.1)\.
- Wuet al\.\(2024\)S\. Wu, S\. Lu, Y\. Gong, N\. Duan, and P\. WeiAlchemy: amplifying theorem\-proving capability through symbolic mutation\.arXiv preprint arXiv:2410\.15748\.Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px1.p1.1),[Mutation strategy and scope of the resource claim\.](https://arxiv.org/html/2610.02444#Sx1.SS0.SSS0.Px4.p1.1)\.
- Xionget al\.\(2025\)W\. Xiong, H\. Zhang, C\. Ye, L\. Chen, N\. Jiang, and T\. ZhangSelf\-rewarding correction for mathematical reasoning\.External Links:2502\.19613,[Link](https://arxiv.org/abs/2502.19613)Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px3.p1.1)\.
- Yanget al\.\(2024\)A\. Yang, B\. Zhang, B\. Hui, B\. Gao, B\. Yu, C\. Li, D\. Liu, J\. Tu, J\. Zhou, J\. Lin, K\. Lu, M\. Xue, R\. Lin, T\. Liu, X\. Ren, and Z\. ZhangQwen2\.5\-math technical report: toward mathematical expert model via self\-improvement\.arXiv preprint arXiv:2409\.12122\.Cited by:[§5\.1](https://arxiv.org/html/2610.02444#S5.SS1.p1.1)\.
- Yaoet al\.\(2026\)J\. Yao, R\. Wang, H\. Bai, and T\. ZhangFuture\-kl regularized grpo: process\-level credit assignment fromff\-divergence regularization\.External Links:2601\.10201,[Link](https://arxiv.org/abs/2601.10201)Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px3.p1.1)\.
- Yuanet al\.\(2024\)L\. Yuan, G\. Cui, H\. Wang, N\. Ding, X\. Wang, J\. Deng, B\. Shan, H\. Chen, R\. Xie, Y\. Lin, Z\. Liu, B\. Zhou, H\. Peng, Z\. Liu, and M\. SunAdvancing llm reasoning generalists with preference trees\.External Links:2404\.02078,[Link](https://arxiv.org/abs/2404.02078)Cited by:[§2](https://arxiv.org/html/2610.02444#S2.SS0.SSS0.Px2.p1.1)\.
- Yueet al\.\(2024\)X\. Yue, T\. Zheng, G\. Zhang, and W\. ChenMAmmoTH2: scaling instructions from the web\.arXiv preprint arXiv:2405\.03548\.Cited by:[§5\.1](https://arxiv.org/html/2610.02444#S5.SS1.p1.1)\.

## Appendix AFull Hyperparameters

Table[6](https://arxiv.org/html/2610.02444#A1.T6)lists the exact hyperparameters used for the SFT and RLVR runs reported in this paper\. The reference\-seed runs were launched fromconfigs/full\_run\.yaml\(SFT\),configs/full\_run\_dense\_test\.yaml\(dense RLVR\) andconfigs/full\_run\_sparse\.yaml\(sparse RLVR\); the additional seeds are inconfigs/seeds/\. Each run directory also carries the fully resolvedconfig\.jsonit was launched with, which is the authoritative record\.

Figure 4:Per\-step training curves for the dense and sparse RLVR runs at the reference seed \(≈\\approx1,752 steps over four epochs of 3,506 prompts\)\. Mean reward rises monotonically and crosses zero by step∼\\sim240 for both variants; KL to the SFT reference decays smoothly; loss is bounded and oscillatory but stable\.Figure[4](https://arxiv.org/html/2610.02444#A1.F4)shows the per\-step training curves for both RLVR runs\. The reward trajectory rises from approximately−0\.20\-0\.20at step 80 to\+0\.40\+0\.40\(dense\) /\+0\.30\+0\.30\(sparse\) at convergence; the KL penalty to the SFT reference declines from∼2\.0\\sim 2\.0to∼0\.5\\sim 0\.5as the policy explores away from imitation; the policy loss is bounded and oscillatory but does not diverge\. Both runs complete the full four epochs without any restart, gradient explosion or reward collapse\.

Table 6:Hyperparameters used for SFT and both RLVR variants, as recorded by the reference\-seed runs\. The one setting that is not uniform is the SFT epoch count: seed 42 uses 3 epochs, and seeds 19, 31 and 64 use 2, after we checked that the two schedules performed equivalently and preferred the shorter one\. SFT wall\-clock on a single RTX 5090 32 GB is under five minutes; each RLVR run is approximately nine hours\.
## Appendix BHuman Audit of Verifier Decisions

We sampled 177 model\-generated witnesses from the held\-out test split, drawn across four seeds and three training configurations \(dense 85, sparse 61, SFT 31\) and all six subdomains, and split by the verifier’s own verdict: 101 that it accepted and 76 that it rejected\. An author with graduate\-level training in the relevant areas judged, independently of the verifier, whether each witness is genuinely a valid counterexample\. Table[7](https://arxiv.org/html/2610.02444#A2.T7)reports the composition\.

Table 7:Composition of the human audit, split by the verifier’s verdict\. Decision accuracy: 99/101 accepted witnesses confirmed valid, 74/76 rejected witnesses confirmed invalid, 173/177 = 97\.7 % overall\. Annotations are released athuman\_eval/\.#### The four disputed decisions\.

Two verifier acceptances were judged invalid: one witness satisfied the remaining hypotheses without actually negating the conclusion, and one supplied a malformed field construction\. Two rejections were judged wrong, and in neither case is the verifier module at fault\. Inbw\_seq\_rn\_\_h3the emitted witness was valid but the witness\-schema description showed a bareMatrixwhere the verifier’s namespace requiressympy\.Matrix; the fault is in the schema text, not the verifier logic\. Inword\_problem\_direct\_productthe conjecture remained true after the hypothesis drop, and the model correctly emittedNONE; the verifier “rejected” only because a counterexample was expected where none exists\. This is the single case in 177 that we attribute to hypothesis\-drop label noise, and the single case attributable to schema quality\.

Among the confirmed\-correct rejections the annotator noted several where the mathematics was right and only the Python namespace or API usage was wrong, such asMatrixforsympy\.Matrix; only 9 of the 76 rejections carry free\-text annotations, so we cannot estimate a rate\.

## Appendix CAnswer Extraction and the Scoring Correction

§[5\.2](https://arxiv.org/html/2610.02444#S5.SS2)adopts strict answer\-extraction rules for the two calibration probes\. This appendix reports both readings so the effect is auditable\.

The evaluation harness that produced our raw records used, as a last resort when no answer frame was present, a parser matching any bare occurrence of*true*or*false*anywhere in the completion, taking the last one\. On completions that exhaust the generation budget mid\-reasoning this converts unfinished chains of thought into apparent verdicts\. The effect is confined almost entirely to the untrained base model, which reasons at length and frequently fails to commit within budget; the trained models emit the required format and are barely affected\.

Table 8:Theorem\-truth probe under both answer\-extraction rules \(reference seed 42, n=347\)\. “Permissive” reproduces what the original evaluation harness recorded; the paper reports the strict column throughout\.Two properties of the finding are invariant to the choice\. Counterexample\-only SFT scores exactly 0\.00 on theSymCE\-prompt probe under both rules and in every seed, and the sparse\-over\-dense gap on that probe is 0\.31 under both\. What the choice does affect is the base model’s apparent calibration, and hence whether RLVR is described as exceeding it\.

We validated that the stricttruth\-classifyrule does not under\-credit models that do answer\. Across every cell in our corpus, each response the rule records as stating no verdict is an unfinished completion; no completion that terminated normally is scored as having failed to answer\. The accepted answer frames were derived by inspecting the completions that the narrowAnswer: TRUEpattern alone would have missed, and cover the phrasings both model families actually produce, including\\boxed\{TRUE\}and “the claim isTRUE”\.

## Appendix DPer\-Seed Results

Table[9](https://arxiv.org/html/2610.02444#A4.T9)gives the individual seed values behind the means of Table[5](https://arxiv.org/html/2610.02444#S6.T5)\. The base model is training\-seed independent and is evaluated once per suite\.

Table 9:Per\-seed values\. The sparse\-over\-dense gap on theSymCE\-prompt probe is positive in every seed \(\+0\.31\+0\.31,\+0\.42\+0\.42,\+0\.35\+0\.35,\+0\.22\+0\.22\); ontruth\-classifyit is not \(\+0\.11\+0\.11,\+0\.01\+0\.01,\+0\.19\+0\.19,−0\.15\-0\.15\), which is why §[6\.6](https://arxiv.org/html/2610.02444#S6.SS6)restricts the claim to theSymCE\-prompt probe\.
## Appendix ETheorem\-Truth Robustness: Seen vs Unseen Subsets

The 347\-item theorem\-truth probe partitions into true theorems whose*mutated*form appeared in the RLVR training corpus \(extra\_stratified, n=150\) and those whose mutated form did not \(from\_test\_set, n=197\)\. Because both subsets are drawn from the same theorem source, comparing them bounds how much of the trained models’ calibration is memorisation\.

Table 10:SymCE\-prompt Pass@1 by subset \(greedy, strict scoring, reference seed 42\)\.Δ\\Delta= seen−\-unseen\.Two readings\. The base model shows a small positiveΔ\\Delta\(\+0\.06\+0\.06\), which sets the scale of any residual difficulty difference between the subsets rather than of memorisation, since the base saw neither\. The trained models show larger gaps \(\+0\.09\+0\.09to\+0\.16\+0\.16\), consistent with some memorisation of theorem identity\. Crucially, the sparse\-over\-dense gap on the*unseen*subset alone is0\.614−0\.274=\+0\.340\.614\-0\.274=\+0\.34, larger than on the full probe, so the central dissociation of this paper is not a memorisation artefact\.

## Appendix FQualitative Examples

Figure[1](https://arxiv.org/html/2610.02444#S6.F1)shows the imitation trap on a true theorem: the SFT model emits a syntactically valid, well\-formatted counterexample expression that none the less fails the negated\-conclusion check, which is a hyp\-only failure in the taxonomy of §[6\.3](https://arxiv.org/html/2610.02444#S6.SS3)\. Figure[5](https://arxiv.org/html/2610.02444#A6.F5)below shows the symmetric failure mode of the sparse reward\.

A false conjecture from the counterexample benchmark\.*Minimal polynomial ofa\+b\\sqrt\{a\}\+\\sqrt\{b\}*\(Field Theory\): the original theorem requires thataa,bbanda​babare all non\-squares in the base field\. The benchmark removes the assumption thataais not a square\.RLVR\-dense witness\.\(F,a,b\)=\(ℚ,1,2\)\(F,a,b\)=\(\\mathbb\{Q\},1,2\)\. Since11is a square inℚ\\mathbb\{Q\}, the claimed quartic is no longer the minimal polynomial of1\+21\+\\sqrt\{2\}:x2−2​x−1≠x4−6​x2\+1\.x^\{2\}\-2x\-1\\;\\neq\\;x^\{4\}\-6x^\{2\}\+1\.RLVR\-dense finds this compact counterexample; RLVR\-sparse abstains and emitsNONE\.

Figure 5:A sparse\-reward failure: improved calibration on true theorems costs false abstentions on genuinely false conjectures\. We discuss the trade\-off in §[7](https://arxiv.org/html/2610.02444#S7)\.
## Appendix GPer\-Model Baseline Breakdowns

Table[11](https://arxiv.org/html/2610.02444#A7.T11)reports the per\-model counterexample\-benchmark scores for the five 7B open\-weights math specialists summarised in the body\. Table[12](https://arxiv.org/html/2610.02444#A7.T12)reports the same for the six commercial\-API frontier models that contribute to the “frontier API range” band in Table[2](https://arxiv.org/html/2610.02444#S6.T2)\. We additionally report the Qwen2\.5\-Math\-1\.5B base in Table[11](https://arxiv.org/html/2610.02444#A7.T11)as a smaller comparison point\. Figure[6](https://arxiv.org/html/2610.02444#A7.F6)shows all comparators together\.

Table 11:Open\-weights baselines on the counterexample benchmark \(n=201\)\. All numbers Pass@kkwith 95 % bootstrap CIs over problem ids\. Sampled decoding usesn=8n=8, temperature 0\.7\. Regenerated bybuild\_camera\_ready\_tables\.py\.Table 12:Frontier commercial APIs on the counterexample benchmark \(n=201\)\. Dashes indicate sampled passes that were not run because token\-budget constraints prevented an 8\-sample run within the budget\. Regenerated bybuild\_camera\_ready\_tables\.py\.Figure 6:Counterexample Pass@1 \(greedy\) for all comparators evaluated\. Our trained 4B models are in colour; open\-weights 7B specialists are in grey; the shaded yellow band shows the range across six frontier commercial APIs\.
## Appendix HWitness\-Schema Generator and Example Schemas

The witness\-schema stage \(§[3\.2](https://arxiv.org/html/2610.02444#S3.SS2)\) is implemented intools/inject\_witness\_schema\.py\. The tool iterates over verifier modules and queries a teacher model \(DeepSeek via the OpenAI\-compatible API client\) with the verifier source code and the canonical witness expression, asking for a single\-sentence Python\-shape description of an acceptable witness, with a concrete example\.

#### Representative schemas \(one per subdomain\)\.

> GroupTheory\.“Python tuple\(G,H\)\(G,H\)where bothGGandHHaresympy\.combinatorics\.PermutationGroupobjects constructed via SymPy group constructors \(e\.g\.,SymmetricGroup\(n\),AlternatingGroup\(n\),DihedralGroup\(n\),CyclicGroup\(n\)\)\. Example syntax:\(SymmetricGroup\(3\), DihedralGroup\(4\)\)\.” RingTheory\.“AnRModuleinstance with attributes:ring\(CommutativeRing\) andgenerators\_count\(int\)\. Example:RModule\(Z, 2\)\.” FieldTheory\.“A SymPyDomainobject representing an integral domain that is not a field\. Example:ZZfrom SymPy\.” LinearAlgebra\.“A SymPyMatrixobject \(square, non\-real\)\. Example:Matrix\(\[\[0, 1\], \[\-1, 0\]\]\)\.” RealAnalysis\.“Python tuple\(f,a,b,p\)\(f,a,b,p\)whereffis a SymPy expression \(or string\) in terms ofSymbol\(’x’\),aaandbbare real numbers\(a<b\)\(a<b\),ppis a real number\.” NumberTheory\.“A Python int orsympy\.Integer\(single integer\)\. Example:5\.”

The schemas are short \(10–40 tokens\) and add a small overhead to the user prompt \(median schema length is well below the SFT user\-prompt median of 120 tokens reported in the dataset stats\)\.

## Appendix IArtefact Licences

All third\-party artefacts are used for non\-commercial research consistent with their release terms\. Models: Qwen3\-4B and Qwen2\.5\-Math \(Apache 2\.0\), Gemma\-3\-4B \(Gemma Terms of Use\), DeepSeek\-Math\-7B\-RL \(DeepSeek Licence\), Eurus\-2\-7B\-PRIME, MAmmoTH2\-7B\-Plus and Abel\-7B\-002 \(Apache 2\.0\)\. Libraries: vLLM, TRL, PEFT/LoRA, SymPy and Z3 \(Apache 2\.0 or MIT\)\. Benchmarks: GSM8K \(MIT\), MATH\-500 \(MIT\), MMLU \(MIT\), AIME\-2024 \(MIT\)\. Commercial APIs were accessed under their providers’ terms of service\.

SymCEitself is released with the code under the MIT Licence and the corpus, verifier modules and human\-audit annotations under CC BY 4\.0\. The corpus consists exclusively of formal mathematical statements and their hypothesis\-dropped mutations; it contains no human\-derived text, no personal information, and no content from which personally identifying information could be derived\.

## Appendix JEval\-Suite Configuration and Reproducibility

All evaluation in the main paper is orchestrated by the multi\-model multi\-benchmark suite runnerpython \-mtraining\.eval\.run\_suite\-\-configconfigs/eval/full\_eval\.yaml, which iterates the cartesian product \{model\}×\\times\{benchmark\}×\\times\{prompt\-style\}×\\times\{greedy, sampled\} and writes one JSON per cell\. Each per\-cell JSON contains asummaryblock \(Pass@kk, by\-domain, and \(where applicable\) subset metrics\) and aper\_recordblock \(one record per test problem with all sample\-level fields:completion,extracted,correct,reason,format\_ok,parse\_ok,is\_none, oracle timing, etc\.\)\.

#### Reproducing the paper from the released artefacts\.

1. 1\.Every table\. python \-mpaper\_preparation\.scripts\.build\_camera\_ready\_tables regenerates all numbers in Tables[2](https://arxiv.org/html/2610.02444#S6.T2),[3](https://arxiv.org/html/2610.02444#S6.T3),[4](https://arxiv.org/html/2610.02444#S6.T4),[5](https://arxiv.org/html/2610.02444#S6.T5),[7](https://arxiv.org/html/2610.02444#A2.T7),[8](https://arxiv.org/html/2610.02444#A3.T8),[9](https://arxiv.org/html/2610.02444#A4.T9),[10](https://arxiv.org/html/2610.02444#A5.T10),[11](https://arxiv.org/html/2610.02444#A7.T11)and[12](https://arxiv.org/html/2610.02444#A7.T12)directly from the raw per\-record evaluation outputs, applying the answer\-extraction rules of §[5\.2](https://arxiv.org/html/2610.02444#S5.SS2)\. It is the single source of truth for this paper\.
2. 2\.Bootstrap CIs\. python \-mpaper\_preparation\.scripts\.bootstrap\_cis regeneratesbootstrap\_cis\.csvandbootstrap\_deltas\.csv\.
3. 3\.Reason distribution \(Fig\.[2](https://arxiv.org/html/2610.02444#S6.F2)\)\. python \-mpaper\_preparation\.scripts\.eval\_reason\_dist regenerates the reason\-counts table\.
4. 4\.All figures\. python \-mpaper\_preparation\.scripts\.make\_plots\-\-all regenerates Figures[2](https://arxiv.org/html/2610.02444#S6.F2),[3](https://arxiv.org/html/2610.02444#S6.F3),[4](https://arxiv.org/html/2610.02444#A1.F4), and[6](https://arxiv.org/html/2610.02444#A7.F6)from the released CSVs\.

#### Dataset fingerprints\.

Each suite run writes adataset\_fingerprint\.jsonfile containing the SHA\-256 hash and line count of every input JSONL used \(the test set, the theorem\-truth probe, and the external\-benchmark sources\)\. These fingerprints are sufficient to verify that all numbers in this paper were produced from the released splits\.

#### Seeds\.

Four training seeds \(42, 19, 31 and 64\) were used; the split seed is fixed at 42 throughout\. The configs are sufficient to reproduce all training runs deterministically up to GPU non\-determinism in the rollout backend \(vLLM tensor\-parallel sampling\); the reported test\-set numbers are robust to this residual non\-determinism within the reported 95 % bootstrap CIs\.