Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs

Omar Farouk Zouak; Houssam Eddine Boukhalfa; Soumaya Lakehal; Shiv Katiyar; Samia Nefti-Meziani

cs.CLOct 1, 2026

Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs

Authors: Omar Farouk Zouak, Houssam Eddine Boukhalfa, Soumaya Lakehal, Shiv Katiyar, Samia Nefti-Meziani

Organizations: National School of Artificial Intelligence, Algiers, Algeria · 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 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.

Figures & tables

Domain	Strict	SFT	RLVR	Test
GroupTheory	874	366	434	74
RingTheory	565	237	280	48
NumberTheory	392	164	195	33
LinearAlgebra	233	98	115	20
FieldTheory	166	70	82	14
RealAnalysis	159	67	79	13

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 RLVR

1{,}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.

Model	Pass@1 (greedy)	Pass@8 (sampled)	Concl.-pass	Format-OK	Parse-OK
Qwen3-4B base	0.30 [0.24, 0.37]	0.49 [0.42, 0.56]	0.30	0.45	0.42
+ SFT	0.35 [0.28, 0.41]	0.64 [0.57, 0.70]	0.41	1.00	0.82
+ RLVR (dense)	0.50 [0.43, 0.57]	0.68 [0.61, 0.74]	0.61	0.98	0.94
+ RLVR (sparse)	0.50 [0.43, 0.57]	0.67 [0.61, 0.74]	0.59	0.97	0.95
Best open-weights 7B (Eurus-2-7B-PRIME)	0.30 [0.24, 0.36]	0.57 [0.50, 0.64]	0.34	0.87	0.70
Frontier APIs (range over 6) a	0.42 – 0.58	up to 0.77	—	—	—

Table 2: In-domain counterexample benchmark (n=201), reference seed 42. Greedy Pass@1 is the headline metric; 95 % bootstrap CIs in brackets. Conclusion-pass is the relaxed criterion

q_{\neg}{=}1

of § 5.2 . Four-seed means for the trained variants are in Table 5 . a Range across six DeepSeek/Gemini frontier APIs. The full per-model open-weights table is in Appendix G .

Model	SymCE -prompt	truth-classify
Qwen3-4B base	0.27	0.36
+ SFT	0.00	0.21
+ RLVR (dense)	0.34	0.73
+ RLVR (sparse)	0.65	0.84

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 . Four-seed means are in Table 5 . The base column is conservative: on 62 % of items the base states no verdict at all, exhausting the token budget mid-reasoning, and it asserts FALSE on only 2.6 %. SFT reverses this, asserting FALSE for 70 % of true theorems. Four-seed spread for both columns is in Table 5 .

Figure 2: Per-sample outcome distribution on the counterexample benchmark (greedy, n=201). The oracle assigns each rollout exactly one outcome: success (

q_{\neg}{=}1

and all hypotheses satisfied),

\neg

Q only (

q_{\neg}{=}1

but not all hypotheses), abstain (the NONE sentinel on a false conjecture), hyp-only (all hypotheses satisfied but

q_{\neg}{=}0

, so the policy asserts the false conjecture is true), partial , parse error and no tag . The released records carry these as the codes success , neg_q_only , none_on_false , hyp_only , partial , oracle_parse_error and no_tag .

Figure 3: Per-domain counterexample Pass@1 (greedy) with 95 % bootstrap CIs. Annotations on top: number of test items per domain. The largest absolute gain 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.

Benchmark (n)	base	SFT	dense	sparse
GSM8K (1319)	0.83	0.82 $\pm$ .03	0.88 $\pm$ .02	0.88 $\pm$ .01
MATH-500 (500)	0.13	0.55 $\pm$ .01	0.65 $\pm$ .02	0.65 $\pm$ .01
MMLU-CM (100)	0.34	0.54 $\pm$ .03	0.70 $\pm$ .05	0.72 $\pm$ .04
AIME-2024 (30)	0.00	0.07 $\pm$ .03	0.08 $\pm$ .03	0.08 $\pm$ .02

Table 4: Out-of-domain transfer under standard chain-of-thought prompting (greedy, Pass@1), mean

\pm

sd 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.

