SymCE

The SymCE paper reformulates the counterexample generation task as 'constraint witness emission targeting a deterministic verifier,' requiring the model to produce, for each false proposition, a counterexample that can be judged valid by a Python verifier.

The SymCE corpus contains 4,707 undergraduate-level false conjectures in the domains of algebra and real analysis, each accompanied by an executable verifier.

SymCE's verifier is used both for evaluation and directly as the reward function for reinforcement learning.

Manual review of 177 verifier judgments shows an accuracy of 97.7%.

Using Qwen3-4B as the base model, applying supervised fine-tuning with only counterexample data causes the model's ability to recognize true theorems to collapse from 0.27 to 0.00.

Using a sparse reinforcement learning reward signal based solely on final outcomes, the model repaired the true-theorem recognition ability destroyed by SFT and raised the recognition rate to 0.66, surpassing the base model.

Sparse and dense rewards are statistically indistinguishable on in-domain success rate, but the gap reaches 33 percentage points on held-out calibration probe tests.

The researchers traced the calibration difference between sparse and dense rewards to the 'partial credit' term in the dense reward.

The trained 4B-parameter model outperforms all 7B open-source math-specialized models evaluated on the counterexample generation task and remains competitive with six frontier commercial APIs.

Without changing the prompt, the capabilities of the SymCE-trained model transfer to mainstream mathematical reasoning benchmarks such as GSM8K, MATH-500, and MMLU-college-math.

The SymCE team has fully open-sourced the code, data, verifier module, and annotations (github.com/ce-rlvr/SymCE).