[AI]《Propose, Solve, Verify: Self-Play Through Formal Verification》A Wilf, P Aggarwal, B Parno, D Fried... [CMU] (2025) AI自我进化的征途上，一直存在一个幽灵：如果反馈信号不准确，模型会在自我博弈中逐渐跑偏，最终陷入“幻觉”的死循环。在代码生成领域，这个挑战尤为突出。传统的单元测试就像是抽查，即便通过了所有测试用例，代码依然可能存在逻辑漏洞。这种“奖励作弊”现象限制了大规模自我博弈的可能性。本文为我们指明了方向：利用形式化验证（Formal Verification）作为AI进化的“真理锚点”。以下是该研究的核心洞察与深度解析：1. 形式化验证：从“看起来对”到“证明是对”传统的代码评估依赖于有限的测试用例，而形式化验证则要求模型同时生成代码和数学证明。通过Verus等工具，验证器可以在数学层面保证代码在所有可能的输入下都符合规范。这种“绝对正确”的信号，为自我博弈提供了坚实的基础，彻底杜绝了错误信号的传播。2. PSV框架：提问、解决、验证的闭环论文提出的PSV框架由三个核心环节组成：- 提问（Propose）：提问者模型根据当前的解决能力，生成具有挑战性的形式化规范（Specifications）。- 解决（Solve）：解决者模型尝试编写能够通过验证的代码和证明。- 验证（Verify）：利用形式化验证器给出二进制的反馈信号。通过这种方式，系统可以自主构建一套从易到难的“进化阶梯”。3. 难度感知的课程学习PSV不仅仅是随机出题。研究引入了“难度感知”机制：提问者会根据解决者的历史通过率，动态调整新题目的难度。如果通过率太高，就增加复杂度；如果模型束手无策，则退回基础逻辑。这种类似人类“区带学习”的模式，极大提升了训练效率。4. 令人惊叹的性能飞跃实验结果显示，基于PSV训练出的PSV-Verus模型，在多个基准测试中表现惊人。在某些任务上，其性能比仅在人类数据上微调的模型提升了高达9.6倍。更重要的是，这种提升随着迭代次数和题目数量的增加展现出了清晰的扩展性（Scaling）。5. 摆脱人类数据的依赖这项研究最深刻的启示在于：AI的进化上限可能不再受限于人类积累的存量数据。只要我们能定义清楚“规则”和“验证机制”，模型就能在自创的沙盒中通过无限次的自我博弈，探索出人类尚未触及的逻辑深度。深度思考与金句：- 真正的智能不仅在于给出答案，更在于拥有一个不可撼动的真理准则。- 形式化验证将代码从概率性的艺术变成了确定性的科学。- 当AI学会了自我审视，进化的速度将不再取决于人类教了什么，而取决于逻辑边界在哪里。- 自我博弈的本质，是模型在真理的反馈下，不断与过去的平庸进行决裂。这项工作不仅是代码生成技术的进步，更是通往通用人工智能（AGI）推理能力演进的重要里程碑。原文链接：arxiv.org/abs/2512.18160
