验证器驱动的智能体 RL 实现可证明正确代码
原文标题：Verifier-Grounded Agentic RL for Provably Correct Code
重要度 4/5 · AI 综合评估报道影响力与新鲜度，4–5 分为高价值资讯。
论文构建智能体环境与奖励，读取程序验证器的诊断而非仅判定结果，按已履行证明义务的加权比例评分，并加入完整性审计防止策略作弊。在 Qwen3 系列模型上，DafnyBench 留出验证率从 66.1% 升至 93.5%，SWE-Proof 从 56.3% 升至 100%，仓库补丁问题解决率从 59.6% 升至 72.5%。
深读 · 结论先行AI 生成展开看要点与影响 ↓
把验证器诊断当奖励，DafnyBench留出验证率从66.1%升至93.5%
- •奖励读取验证器诊断而非通过/拒绝判定，按已履行证明义务的加权比例打分，解决全失败时无梯度的问题
- •加入完整性审计，拒绝篡改规范或预设待证结论的候选，防止策略作弊
- •Qwen3系列1.7B至14B及35B MoE上，DafnyBench留出验证率66.1%→93.5%，SWE-Proof 56.3%→100%
- •仓库补丁问题解决率从59.6%升至72.5%，优于二元通过/失败奖励等对比训练信号
为什么重要：对做代码RL训练的人，这提供了一条不依赖测试覆盖率的奖励路径，直接指向可证明正确代码；验证器从推理期工具变成训练信号是关键转变。
以上深读由 AI 依据标题/摘要/正文节选生成，仅供参考；事实以原文为准。
AI 处理过程展开/收起
相关推荐
谷歌 Gemini 4 Carbon 全面超越 Opus 5.5，首发 Token 半价
AI 摘要谷歌发布 Gemini 4 Carbon，宣称在多项能力上全面超越 Opus 5.5，并推出首发 Token 半价优惠。该模型可连续数日修复 Bug，且具备免疫提示词注入的安全特性，加剧头部大模型竞争。
谷歌发布 Gemini 4 Carbon，主打网络安全能力跃升
AI 摘要谷歌推出前沿模型 Gemini 4 Carbon，在编程、智能体任务和网络安全方面显著提升，登顶 Artificial Analysis 智能指数，领先 Claude Opus 5.5 与 GPT-6 Astra。该模型目前仅向部分网络安全防御公司开放，定价与 Argon 相同，为每百万输入 token 2 美元、输出 10 美元。
谷歌发布 Gemini 4，API 限时半价
AI 摘要谷歌正式发布 Gemini 4，被视为重回大模型第一梯队的关键动作，同时推出 API 限时半价优惠。该发布对模型竞争格局与开发者成本结构均有直接影响。
谷歌 Meta 发布前沿模型，AI 竞赛重启
AI 摘要谷歌发布 Gemini 4 Argon，Meta 推出新前沿模型，两家公司声称可与 OpenAI 和 Anthropic 的旗舰模型匹敌。谷歌以激进定价策略切入市场，入门期价格比竞争对手低至80%。AI 前沿竞争格局重新洗牌。