Qwen3-4B, mean $\pm$ sd over 4 seeds
Metric	base	SFT	dense	sparse
SymCE Pass@1	0.30	0.34 $\pm$ .02	0.49 $\pm$ .02	0.46 $\pm$ .03
SymCE Pass@8	0.49	0.62 $\pm$ .02	0.66 $\pm$ .02	0.64 $\pm$ .02
Truth SymCE -prompt	0.27	0.00 $\pm$ .00	0.33 $\pm$ .04	0.66 $\pm$ .04
Truth-classify	0.36	0.16 $\pm$ .05	0.71 $\pm$ .09	0.75 $\pm$ .13
Gemma-3-4B, seed 56

Table 5: Robustness of the headline findings. SymCE Pass@

k

is the counterexample benchmark (n=201); the two Truth rows are the theorem-truth probe (n=347) under the two prompt styles of § 5.2 . Qwen3-4B seeds are 42, 19, 31 and 64; the base is training-seed independent. Bold marks the best value in a row.

Appendix figures & tables9 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 4: Per-step training curves for the dense and sparse RLVR runs at the reference seed (

\approx

1,752 steps over four epochs of 3,506 prompts). Mean reward rises monotonically and crosses zero by step

\sim

240 for both variants; KL to the SFT reference decays smoothly; loss is bounded and oscillatory but stable.

Supervised fine-tuning (SFT)
Base model	unsloth/Qwen3-4B
Chat template	qwen-3
Max sequence length	2048
Precision	bfloat16
LoRA rank $r$ / scale $\alpha$	16 / 16
LoRA dropout	0

Appendix

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.

Domain	accepted	rejected	total
GroupTheory	31	27	58
RingTheory	20	15	35
NumberTheory	23	8	31
LinearAlgebra	11	11	22
FieldTheory	8	8	16
RealAnalysis	8	7	15

Appendix

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 at human_eval/ .

	SymCE -prompt		truth-classify
Model	strict	permissive	strict	permissive
Qwen3-4B base	0.27	0.86	0.36	0.71
+ SFT	0.00	0.00	0.21	0.23
+ RLVR (dense)	0.34	0.37	0.73	0.76
+ RLVR (sparse)	0.65	0.69	0.84	0.84

Appendix

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.

Metric	Arm	42	19	31	64
SymCE Pass@1	SFT	0.348	0.358	0.323	0.338
	dense	0.502	0.478	0.458	0.502
	sparse	0.497	0.438	0.463	0.453
SymCE Pass@8	SFT	0.637	0.617	0.592	0.632
	dense	0.677	0.632	0.672	0.662
	sparse	0.672	0.622	0.632	0.637

Appendix

Table 9: Per-seed values. The sparse-over-dense gap on the SymCE -prompt probe is positive in every seed (

+0.31

+0.42

+0.35

+0.22

); on truth-classify it is not (

+0.11

+0.01

+0.19

-0.15

), which is why § 6.6 restricts the claim to the SymCE -prompt probe.

Model	unseen	seen	$\Delta$
Qwen3-4B base	0.244	0.307	$+0.063$
+ SFT	0.000	0.000	$\phantom{+}0.000$
+ RLVR dense	0.274	0.433	$+0.159$
+ RLVR sparse	0.614	0.707	$+0.092$

Appendix

Table 10: SymCE -prompt Pass@1 by subset (greedy, strict scoring, reference seed 42).

\Delta

= seen

-

unseen.

Model	Pass@1 (greedy)	Pass@1 (sampled)	Pass@3 (sampled)	Pass@8 (sampled)
Eurus-2-7B-PRIME	0.299 [0.24, 0.36]	0.292 [0.24, 0.34]	0.458 [0.40, 0.52]	0.567 [0.50, 0.64]
Qwen2.5-Math-7B-Instruct	0.199 [0.14, 0.25]	0.063 [0.05, 0.08]	0.155 [0.12, 0.19]	0.289 [0.23, 0.35]
DeepSeek-Math-7B-RL	0.105 [0.06, 0.15]	0.072 [0.05, 0.09]	0.171 [0.13, 0.21]	0.308 [0.25, 0.37]
Abel-7B-002	0.045 [0.02, 0.07]	0.052 [0.04, 0.07]	0.124 [0.09, 0.16]	0.224 [0.17, 0.28]
MAmmoTH2-7B-Plus	0.000 [0.00, 0.00]	0.040 [0.03, 0.05]	0.106 [0.08, 0.14]	0.219 [0.16, 0.28]
Qwen2.5-Math-1.5B (smaller ref.)	0.010 [0.00, 0.02]	0.017 [0.01, 0.03]	0.045 [0.03, 0.07]	0.095 [0.05, 0.13]

