Propose, Solve, Verify: Self-Play Through Formal Verification

📄 arXiv: 2512.18160v1 📥 PDF

作者: Alex Wilf, Pranjal Aggarwal, Bryan Parno, Daniel Fried, Louis-Philippe Morency, Paul Pu Liang, Sean Welleck

分类: cs.AI

发布日期: 2025-12-20

💡 一句话要点

提出PSV框架，通过形式化验证的自博弈提升代码生成能力

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 代码生成 自博弈 形式化验证 专家迭代 程序合成

📋 核心要点

  1. 现有代码生成模型依赖单元测试作为奖励信号，但单元测试脆弱且易于误差传播，限制了自博弈训练的效果。
  2. PSV框架利用形式化验证提供可靠的正确性信号，通过自博弈训练proposer生成难题，并训练solver解决这些难题。
  3. 实验结果表明，PSV-Verus在代码生成任务上显著优于现有方法，pass@1指标提升高达9.6倍，验证了该方法的有效性。

📝 摘要（中文）

本文研究了在验证代码生成环境中，利用形式化验证提供可靠的正确性信号进行自博弈训练。提出了Propose, Solve, Verify (PSV)框架，该框架利用形式化验证信号创建一个能够生成具有挑战性的合成问题的proposer，以及一个通过专家迭代训练的solver。使用PSV训练的PSV-Verus在三个基准测试中，pass@1指标相比于仅推理和专家迭代的基线方法，提升高达9.6倍。实验表明，性能随生成问题数量和训练迭代次数的增加而提升，并且通过消融实验确定了形式化验证和难度感知的proposal是成功自博弈的关键要素。

🔬 方法详解

问题定义：论文旨在解决代码生成模型在自博弈训练中，由于奖励信号（通常是单元测试）不可靠而导致性能提升受限的问题。现有方法依赖的单元测试容易出错，导致误差累积，使得模型难以有效地从自博弈中学习。

核心思路：论文的核心思路是利用形式化验证来提供可靠的正确性信号，从而克服单元测试的局限性。通过形式化验证，可以准确判断生成的代码是否满足给定的规范，从而为自博弈训练提供更准确的奖励。

技术框架：PSV框架包含三个主要模块：Propose, Solve, Verify。Propose模块负责生成具有挑战性的代码生成问题；Solve模块负责解决Propose模块生成的问题；Verify模块使用形式化验证来判断Solve模块生成的代码是否正确。整个流程通过自博弈的方式迭代进行，Propose模块根据Solve模块的性能不断调整生成问题的难度，Solve模块则不断学习解决Propose模块生成的问题。

关键创新：最重要的技术创新点在于将形式化验证引入到代码生成模型的自博弈训练中。与传统的基于单元测试的奖励信号相比，形式化验证提供了更准确、更可靠的正确性判断，从而避免了误差累积的问题。此外，难度感知的proposal机制也是一个重要的创新，它使得proposer能够生成更具挑战性的问题，从而促进solver的学习。

关键设计：PSV框架的关键设计包括：(1) Propose模块如何生成具有挑战性的问题，例如，可以通过调整问题生成的难度系数来实现；(2) Solve模块如何利用专家迭代进行训练，例如，可以使用强化学习算法来优化solver的策略；(3) Verify模块如何高效地进行形式化验证，例如，可以使用现有的SMT求解器或模型检查器来实现。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，PSV-Verus在三个代码生成基准测试中取得了显著的性能提升，pass@1指标相比于仅推理和专家迭代的基线方法，提升高达9.6倍。实验还验证了形式化验证和难度感知的proposal是成功自博弈的关键要素，并且性能随着生成问题数量和训练迭代次数的增加而提升。

🎯 应用场景

该研究成果可应用于自动化代码生成、程序修复、软件测试等领域。通过形式化验证和自博弈训练，可以生成更可靠、更高效的代码，提高软件开发的效率和质量。未来，该方法有望扩展到更复杂的代码生成任务，例如生成具有特定功能的应用程序或操作系统组件。

📄 摘要（原文）

Training models through self-play alone (without any human data) has been a longstanding goal in AI, but its effectiveness for training large language models remains unclear, particularly in code generation where rewards based on unit tests are brittle and prone to error propagation. We study self-play in the verified code generation setting, where formal verification provides reliable correctness signals. We introduce Propose, Solve, Verify (PSV) a simple self-play framework where formal verification signals are used to create a proposer capable of generating challenging synthetic problems and a solver trained via expert iteration. We use PSV to train PSV-Verus, which across three benchmarks improves pass@1 by up to 9.6x over inference-only and expert-iteration baselines. We show that performance scales with the number of generated questions and training iterations, and through ablations identify formal verification and difficulty-aware proposal as essential ingredients for successful self-play.