SymCE：符号验证器驱动的反例生成

大语言模型常能正向证明定理却无法否证一个相近的假命题：这一否证差距监督微调不能弥合，甚至会主动恶化。我们把反例生成表述为针对确定性逐定理Python验证器的受限见证发射，并发布SymCE：4707个假的本科代数与实分析猜想语料，每个配可执行验证器；验证器兼作奖励函数，使SymCE成为训练环境。在该oracle下以SFT+GRPO训练Qwen3-4B揭示出模仿陷阱：仅反例的SFT使真定理识别从0.27崩塌至0.00，而稀疏结果奖励的RLVR修复并超越基座至0.66。该崩塌在四个种子与Gemma-3-4B上复现。稀疏与稠密奖励的域内成功在统计上不可区分，却在留出校准探针上相差33分，我们把这一分离追溯到部分得分项。我们的4B模型超过所有受评7B开放权重的数学专精模型，与六个前沿商用API具竞争力，并在提示不变下迁移到GSM8K、MATH-500与MMLU-college-math。对177个验证器决策的人工审计准确率97.7%。代码/项目页：https://github.com/ce-rlvr/SymCE。