SymCE generates counterexamples with per-theorem symbolic verifiers: counterexample-only SFT collapses true-theorem recognition from 0.27 to 0.00, while sparse-reward RL repairs it to 0.66

The paper introduces and releases SymCE: 4,707 false undergraduate-algebra and real-analysis conjectures, each paired with an executable per-theorem Python verifier that also serves as the reward function, making the corpus a training environment. Where earlier counterexample-generation settings center on natural language or human judgment, this work defines a counterexample as constrained witness emission against a deterministic verifier, making correctness executable and reproducible. The corpus size and pairing structure are stated in the abstract; verifier decisions were human-audited over 177 cases with 97.7% accuracy.

Counterexample-only SFT produces an imitation trap: true-theorem recognition collapses from 0.27 to 0.00, and RLVR with a sparse outcome-only reward repairs this and exceeds the base, reaching 0.66. The result indicates supervised fine-tuning not only fails to close the falsification gap but can actively damage existing forward-theorem recognition, whereas reinforcement learning restores and improves it. The collapse replicates across four seeds and on Gemma-3-4B, indicating it is not a single-run or single-model artifact.

Sparse and dense rewards are statistically indistinguishable on in-domain success yet diverge by 33 points on a held-out calibration probe, a dissociation the authors trace to the partial-credit term. This suggests the partial-credit term in reward shaping changes model behavior on calibration-style probes in ways in-domain metrics do not expose. The difference is presented as a 33-point gap on a held-out calibration probe and attributed to the specific mechanism of the partial-credit term.

The 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. This indicates that reinforcement learning with per-theorem verifiers as reward can yield cross-benchmark transfer at a smaller parameter scale rather than only fitting the training distribution. Comparisons are against evaluated 7B open-weights math specialists and six commercial APIs, with transfer measured on three external benchmarks under identical prompting.

The result targets formal mathematics settings that admit an executable checker: SymCE covers false conjectures in undergraduate algebra and real analysis, and the verifiers are deterministic per-theorem Python programs, so a counterexample is bounded to a witness that verifier accepts. For researchers and engineering teams seeking to improve a model's falsification ability with a reproducible reward signal, this setting offers directly usable corpora, verifier modules and a training recipe; the transfer evidence comes from GSM8K, MATH-500 and MMLU-college-math under unchanged prompting.

This is a summary-level reading without the body's figures, hyperparameters or full experiment tables, so the exact data mix and step counts for SFT and RLVR, the precise form of the sparse and dense rewards, and the item-by-item decomposition of the 33-point calibration gap still require the original text. How the calibration probe is constructed and how the partial-credit term is defined are key open questions for judging whether the dissociation generalizes to other tasks; the 97.7% human-audit accuracy of verifier decisions also leaves residual judgment error whose behavior at larger scale or on harder conjectures merits further observation.