PaperlayerView exact revision on arXiv

Source-linked AI summary

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

arXiv:2610.02444v1cs.CLcs.AI

TL;DR

Large language models can solve mathematical statements forward yet fail to falsify closely related false claims, and counterexample data and reliable evaluation remain limited. This paper builds SYMCE, a verifier-based falsification and training environment, and finds that sparse-reward verifier-grounded RL repairs the calibration loss from counterexample-only SFT. Its Qwen3-4B model also outperforms evaluated 7B open-weights math specialists and transfers to standard math tasks.

  • Problem

    Models that solve mathematical statements forward can still fail to falsify related false claims, while counterexample data is scarce and SFT alone is insufficient.

    Source: §1 · p. 1

  • Method

    The paper builds SYMCE, a corpus of false conjectures paired with deterministic per-theorem Python verifiers that check emitted witnesses and supply RL rewards.

    Source: §1 · p. 1

  • Results

    True-theorem Pass@1 falls from 0.27 to 0.00 after counterexample-only SFT, while outcome-only RL restores it to 0.66 and Qwen3-4B reaches 0.49 ± 0.02 in-domain Pass@1.

    Source: §1 · p. 2, §7 · p. 8

  • Takeaways & Limitations

    The Qwen3-4B RLVR model exceeds every evaluated 7B open-weights math specialist, remains competitive with frontier APIs, and transfers to GSM8K, MATH-500, and MMLU-college-math.

    Source: §8 · p. 9

    The paper does not cross-evaluate on COUNTERMATH because its test labels and evaluation scripts are unreleased and scoring requires submission for LLM judging.

    Source: Limitations · p. 10

Abstract

from arXiv · show

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.

1 Introduction

The paper addresses the gap between forward mathematical solving and falsifying related false claims, alongside the scarcity of large-scale, symbolically verified counterexample data. It introduces SYMCE as both a benchmark and a verifier-based training environment, and reports that verifier-grounded RL repairs the calibration failure of counterexample-only SFT.

1 Introduction

  • Existing falsification benchmarks are small or use LLM judging, while counterexample-only SFT can erase true-statement recognition.COUNTERMATH contains 1,216 problems, and the authors identify both data scarcity and insufficient SFT as obstacles to making counterexample generation a primary objective.Source: §1 · p. 1

Contributions

  • SYMCE retains 4,707 false-conjecture records with independent executable Python verifiers, which also provide the reward signal for reinforcement learning.The pipeline starts from 6,748 undergraduate-level theorems and uses hypothesis dropping to construct candidates.Source: §1 · p. 1
  • Counterexample-only SFT collapses true-theorem Pass@1 from 0.27 to 0.00, while verifier-grounded outcome-only RL repairs the pathology.The collapse reproduces across all four training seeds and on a second model family; partial-credit dense rewards yield equal in-domain success but do not restore calibration.Source: §1 · p. 2
  • Qwen3-4B RLVR reaches 0.49 ± 0.02 in-domain Pass@1, beats every evaluated 7B open-weights math specialist, and transfers to standard forward-math benchmarks.The paper also reports competitiveness with frontier APIs and zero-shot transfer to MATH-500 and GSM8K.Source: §1 · p. 2

2 Related Work

Related work spans counterexample benchmarks and training resources, verifiable-reward RL for mathematics, process supervision, and imitation-induced calibration failures. The paper positions its contribution as a deterministic falsification environment and an analysis of the calibration effects of reward design.

Counterexample and falsification benchmarks

  • COUNTERMATH contains 1,216 university-level problems and uses LLM judging, while RE-FUTE reports forward solution rates around 48% versus counterexample success below 9%.Learning to Disprove builds roughly 575K Lean 4 Mathlib mutations; SYMCE is smaller but uses a Python-verifier substrate tailored to its evaluated algebraic and real-analytic structures.Source: §2 · p. 2

Verifiable-reward reinforcement learning for mathematics

  • The paper situates its GRPO-based RLVR work among methods developed for forward mathematical reasoning and reports that falsification training transfers to out-of-distribution tasks.The authors interpret those transfer results as suggesting that falsification training installs transferable inverse-reasoning skills.Source: §2 · p. 2

Process supervision and symbolic verifiers

  • Per-theorem verifiers provide a structured boolean signal between outcome rewards and learned process reward models, without PRM annotation costs.Their externally grounded, non-learned boolean tuple lets the authors attribute behavioral change to a reward aggregation term.Source: §2 · p. 2

