SymCE 用逐定理符号验证器生成反例：仅模仿的 SFT 使真定理识别从 0.27 崩到 0.00，稀疏奖励强化学习修复并升至 0.66
相关研究与后续进展
核心概要
该工作把反例生成建模为针对逐定理确定性 Python 验证器的受限见证输出，发布含 4,707 条假猜想及其可执行验证器的 SymCE 语料，并以验证器作为奖励训练 Qwen3-4B：仅反例的 SFT 使真定理识别从 0.27 崩至 0.00，而稀疏结果奖励的 RLVR 修复并超过基座至 0.66，该崩溃在四个随机种子与 Gemma-3-4B 上复现。
Figure 2: Per-sample outcome distribution on the counterexample benchmark (greedy, n=201). The oracle assigns each rollout exactly one outcome: success ( q ¬ = 1 q_{\neg}{=}1 and all hypotheses satisfied), ¬ \neg Q only ( q ¬ = 1 q_{\neg}{=}1 but not all hypotheses), abstain (the NONE sentinel on a false conjecture), hyp-only (all hypotheses satisfied but q ¬ = 0 q_{\neg}{=}0 , so the policy asserts the false conjecture is true), partial , parse error and no tag . The released records carry these as the codes success , neg_q_only , none_on_false , hyp_only , partial , oracle_parse_error and no_tag .
arXiv深度剖析
论文提出并发布 SymCE：4,707 条本科代数与实分析假猜想，每条配有可执行的逐定理 Python 验证器，验证器同时充当奖励函数，使该语料成为训练环境。 相对以往以自然语言或人工评判为中心的反例生成设定，这里把“反例”定义为对确定性验证器的受限见证输出，使正确性判定可执行、可复现。 语料规模与配对结构在摘要中明确给出；验证器决策经 177 次人工审计，准确率 97.7%。
仅用反例数据做 SFT 会出现“模仿陷阱”：真定理识别从 0.27 塌陷到 0.00；随后用稀疏结果奖励的 RLVR 修复该塌陷并超过基座，达到 0.66。 该结果指出监督微调不仅无法弥合证伪差距，还可能主动破坏原有的正向定理识别能力，而强化学习可恢复并提升。 崩溃在四个随机种子以及 Gemma-3-4B 上复现，说明并非单次运行或单一模型的偶然现象。
稀疏奖励与稠密奖励在域内成功率上统计不可区分，但在一个留出校准探针上相差 33 个百分点，作者将该解离追溯到部分得分项。 这提示奖励塑形中的部分得分项会改变模型在校准类探针上的行为，而域内指标无法暴露这一差异。 差异以留出校准探针上的 33 点差距呈现，并被归因于部分得分项这一具体机制。
该 4B 模型优于所有被评估的 7B 开源权重数学专用模型，与六个前沿商业 API 保持竞争力，并在提示不变的条件下迁移到 GSM8K、MATH-500 与 MMLU-college-math。 表明以逐定理验证器为奖励的强化学习在较小参数规模上即可获得跨基准的迁移表现，而非仅拟合训练分布。 比较对象为被评估的 7B 开源数学专用模型与六个商业 API，迁移在三个外部基准上以相同提示进行。
启示与展望
该结果面向需要可执行判定器的形式化数学场景：SymCE 覆盖本科代数与实分析中的假猜想，验证器为逐定理的确定性 Python 程序，因此“反例”被限定为能被该验证器接受的受限见证。对希望以强化学习提升模型证伪能力、并需要可复现奖励信号的研究者与工程团队，这一设置提供了可直接使用的语料、验证器模块与训练配方；其迁移证据来自 GSM8K、MATH-500 与 MMLU-college-math 在提示不变条件下的评测。
本文为摘要级阅读，未包含正文的图表、超参数与完整实验表，因此 SFT 与 RLVR 的具体数据配比、训练步数、稀疏与稠密奖励的精确形式，以及 33 点校准差距的逐项分解，仍需查阅原文确认。校准探针的构造方式与部分得分项的具体定义，是理解该解离能否推广到其他任务的关键开放问题；验证器 97.7% 的人工审计准确率也提示剩余判定误差在更大规模或更难猜想上的表现值得进一步观察。