SpecRL：强化学习，为形式化规范综合提供基于测试的完整性奖励

规范综合要求模型为现有程序生成规范和辅助注释。在现代软件验证项目中，规范的准确性至关重要。规范是方法行为的抽象，调用者根据被调用者的规范而不是其实现进行验证。因此，被调用者的规范会极大地影响调用者可以证明的属性。然而，验证者的反馈本身对于规范综合来说是一个很差的训练信号：验证可以证明规范对于实现来说是合理的，但它不能判断规范是否太弱。我们提出了 SpecRL，这是一个强化学习框架，它为 Dafny 中的规范综合添加了经验完整性信号。 SpecRL 从实现不可能的输入输出对构建负面测试或 Spectests，弱规范（例如确保 true ）仍可能承认。在训练过程中，SpecRL 根据规范拒绝的 Spectest 的比例来奖励经过验证的候选者，从而根据他们排除的不可能实现的行为的数量对这些候选者进行排名。在分布外 DafnyComp-Spec 基准测试中，7B SpecRL 模型比监督 微调 的验证成功率和完整性分别提高了 49.96% 和 26.46%。这些相对增益表明，细粒度的光谱测试反馈提高了可验证性和规范准确性。