事件B代理：面向LLM形式模型合成和修复代理

构建通过构造正确的软件是软件工程的一个长期目标，因为它确保设计和开发期间而不是部署之后的可靠性。形式化方法通过用数学表达系统行为和需求来实现这一愿景，从而通过形式验证（包括定理证明和模型检查）保证正确性。然而，陡峭的学习曲线和对数学专业知识的需求阻碍了形式方法的广泛采用。 大语言模型 (LLM) 最近在通过自动形式化弥合这一差距方面表现出了希望。然而，现有的基于 LLM 的方法很大程度上仅限于孤立的任务，例如没有形式化的定理证明或验证不足的模型合成。虽然这些努力很有价值，但并没有充分利用模型和证明共同发展的更全面框架的潜力，这一过程密切反映了现实世界的开发实践。为了解决这一差距，我们提出了 Event-B Agent，这是一种受软件设计交错性质启发的新颖框架。根据自然语言要求，Event-B Agent 构建初始模型，并使用形式验证反馈迭代修复和完善它。细化简化了证明的发布，而模型和证明的修复则确保了每个细化步骤的健全性。这两个组件相辅相成，逐步提高模型质量。对不同复杂度的系统进行的评估表明，Event-B Agent 在端到端形式模型合成和修复方面远远优于基线，同时保持了合理的效率。这些结果表明，Event-B Agent 是朝着构建正确形式模型合成和修复迈出的有希望的一步。