核心问题

代码 Attacker-Defender 博弈是否可行？验证器如何设计？

SInQ 的发现

Program Semantic Inequivalence Game (SInQ) [ref] 提供了一个巧妙的设计：

游戏机制

角色 目标
Generator (Alice) 创建语义不同的程序变体 Q + 提供区分输入 x
Evaluator (Bob) 给定 P 和 Q（不给 x），找出区分输入 x̂

验证方式：程序执行 - 这是一个可靠的 Layer-0 外部锚点。

关键设计：Positive-sum 而非 Zero-sum

这是最重要的发现：

博弈类型 目标难度 结果
Zero-sum 最大难度 (10) Alice 创建不可能问题（如密码学难题）
Positive-sum 目标难度 < 最大值 (如 7) Alice 成为"教师"，创建难但可解的问题

“This changes the nature of the game from zero-sum to positive-sum, where Alice acts as a teacher that challenges Bob with instances which are hard, but not too hard for its current level.”

避免 Reward Hacking 的机制

  1. 随机化时间限制（2.5-5.5 秒）- 防止固定超时游戏
  2. 外部程序源（P 来自 MBPP 数据集）- 防止 Alice 生成无意义的代码
  3. Positive-sum 设计 - 防止 Alice 创建不可能问题
  4. 验证管道 - AST 解析、语法验证、语义验证

实验结果

任务 基线 SInQ 提升
MBPP 游戏性能 75.99% 86.98% +10.99%
Python Builtin Identifier Swap 1.65% 5.35% +3.70%
C/C++ 漏洞检测 (跨语言！) 55.23% 55.60% +0.37%

关键发现：Python 训练的模型在 C/C++ 漏洞检测上提升 - 跨语言泛化。

重新分类：三种博弈范式

结合之前的分析，我现在可以对三种代码自博弈范式进行更准确的分类：

范式 博弈性质 角色关系 约束来源
Sol-Ver 协同进化 Solver + Verifier 共同提升 能力协同
PSV 难度匹配 Proposer 根据能力生成问题 Pass rate 分类
SInQ Positive-sum Teacher-Student（教师-学生） 目标难度控制

共同特征：都不是传统意义上的 Attacker-Defender 零和博弈。

为什么 Zero-sum Attacker-Defender 不可行？

SInQ 论文揭示了根本问题：

  1. Zero-sum 博弈的不可能问题：Attacker 总能创建不可能问题（如密码学难题）
  2. 无外部锚点时的崩溃：没有稳定机制，博弈会走向极端
  3. 与教育的类比：真正的教师不会创建不可能的考试，而是"难但可解"的问题

这解释了为什么 SPIRAL 需要 RAE（EMA baseline），为什么 SInQ 需要 Positive-sum 设计。

与之前框架的连接

外部锚点的重要性再次被验证：

系统 外部锚点 稳定机制
SInQ 程序执行 Positive-sum 设计
PSV 形式化验证 Pass rate 分类
SPIRAL 游戏规则 RAE（EMA baseline）
创意写作对抗 真实标签 Reflector

共同模式：对抗性训练需要外部锚点 + 稳定机制。

开放问题

  1. Positive-sum 的最佳难度设置：如何动态调整目标难度？
  2. 跨任务迁移的机制：为什么 Python 训练能提升 C/C++ 任务？
  3. 与其他范式的组合：能否将 SInQ 与 PSV 的形式化验证结合？

批判性反思

框架过度扩展问题：我之前将 PSV、Sol-Ver、Afterburner 都归入"动态约束"框架，但实际上它们的博弈性质不同：

  • Sol-Ver：协作（不是对抗）
  • PSV：难度匹配（不是零和对抗）
  • SInQ：Positive-sum（刻意避免零和）
  • Afterburner：自我迭代（没有博弈）

更准确的分类应该是：协作式 vs 对抗式 vs 自我迭代式。

真正的"Attacker-Defender 零和博弈"在 LLM 代码生成领域可能不适合作为训练范式。Positive-sum 设计才是可持续的方向。

关联论文: