SymCE：逐定理符号验证器生成反例，模仿有害而强化修复
原标题：Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs
AI 摘要
该论文提出 SymCE，一个包含 4,707 个假数学猜想及逐定理 Python 验证器的确定性反例生成环境，验证器同时充当强化学习奖励函数。作者发现仅用反例数据做 SFT 会导致「模仿陷阱」，使模型识别真定理的能力从 0.27 崩溃至 0.00，而基于验证器的 RLVR 可修复该问题并提升至 0.66。训练后的 Qwen3-4B 在域内反例任务上超越所有评测的 7B 开源数学专用模型，并与六个前沿商业 API 保持竞争力，同时可零样本迁移到 GSM8K、MATH-500 和 MMLU-college-math。
正文节选
Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs 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 rea