The hallucination tax

  • Prior work reports imitation-style calibration failures, and this paper localizes its counterexample-generation imitation trap to the partial-credit reward term.The authors describe their finding as the first to localize that mechanism in this setting.Source: §2 · p. 3

3 Dataset and Verification Environment

SYMCE treats falsification as constrained witness generation checked by reusable per-theorem Python verifiers. Its data pipeline, witness schemas, reward variants, and verifier audit define the environment used for training and evaluation.

3.1 Source theorems and hypothesis dropping

  • From 18,262 one-hypothesis-drop candidates, gating distilled 4,707 verifier-backed records across 3,485 unique theorems after teacher checks for well-posedness, non-triviality, valid Python verifiers, and verifier-valid counterexamples.The teacher produced verifiers for 12,376 candidates; 4,700 retained records carry a witness schema.Source: §3.1 · p. 3

3 Dataset and Verification Environment

  • A reusable Python verifier evaluates a witness expression and returns booleans for each remaining hypothesis and the negated conclusion, providing deterministic symbolic checking.The policy and verifier share no code paths beyond Python eval; the verifier is fixed for each conjecture across rollouts.Source: §3.1 · p. 3

3.2 Witness-schema interface

  • Automatically generated witness schemas specify the acceptable Python object shape and are included in prompts as a structural prior for RLVR.The paper describes schemas as enabling practical RLVR effectiveness without changing the reward function or verifier.Source: §3.2 · p. 3

3.3 Split construction

  • The fixed-seed, domain-stratified split assigns 201 records to test, 1,000 to SFT, and 3,506 to the RLVR prompt set.The RLVR set combines 1,188 strict-pool records with 2,318 loose records.Source: §3.3 · p. 3, Table 1 · p. 4

3.4 Reward function

  • The oracle reward uses satisfied-hypothesis counts, a negated-conclusion indicator, format and parse checks, and a penalty for emitting NONE.The dense variant uses partial-credit weights, whereas the sparse variant has reward range {−1, 0, +1}.Source: §3.4 · p. 4
  • In the dense reward design, any valid rollout that negates the conclusion strictly dominates a hypothesis-only failure, preventing that failure mode from earning the higher reward.The comparison applies to formatting-compliant rollouts that have not given up.Source: §3.4 · p. 4

3.5 Verifier audit and operational measurements

  • A human audit of 177 model-generated witnesses found 97.7% verifier-decision accuracy, with 99/101 accepted witnesses valid and 74/76 rejected witnesses invalid.The oracle's median call time was 132 ms, with a p95 of 145 ms and a maximum of 326 ms.Source: §3.5 · p. 4

4 Training Setup

The training setup fine-tunes Qwen3-4B with SFT and then applies GRPO-based RLVR from the SFT adapter. The runs use LoRA and are conducted on a single consumer GPU.

4 Training Setup

  • Qwen3-4B is trained with SFT followed by GRPO-based RLVR, initialized for RLVR from the SFT adapter.SFT runs for 2–3 epochs; RLVR runs for four epochs, approximately 1,752 steps.Source: §4 · pp. 4–5
  • RLVR samples four rollouts per prompt and uses a KL penalty of 0.02 against the SFT reference policy.Both stages use rank-16 LoRA on attention and MLP modules with bfloat16 precision.Source: §4 · p. 5
  • Training runs on one NVIDIA RTX 5090 with SFT under five minutes and each RLVR run taking about nine hours.The paper places full hyperparameters, optimizer configurations, and prompt templates in Appendix A.Source: §4 · p. 5

5 Experimental Setup

The experiments compare Qwen3-4B checkpoints and external models across counterexample, theorem-truth, and standard math benchmarks. They use greedy and sampled decoding, with greedy Pass@1 as the headline metric.

5.1 Models

  • The setup evaluates an unmodified Qwen3-4B base, an SFT checkpoint, and dense- and sparse-reward RLVR checkpoints, alongside five 7B specialists and six frontier APIs.Gemma-3-4B is used for a cross-family replication.Source: §5.1 · p. 5

5.2 Benchmarks

  • The benchmark suite includes 201 held-out counterexample items, 347 true-theorem probes under two prompt styles, and four external math benchmarks.The external set comprises GSM8K, MATH-500, MMLU-college-math, and AIME-2024; the training splits contain none of these examples or answer-extraction formats.Source: §5.2 · p. 5

5.3 Decoding and metrics

  • Greedy Pass@1 is the headline metric; sampled decoding uses temperature 0.7 and eight rollouts, with Pass@k estimated using Chen et al. (2021).Confidence intervals use 10,000 bootstrap resamples over problem IDs, and paired deltas bootstrap per-problem differences.Source: §5.3 · p. 5

6 Results

Verifier-grounded RL improves counterexample generation over the base, while counterexample-only SFT sharply harms true-theorem recognition. Dense and sparse rewards have similar in-domain success but differ on calibration, and the reported gains extend across domains and external math benchmarks.

6.1 Counterexample generation

  • 0.50 [0.43, 0.57] greedy Pass@1: verifier-grounded RL beats the Qwen3-4B base at 0.30, while the 4B RLVR model exceeds every evaluated 7B specialist and is competitive with frontier APIs.Across four seeds, dense and sparse RLVR reach 0.49 ± 0.02 and 0.46 ± 0.03, respectively; the six frontier APIs range from 0.42–0.58.Source: §6.1 · pp. 5–6, Table 2 · p. 6

6.2 The imitation trap

  • 0.27 to 0.00: counterexample-only SFT collapses true-theorem Pass@1 under the training-style prompt, while sparse-reward RLVR restores and exceeds the base.Sparse RLVR reaches 0.65 on the training-style probe and 0.84 under explicit classification; dense RLVR reaches 0.34 on the training-style probe, and the reward variants differ by 33 ± 8 points across four seeds.Source: Table 3 · p. 6, §6.2 · p. 6

6.3 Why it happens: a reason-taxonomy analysis

  • SFT trades format errors for logical errors: hyp-only failures rise from 1% to 31%, as the model satisfies remaining hypotheses but asserts the false conclusion.Sparse RL reintroduces abstention (10%, versus 2% under dense RL); the authors attribute the calibration gap to dense reward’s partial-credit term, which favors trying a partially successful witness over abstaining. Dense and sparse success fractions are nearly identical (0.502 vs 0.497), but their remaining failures differ.Source: §6.3 · p. 7

6.4 Cross-domain consistency

  • Both RLVR variants improve over the base in every domain; Real Analysis rises from 0.23 to 0.46 despite comprising only 6.7% of RLVR training.Figure 3 reports per-domain counterexample Pass@1 with 95% bootstrap confidence intervals; dense and sparse intervals overlap in almost every domain.Source: Figure 3 · p. 7, §6.4 · p. 7

6.5 Out-of-domain transfer

  • Training improves performance across four external math benchmarks under identical chain-of-thought prompts, with no benchmark examples or answer-format training in the pipeline.On GSM8K, RLVR reaches 0.88 versus the base’s 0.83, while SFT alone does not improve on the base; the authors note that part of the MATH-500 gain reflects answer-format adaptation.Source: §6.5 · pp. 7–8, Table 4 · p. 8

6.6 Robustness across seeds and model families

  • The imitation trap replicates across all four Qwen seeds and on Gemma-3-4B; the sparse-over-dense calibration gap on the training-style probe is positive in every Qwen seed at +0.33 ± 0.08.On the explicit classification probe, the sparse advantage is smaller and less consistent, so the authors restrict that calibration claim to the training-style probe.Source: Table 5 · p. 8, §6.6 · p. 8

7 Discussion

The discussion distinguishes counterexample-only SFT’s selective calibration failure from generic forgetting and explains why sparse rewards better preserve abstention. It also bounds the verifier’s scope and presents cross-domain results as evidence for transferable inverse reasoning.

7 Discussion

  • SFT improves MATH-500 (0.13 → 0.55) while true-theorem recognition falls to 0.00; sparse RL raises recognition from 0.27 → 0.66.The dense-versus-sparse comparison holds data and initialization fixed and still differs by 33 points; no true theorems appear in training.Source: §7 · p. 8

Why sparse generalises better on calibration

  • Dense partial credit rewards parsed counterexamples even when the conjecture is true, whereas sparse reward rewards only correct negation and leaves abstention no worse than a wrong witness.Sparse reward has a higher in-distribution abstention rate (10% vs 2%) and preserves abstention on true theorems; the dense partial-credit term is in tension with calibration.Source: §7 · p. 9

7 Discussion

  • The authors conjecture this approach may generalize when rewards provide structured boolean tuples and the target failure is answering instead of abstaining; whether it survives at scale remains future work.Source: §7 · p. 9

