基于模型的证明草图指导形式化模型构建

形式化建模为系统的正确性提供了强有力的保证，但开发和修复形式化模型仍然是劳动密集型的，并且需要大量的逻辑和形式推理方面的专业知识。最近基于 LLM 的自动形式化代理试图通过生成候选形式模型并使用形式工具的反馈对其进行修改来减轻这种负担。然而，现有的方法遵循生成和修复范例，其中修复是由生成模型的验证失败驱动的，因此在很大程度上取决于反馈的粒度和大语言模型的修复能力。因此，针对一个验证级别的修复可能会使另一级别的属性无效，这需要对整套事件防护进行推理。为了解决这些限制，我们提出了证明草图引导的形式模型综合（ProGS），这是一种以基于模型的证明草图为中心的自动形式化方法。基于模型的证明草图将目标形式系统的证明结构表示为树。内部节点捕获案例分割和归纳推理步骤，而叶节点对应于实现各个子目标的具体状态转换事件。 ProGS 使用 LLM 生成和修复这些草图，并将验证失败映射回特定节点和子树，为迭代修复提供结构化指导。我们对 27 个形式系统基准的评估表明，ProGS 在句法有效性、演绎可验证性和行为正确性方面比最先进的代理形式建模方法有所改进，证明了围绕分层证明草图组织形式模型构建的好处。