Breakthrough in Counterexample Generation: Symbolic Verifiers Expose the Imitation Learning Trap and How RL Fixes It

Large language models have a little-known blind spot: a model can prove a theorem forward, yet often fails to refute a similar but incorrect proposition. This "falsification gap" not only resists being closed by supervised fine-tuning — it can actually make things worse. A newly released arXiv paper (SymCE) systematically exposes the mechanism behind this phenomenon by constructing per-theorem symbolic verifiers, and offers a concrete repair path using reinforcement learning.

What Is the Counterexample Generation Task

Counterexample generation is essentially the task of producing a concrete falsifying instance for an incorrect conjecture. The paper reframes this as "constrained witness emission toward a deterministic verifier" — the model must, for each false proposition, produce a counterexample that a Python verifier judges as valid.

The research team released the SymCE corpus, comprising 4,707 undergraduate-level false conjectures in algebra and real analysis, each paired with an executable verifier. The elegance of this design lies in the dual role of the verifier: it serves not only as an evaluation tool but also directly as the reward function for reinforcement learning. In other words, SymCE is itself a complete training environment, not merely a static dataset.

The reliability of the verifiers was confirmed through human audit — manual review of 177 verifier judgments showed an accuracy of 97.7%, providing a solid ground-truth foundation for subsequent training and evaluation.

What is GRPO? GRPO (Group Relative Policy Optimization) is a reinforcement learning algorithm proposed by the DeepSeek^Ad team, and is a variant of PPO (Proximal Policy Optimization). Its core idea is to sample a group of outputs for the same input, then use intra-group relative scores in place of a traditional value function estimate — eliminating the need to train a separate Critic network. In mathematical reasoning settings, GRPO is typically used alongside verifiable final-outcome rewards (e.g., whether an answer is correct), allowing the model to self-improve by contrasting which reasoning paths ultimately succeed. In SymCE, Python verifiers directly judge the validity of counterexamples, which naturally aligns with GRPO's preference for binary or sparse reward signals — making the verifier both an evaluation tool and a seamless component of the training loop.

The Imitation Trap: Why Supervised Fine-Tuning Backfires

The paper's most striking finding is what it calls the "imitation trap." The researchers used Qwen3-4B as the base model, first applying supervised fine-tuning (SFT), then training with GRPO (a reinforcement learning method).

The results are alarming: SFT on counterexample data alone causes the model's ability to recognize true theorems to collapse from 0.27 all the way to 0.00. In other words, in learning to generate counterexamples, the model completely loses its ability to judge whether a proposition is true — it begins attempting to construct counterexamples for every proposition, even correct ones.

This collapse is not a fluke. The researchers observed the same phenomenon across four random seeds, and replicated it on Gemma-3-4B, demonstrating that this is a systemic flaw in the supervised fine-tuning paradigm itself — not an artifact of a specific model or training configuration.

Why does SFT cause this? The essence of SFT is maximizing the log-likelihood of demonstration data, training the model to reproduce the output distribution of human (or synthetic) annotations as closely as possible. When nearly all training samples involve the action of "providing a counterexample," the model binds the behavior pattern of "generating a counterexample" to any mathematical proposition input, rather than learning the conditional logic of "first judge true or false, then decide whether to falsify." This distributional bias is known in NLP as "shortcut learning": the model exploits surface-level statistical patterns in the data rather than deep reasoning to minimize training loss. The complete collapse of Qwen3-4B's true-theorem recognition rate after SFT in the SymCE experiments is an extreme manifestation of this mechanism — the newly learned output tendency completely overwrites the true/false judgment capability formed during pretraining.

How Reinforcement Learning Repairs the Capability Collapse

In sharp contrast to SFT, reinforcement learning with verifiable rewards (RLVR) not only repairs the true-theorem recognition ability destroyed by SFT, but also surpasses the base model, raising the recognition rate to 0.66.

This comparison reveals an important philosophical difference in training approaches: imitation-based learning (SFT) has the model mechanically replicate counterexample generation behavior, yet destroys existing capabilities due to distributional bias in the data; reinforcement learning, through interaction with a deterministic verifier, allows the model to autonomously establish — through exploration — the judgment boundary of "when to falsify versus when to accept as true."

The Subtle Divergence Between Sparse and Dense Rewards

The study also delves into a detailed comparison of sparse versus dense reward signals. On in-domain success rates, the two are statistically indistinguishable; however, on a held-out calibration probe, the gap between them reaches 33 percentage points.

The researchers trace this difference back to the "partial-credit" component in dense rewards. This suggests that seemingly harmless reward shaping can quietly introduce bias at the level of generalization and calibration — identical in-domain metrics do not mean the model has learned equally reliable reasoning.

Sparse vs. dense rewards explained: The fundamental difference between sparse and dense rewards lies in feedback granularity. Sparse rewards only provide a 0/1 signal when the task is finally completed, forcing the model to figure out the successful path on its own; dense rewards provide continuous scores at each step or sub-goal throughout the process, aiming to accelerate learning. "Partial credit" is a typical implementation of dense rewards: even if the final counterexample is invalid, the model still receives partial reward as long as its intermediate output satisfies certain structural conditions (e.g., correct format, reasonable numerical range). The SymCE experiments show that this intermediate incentive produces in-domain success rates close to those of sparse rewards, but subtly distorts the model's internal calibration of "when a proposition is true" — the model may learn local shortcuts while pursuing partial scores, rather than truly understanding the boundary conditions for falsification, ultimately leading to a significant drop on out-of-distribution calibration probes.

Surprising Performance and Generalization from a Small Model

The practical value of this work is equally noteworthy. The trained 4B-parameter model outperforms all evaluated 7B open-source math-specialized models on the counterexample generation task, and remains competitive with six frontier commercial APIs.

More critically, the generalization capability: with no changes to the prompt, the model's capabilities transfer to mainstream mathematical reasoning benchmarks such as GSM8K, MATH-500, and MMLU-college-math. This shows that the falsification ability trained through symbolic verifiers is not overfitting to a specific task, but rather enhances the model's more fundamental mathematical reasoning capacity.

The team has open-sourced all code, data, verifier modules, and annotations (github.com/ce-rlvr/SymCE), providing a fully reproducible toolkit for follow-up research.

Implications for AI Training Methodology

SymCE's value extends beyond being a counterexample generation dataset. It provides several generalizable conclusions backed by rigorous experimental evidence:

• Supervised fine-tuning is not always safe — on certain tasks, simply imitating demonstration data can destroy core capabilities the model already possesses;
• Reinforcement learning with verifiable rewards builds more robust capability boundaries than imitation learning in settings requiring precise judgment;
• Reward design must guard against the hidden calibration biases introduced by shaping techniques like partial credit — in-domain metrics alone are insufficient evidence of true capability.

For teams building reasoning models, these findings offer concrete decision-making guidance on "when to use SFT and when to shift to RL."