FM-Agent：基于LLM的Hoare-style推理扩展形式方法规模化
软件工程
2026-04-14 v1 人工智能
摘要
LLM辅助软件开发日益普及，可以生成大型系统，如编译器。因此，加强生成代码的正确性至关重要。然而，由于代码复杂性，自动化推理对于大型系统仍然具有挑战性。Hoare逻辑提供了一种方法，通过将大型系统分解为更小的组件并单独推理每个组件(即组合推理)。然而，现有工作仍难以扩展，因为Hoare逻辑需要为每个函数编写形式化规范，这增加了巨大的人力负担。当代码由LLM生成时，开发人员因缺乏对每个函数预期行为的深入理解而问题更为严重。本文提出了FM-Agent，第一个实现大型系统自动化组合推理的框架。利用LLM，FM-Agent引入一种自上而下的范例，自动生成函数级别的规范。具体而言，FM-Agent从调用函数的预期行为中推导出该函数的规范，即使实现存在错误，所生成的规范也能反映开发人员对该函数意图的理解。开发人员的意图通常以自然语言表达，而现有验证程序仅支持公式。因此，FM-Agent将Hoare-style推理扩展到针对自然语言规范来推理函数。最后，为了确认bug的存在并解释bug的原因，FM-Agent自动生成测试用例以触发潜在的bug。在我们的评估中，FM-Agent成功地在2天内推理了大型系统，每个系统规模可达143k LoC。这些系统已经由开发人员测试，但FM-Agent仍发现了522个新发现的bug。这些bug可能导致严重后果，包括系统崩溃和错误的执行结果。
引用
@article{arxiv.2604.11556,
title = {FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning},
author = {Haoran Ding and Zhaoguo Wang and Haibo Chen},
journal= {arXiv preprint arXiv:2604.11556},
year = {2026}
}