使用多模态验证器进行认证程序合成

认证程序合成（又称验证编码）是根据自然语言描述自动生成程序、其形式规范以及机器可检查的对齐证明的过程。有两个挑战使验证变得困难。首先，从自然语言合成的规范通常要么太弱而没有意义，要么太强而无法实现，而现有的方法缺乏系统的手段来检测这些缺陷。其次，程序验证器的格局是支离破碎的：每个工具都支持特定的推理模式——自动主动（例如，Dafny、Verus）或交互式（例如，Coq、Lean）——在自动化和表现力之间有自己的权衡。这迫使每种综合方法都针对单一验证范例进行定制，从而限制了它可以有效处理的任务类别。我们通过围绕多模式验证器构建经过认证的综合工作流程来克服这两个挑战，多模式验证器是一种将动态验证、自动证明和交互式证明脚本结合在一个基础框架中的单一工具。我们在 LeetProof 中实现了这个想法，这是一个基于 Velvet 构建的代理管道，Velvet 是嵌入在 Lean 中的多模式验证器。多模态使 LeetProof 能够在合成任何代码之前通过基于属性的随机测试来验证生成的规范，将合成任务分解为由验证条件引导的子问题，并将剩余证明义务委托给专门针对精益的前沿 AI 证明者。我们根据先前认证合成工作得出的基准来评估 LeetProof。我们的规范验证发现了现有参考基准中的缺陷，并且 LeetProof 的分阶段管道在相同预算下比单模式基准实现了显着更高的完全认证解决方案率 - 在两个前沿 LLM 后端上始终如一。