🔥 今日值得一读
SFT让真定理识别率从0.27崩到0.00，RLVR修复后反超至0.66！
Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs
👨💼 主理人解读 · 为什么值得关注
用可执行验证器作奖励训练LLM生成数学反例，解决SFT反而变差的问题，适合形式化推理训练。
📖 AI 总结
该研究针对大语言模型能正向证明定理、却难以反驳相近错误命题的“证伪鸿沟”问题，将反例生成重新定义为面向确定性逐定理Python验证器的受限见证输出任务，并发布了包含4707个错误本科学代数与实分析猜想及其可执行验证器的SymCE语料库，验证器同时充当奖励函数。实验以Qwen3-4B为对象，先做监督微调再做GRPO强化学习，发现“模仿陷阱”：仅用反例数据做SFT会使真定理识别率从0.27骤降至0.00，而采用稀疏结果奖励的RLVR可修复该问题并提升至0.66，该崩溃在四个随机种子及Gemma-3-4B上均可复现。稀疏与稠密奖励在域内成功率上无显著差异，但在校准探针上相差33个百分点，作者将其归因于部分得分项。该4B模型超越所有受评的7B开源数学专用模型，与六个前沿商业API相当，并可零样本迁移至GSM8K、MATH-500和MMLU大学数学；对177项验证器决策的人工审计准确率达97.7%。
🔑 关键词速览
| SymCE | 一个包含4,707个错误数学猜想及其可执行验证器的语料库，用于训练和评估反例生成模型。 |
| GRPO | 一种强化学习算法，通过分组相对策略优化来训练语言模型，常用于RLVR中。 |
| RLVR | 可验证奖励的强化学习，利用确定性验证器作为奖励函数来训练模型。 |
| 模仿陷阱 | 指仅使用反例进行监督微调时，模型会丧失识别真定理的能力，导致性能崩溃的现象。 |
| 证伪差距 | 模型能证明真定理却无法反驳相关错误命题之间的能力差异。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