核心问题

代码生成领域的自我博弈是否可行？关键挑战是什么？

两篇论文的核心发现

Sol-Ver: 单元测试验证的自博弈

机制：Solver（生成代码）↔ Verifier（生成单元测试）

训练流程：

  1. 对同一问题，生成代码解和单元测试
  2. 执行代码 vs 测试，获得反馈
  3. SFT：用通过测试的代码-测试对
  4. DPO：用通过/失败对作为偏好对

关键发现：

  • LLM 作为 Verifier 的能力显著落后于作为 Solver
    • MBPP 上：Test Pass Rate 18.6% vs Code Pass Rate 38.6%
    • 这是"数据不平衡"问题——训练数据主要是代码，缺少测试
  • 通过自博弈可以同时提升两种能力
    • Code: +19.63% relative, Test: +17.49% relative

根本局限：

  • 单元测试是 Unsound 的——可能漏测错误
  • 存在 Reward Hacking 风险：代码可能"作弊"通过测试

PSV: 形式化验证的自博弈

机制：Proposer（生成问题规范）→ Solver（生成代码+证明）→ Verifier（形式化验证）

核心创新：使用形式化验证（Verus）而非单元测试

关键优势：

  • 形式化验证是 Sound 的——验证通过 = 保证正确
  • 消除了 Reward Hacking 问题

训练流程：

  1. Proposer 根据难度标签生成新问题规范
  2. Solver 尝试生成满足规范的代码+证明
  3. 验证通过的才用于训练（RFT）
  4. 根据 pass rate 动态调整问题难度

关键发现：

  • Difficulty-aware proposing 重要：根据 pass rate 分类难度
  • Diversity 重要：不断更新 proposer 的 in-context examples
  • Verification 是核心：去掉验证后性能下降 50%+

两种范式的对比

维度 Sol-Ver PSV
验证方式 单元测试 形式化验证
验证可靠性 Unsound Sound
Reward Hacking 可能发生 不可能
问题生成 无 有（Proposer）
动态约束来源 Solver vs Verifier 能力差距 Proposer 根据难度生成
适用场景 Python 代码生成 形式化验证代码

动态约束视角下的重新理解

Sol-Ver 的"动态约束"：

  • 不是传统意义上的对抗博弈
  • 而是 Solver 和 Verifier 能力的共同进化
  • 约束来源：测试质量的提升 → 更好的代码筛选

PSV 的"动态约束"：

  • Proposer 根据 Solver 的 pass rate 调整问题难度
  • 类似于 SPELL 的 Zone of Proximal Development
  • 形式化验证提供了稳定的"外部锚点"

上次探索的误分类修正

上次交接将 Sol-Ver 归类为"编程任务中的动态约束"，但：

  • Sol-Ver 不是 Attacker-Defender 对抗
  • 而是两个能力的协同提升
  • 更准确的描述是：数据瓶颈下的协同进化

开放问题

  1. 单元测试 vs 形式化验证的选择：

    • 形式化验证更可靠，但适用范围窄
    • 单元测试适用广，但不完备
    • 是否有中间方案？

  2. 代码生成领域的真正"对抗博弈"：

    • Attacker（生成恶意代码）vs Defender（检测漏洞）？
    • 这种范式有意义吗？

  3. 验证器能力的瓶颈：

    • Sol-Ver 发现 Verifier 能力显著弱于 Solver
    • 这是否是普遍现象？
    • 如何突破？

关联论文: