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

arXiv: https://arxiv.org/abs/2610.02444 · HTML: https://mlsanity.com/paper/2610.02444/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 18 of its 24 references that are in the map.
- First posted on arXiv 1 Oct 2026.

## Builds on (most cited first, 18 of 18)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Efficient Memory Management for Large Language Model Serving with PagedAttention](https://mlsanity.com/paper/2309.06180/) (2023)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvement](https://mlsanity.com/paper/2409.12122/) (2024)
- [Spurious Rewards: Rethinking Training Signals in RLVR](https://mlsanity.com/paper/2506.10947/) (2025)
- [Advancing LLM Reasoning Generalists with Preference Trees](https://mlsanity.com/paper/2404.02078/) (2024)
- [Self-rewarding correction for mathematical reasoning](https://mlsanity.com/paper/2502.19613/) (2025)
- [The Hallucination Tax of Reinforcement Finetuning](https://mlsanity.com/paper/2505.13988/) (2025)
- [One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs](https://mlsanity.com/paper/2502.10454/) (2025)
- [TreeCut: A Synthetic Unanswerable Math Word Problem Dataset for LLM Hallucination Evaluation](https://mlsanity.com/paper/2502.13442/) (2025)
- [Future-KL Regularized GRPO: Process-Level Credit Assignment from f-Divergence Regularization](https://mlsanity.com/paper/2601.10201/) (2026)
- [Efficient PRM Training Data Synthesis via Formal Verification](https://mlsanity.com/paper/2505.15960/) (2025)
- [Can Language Models Falsify? Evaluating Algorithmic Reasoning with Counterexample Creation](https://mlsanity.com/paper/2502.19414/) (2025)
- [Learning to Disprove: Formal Counterexample Generation with Large Language Models](https://mlsanity.com/paper/2603.19514/) (2026)
- [Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation](https://mlsanity.com/paper/2410.15748/) (2024)

## Abstract (arXiv)

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.