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.
Keywords
Subject
Publication details
- Journal
- Not available
- Open access
- Green open access
Cite this article
APA 7
Zouak, O. F., Boukhalfa, H. E., Lakehal, S., Katiyar, S., & Nefti-Meziani, S. (2026). Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs. https://omanscience.com/en/articles/counterexample-generation-via-per-theorem-symbolic-verifiers-when-imitation-hurts-and-reinforcement-repairs
MLA 9
Zouak, Omar Farouk, et al. "Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs." https://omanscience.com/en/articles/counterexample-generation-via-per-theorem-symbolic-verifiers-when-imitation-hurts-and-reinforcement-repairs.
Chicago (author–date)
Zouak, Omar Farouk, Houssam Eddine Boukhalfa, Soumaya Lakehal, Shiv Katiyar, and Samia Nefti-Meziani. 2026. "Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs." https://omanscience.com/en/articles/counterexample-generation-via-per-theorem-symbolic-verifiers-when-imitation-hurts-and-reinforcement-repairs.
Harvard
Zouak, O. F., Boukhalfa, H. E., Lakehal, S., Katiyar, S. and Nefti-Meziani, S. (2026) 'Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs', Available at: https://omanscience.com/en/articles/counterexample-generation-via-per-theorem-symbolic-verifiers-when-imitation-hurts-and-reinforcement-repairs.
Vancouver
Zouak OF, Boukhalfa HE, Lakehal S, Katiyar S, Nefti-Meziani S. Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs. https://omanscience.com/en/articles/counterexample-generation-via-per-theorem-symbolic-verifiers-when-imitation-hurts-and-reinforcement-repairs
IEEE
O. F. Zouak, H. E. Boukhalfa, S. Lakehal, S. Katiyar, and S. Nefti-Meziani, "Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs," https://omanscience.com/en/articles/counterexample-generation-via-per-theorem-symbolic-verifiers-when-imitation-hurts-and-reinforcement-repairs.