Deterministic verification

  • The verifier achieves 97.7% accuracy across 177 human-checked decisions, but its scope is bounded by problems decidable in Python with SymPy/Z3.Construction-time LLM dependence is frozen and auditable, unlike stochastic LLM-judge error at each evaluation.Source: §7 · p. 9

Counterexample reasoning as a fundamental capability

  • Real Analysis (6.7% training share, +0.23 absolute gain) and MATH-500 (+52 percentage-point gain) are presented as evidence that falsification training transfers beyond disproof.The authors interpret these results as support for transferable inverse-reasoning skill.Source: §7 · p. 9

8 Conclusion

The paper presents SYMCE as a counterexample-generation dataset and verification environment, using it to identify an imitation trap in counterexample-only SFT. Sparse verifier-grounded RL repairs calibration, and the trained model transfers to external math benchmarks.

8 Conclusion

  • Counterexample-only SFT collapses true-theorem recognition, while sparse outcome-only verifier-grounded RL repairs and exceeds original calibration; dense partial-credit reward does not.The collapse replicates across every training seed and on a second model family.Source: §8 · p. 9
  • The resulting Qwen3-4B model exceeds every evaluated 7B open-weights math specialist, remains competitive with frontier commercial APIs, and transfers under unchanged prompting to three external benchmarks.The benchmarks are GSM8K, MATH-500, and MMLU-college-math.Source: §8 · p. 9
  • The release includes the dataset, verifier modules, human-audit annotations, witness-schema generator, and full evaluation pipeline; proposed next steps include broader domains and larger scales.The authors also identify alternative RL algorithms and a Lean back-end as possible extensions.Source: §8 · p. 9

Limitations

The study leaves scale, parameterisation, RL algorithm, verifier coverage, mutation breadth, benchmark comparison, audit strength, and teacher dependence as boundaries on its claims.

Scale, parameterisation and RL algorithm

  • All trained variants use 4B LoRA models with GRPO, leaving larger scales, full-parameter fine-tuning, and alternative RL algorithms untested.Full fine-tuning with GRPO rollouts was infeasible on the available compute, so environment and algorithm effects cannot be separated; scaling is the main open question.Source: Limitations · pp. 9–10

Verifier scope

  • The Python, SymPy, and Z3 substrate covers the six evaluated subdomains, but not topology, general higher-order logic, or claims reducible to undecidable fragments.The authors identify a Lean backend or continuous-FOL extensions for metric spaces as possible follow-ups.Source: Limitations · p. 10

Audit scope

  • The 177-decision audit was annotated by one author, reports no interannotator agreement, and bounds the verifier collection’s error rate only coarsely.The authors say a larger, independently annotated audit would support stronger claims.Source: Limitations · p. 10

Mutation strategy and scope of the resource claim

  • SYMCE mutates statements only by dropping one hypothesis, enabling attributable falsity and per-hypothesis outcomes while leaving other mutation strategies unexplored.Conclusion mutation, multiple-hypothesis dropping, and AST-level mutation would broaden the distribution but complicate attribution; SYMCE is a falsification environment, not a benchmark of all mathematical fallacies.Source: Limitations · p. 10

No COUNTERMATH cross-evaluation

  • The study does not cross-evaluate on COUNTERMATH because its labels and scripts are unavailable and its scoring requires external LLM-judged submissions.The authors leave comparison against the published frontier on that broader-coverage benchmark for future work.Source: Limitations · p. 10

Teacher model dependence

  • Verifier generation depends on Gemini 3.1 Pro and witness schemas on DeepSeek, so teacher-output quality remains a pipeline dependency.Multi-model consensus generation before verifier inclusion is proposed but not implemented.Source: Limitations · p. 10

Ethics and Risk Considerations

The authors report no notable dual-use risks beyond those general to LLM mathematical reasoning, and describe the released artifacts and training runs. The appendix records the run configurations and reports stable, completed RLVR curves.

Ethics and Risk Considerations

  • The released dataset contains formal mathematical statements and hypothesis-dropped mutations, with no human-derived text, personal information, or content from which PII could be derived.The models are for research use, not deployed in a user-facing setting, and the methodology is not said to meaningfully extend existing open-source mathematical reasoning capabilities; artefact licences are listed in Appendix I.Source: Ethics and Risk Considerations · p. 10

A Full Hyperparameters

  • Both RLVR runs completed four epochs without restart, gradient explosion, or reward collapse, while reward rose and KL and loss remained controlled.Reward crossed zero by about step 240; the reported curves show smooth KL decay and bounded, oscillatory loss.Source: A Full Hyperparameters · p. 12, Figure 4 · p. 12
  • Table 6 records the SFT and RLVR hyperparameters; SFT used three epochs for seed 42 and two for seeds 19, 31, and 64.SFT took under five minutes and each RLVR run approximately nine hours on a single RTX 5090 32 GB; the reference-seed configs and resolved run configs are identified as records of the settings.Source: Table 6 · p. 12, A Full Hyperparameters · p. 12

B Human Audit of Verifier Decisions

The human audit confirms most verifier decisions but identifies errors associated with witness validity, schema quality, and hypothesis-drop label noise. The appendix also checks extraction-rule sensitivity and points to per-seed results underlying reported means.

B Human Audit of Verifier Decisions

  • 173/177 verifier decisions were confirmed correct, for 97.7% overall accuracy in the human audit.The audit confirmed 99/101 accepted witnesses as valid and 74/76 rejected witnesses as invalid.Source: Table 7 · p. 13
  • Four decisions were disputed: two accepted witnesses were invalid, while two rejected witnesses were judged wrong for reasons involving schema quality or a true conjecture after hypothesis dropping.The two invalid acceptances failed the negated-conclusion check or used a malformed field construction; the two rejections involved a namespace mismatch and a case where no counterexample existed.Source: B Human Audit of Verifier Decisions · p. 13
  • Only 9 of 76 rejected cases have free-text annotations, so the audit cannot estimate how often correct mathematics was rejected for Python namespace or API usage.The annotator noted examples such as using Matrix instead of sympy.Matrix.Source: B Human Audit of Verifier Decisions · p. 13

C Answer Extraction and the Scoring Correction

  • The permissive fallback parser could treat an unfinished chain of thought as a verdict, an effect concentrated in the base model; trained models were barely affected.The strict truth-classify rule recorded no verdict only for unfinished completions, not normally terminated responses.Source: C Answer Extraction and the Scoring… · p. 13
  • Under both extraction rules and in every seed, SFT scores 0.00 on the SYMCE-prompt probe and the sparse-over-dense gap is 0.31.The extraction choice changes the base model’s apparent calibration and whether RLVR is described as exceeding it.Source: C Answer Extraction and the Scoring… · p. 13

D Per-Seed Results

  • Table 9 gives individual seed values underlying Table 5’s means; the base model is training-seed independent and evaluated once per suite.Source: D Per-Seed Results · p. 13

E Theorem-Truth Robustness: Seen vs Unseen Subsets

On the theorem-truth probe, the sparse-over-dense calibration gap is larger on unseen than on the full probe; the accompanying sections document qualitative failures, comparator sets, witness schemas, release terms, and reproducibility practices.

E Theorem-Truth Robustness: Seen vs Unseen Subsets

F Qualitative Examples

  • Sparse reward's improved calibration on true theorems costs false abstentions on genuinely false conjectures.The qualitative examples also show SFT producing a syntactically valid counterexample that fails the negated-conclusion check.Source: Figure 5 · p. 14, F Qualitative Examples · p. 14

G Per-Model Baseline Breakdowns

  • Figure 6 compares trained 4B models with five 7B open-weights specialists and the range across six frontier commercial APIs.Tables 11 and 12 report the per-model scores for those open-weights and commercial-API comparators.Source: Figure 6 · p. 14, G Per-Model Baseline Breakdowns · p. 14

H Witness-Schema Generator and Example Schemas

  • The witness-schema generator queries a teacher model for acceptable Python witness shapes and examples; schemas span multiple subdomains and are 10–40 tokens long.Their median prompt overhead is well below the reported 120-token SFT user-prompt median.Source: H Witness-Schema Generator and Example… · pp. 14–15

I Artefact Licences

  • SYMCE is released under MIT, while its corpus, verifier modules, and human-audit annotations use CC BY 4.0; the corpus contains no personal information.The corpus consists of formal mathematical statements and hypothesis-dropped mutations.Source: I Artefact Licences · p. 15

J Eval-Suite Configuration and Reproducibility

  • Reproduction is supported by dataset fingerprints and four training seeds, with reported test-set numbers robust to residual rollout-backend nondeterminism within 95% bootstrap CIs.The evaluation suite records per-problem outputs and metrics for each run.Source: J Eval-Suite Configuration and… · p. 16

Related papers

Loading 2610.02444v1…