用形式化验证驱动自对弈，提升代码生成模型性能。
Propose, Solve, Verify: Self-Play Through Formal Verification
- 通过形式化验证提供可靠反馈，构建生成与求解的自对弈框架。
- 在三个基准上，pass@1最高提升9.6倍，优于纯推理与专家迭代方法。
- 适合追求高可靠性代码生成的研究者或工业级AI应用团队。
仅通过自对弈训练模型（无需人类数据）是人工智能长期目标，但在代码生成领域，基于单元测试的奖励机制脆弱且易引发错误传播。本文研究在形式化验证保障下的自对弈代码生成，提出Propose, Solve, Verify（PSV）框架：利用形式化验证信号构建可生成挑战性合成问题的提议者，以及通过专家迭代训练的求解器。使用PSV训练的PSV-Verus模型，在三个基准测试中，pass@1最高提升9.6倍，优于仅推理和专家迭代基线。实验表明性能随生成问题数量与训练轮次增长，消融分析确认形式化验证与难度感知提议为成功自对弈的关键要素。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。