Appendix

Table 11: Open-weights baselines on the counterexample benchmark (n=201). All numbers Pass@

k

with 95 % bootstrap CIs over problem ids. Sampled decoding uses

n=8

, temperature 0.7. Regenerated by build_camera_ready_tables.py .

Model	Pass@1 (greedy)	Pass@1 (sampled)	Pass@3 (sampled)	Pass@8 (sampled)
Gemini-3.1-Flash-Lite	0.577 [0.51, 0.64]	0.565 [0.50, 0.63]	0.638 [0.57, 0.70]	0.687 [0.62, 0.75]
Gemini-3.5-Flash	0.493 [0.42, 0.56]	—	—	—
Gemini-3-Flash-Preview	0.468 [0.40, 0.54]	0.489 [0.44, 0.53]	0.708 [0.65, 0.76]	0.771 [0.71, 0.83]
Gemini-3.1-Pro	0.433 [0.36, 0.50]	—	—	—
DeepSeek-Pro	0.428 [0.36, 0.49]	0.437 [0.38, 0.49]	0.551 [0.49, 0.61]	0.622 [0.55, 0.69]
DeepSeek-Flash	0.423 [0.35, 0.49]	0.432 [0.38, 0.49]	0.562 [0.50, 0.62]	0.637 [0.57, 0.70]

Appendix

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 by build_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.

Explore similar work

Learning to Disprove: Formal Counterexample Generation with Large Language Models
Mar 19, 2026Zenan Li, Zhaoyu Li, Kaiyu Yang +2LLM Mathematical Reasoning Synthetic Data Generation for Language Models
ETH Zurich · University of Toronto · MiroMind +1
Euston: Training Away Mathematical Sycophancy Without Losing the Mathematics
Sep 19, 2026Zehua Cheng, Wei Dai, Jiahao SunClaim Verification LLM Sycophancy
University of Oxford
LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics
Feb 27, 2026Antoine Peyronnet, Fabian Gloeckle, Amaury HayatMathematical Reasoning Benchmarks Automated Theorem Proving
1Ecole Normale Superieure de Rennes · 2Ecole des Ponts Paris · 3Korean Institute for Advanced Study

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

Learning to Disprove: Formal Counterexample Generation with Large Language Models

Zenan Li, Zhaoyu Li, Kaiyu Yang, Xiaoxing Ma+1

ETH Zurich · University of Toronto · MiroMind+1

LLM Mathematical Reasoning Synthetic Data Generation for Language Models Formal Verification

Open paper AskPDF arXiv

Mathematical reasoning demands two critical, complementary skills: constructing rigorous proofs for true statements and discovering counterexamples that disprove false ones. However, current AI efforts in mathematics focus almost exclusively on proof construction, often neglecting the equally important task of finding counterexamples. In this paper, we address this gap by fine-tuning large language models (LLMs) to reason about and generate counterexamples. We formalize this task as formal counterexample generation, which requires LLMs not only to propose candidate counterexamples but also to produce formal proofs that can be automatically verified in the Lean 4 theorem prover. To enable effective learning, we introduce a symbolic mutation strategy that synthesizes diverse training data by systematically extracting theorems and discarding selected hypotheses, thereby producing diverse counterexample instances. Together with curated datasets, this strategy enables a multi-reward expert iteration framework that substantially enhances both the effectiveness and efficiency of training LLMs for counterexample generation and theorem proving. Experiments on three newly collected benchmarks validate the advantages of our approach, showing that the mutation strategy and training framework yield significant performance gains.

Abstract

Explore similar work

Learning to Disprove: Formal Counterexample Generation with Large Language Models

Euston: Training Away Mathematical Sycophancy Without Losing the Mathematics

LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics