Event-B Agent：面向形式模型合成与修复的LLM Agent
软件工程
2026-05-19 v1
摘要
通过形式化方法构建正确的软件是软件工程的一个长期目标，因为它确保在设计和开发期间可靠性，而不是在部署后。形式化方法通过使系统行为和需求以数学形式表达，从而通过形式验证(包括定理证明和模型检查)保证正确性。然而，陡峭的学习曲线和对数学专业知识的需求阻碍了形式化方法的广泛采用。大型语言模型(LLM)最近在通过自动形式化方面显示出潜力。然而，现有的LLM方法大多局限于孤立任务，如在没有形式化证明的情况下的定理证明或模型合成但验证不足。虽然这些努力固有其价值，但它们并未充分发挥出更全面框架的潜力，在这种框架中，模型和证明可以共同演化，这一过程贴近实际的开发实践。为此，我们提出Event-B Agent，一种受软件设计交叉过程启发的新型框架。给定自然语言需求，Event-B Agent构建初始模型，并通过形式验证反馈迭代地修复和细化模型。细化简化证明求解，模型和证明的修复确保每个细化步骤的可靠性。这两个组件相互强化，以逐步提高模型质量。跨越不同复杂度的系统进行评估显示，Event-B Agent在端到端形式模型合成和修复方面显著优于基线方法，同时保持合理的效率。这些结果表明，Event-B Agent是正确构造形式模型合成和修复的有前景的一步。
引用
@article{arxiv.2605.17475,
title = {Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair},
author = {Hongshu Wang and Xinyue Zuo and Yuhan Sun and Qin Li and Yamine Ait Ameur and Jin Song Dong},
journal= {arXiv preprint arXiv:2605.17475},
year = {2026}
}
备注
accepted by FSE 2026