面向后端系统的自动化形式化验证：融合大语言模型方法
软件工程
2025-06-16 v1 人工智能
摘要
软件测试在确保系统按预期运行方面发挥着关键作用。然而，现有自动化测试方法因测试局部性、缺乏通用可靠性以及对业务逻辑盲目等局限，难以匹配人类工程师的能力。本文提出一种新框架，利用函数式编程与类型系统将Scala后端代码转化为形式化Lean表示。我们的处理管道自动生成用于指定API和数据库操作意图行为的定理，并运用基于LLM的证明器进行验证。当定理被证明时，相应逻辑即被保证正确，无需进一步测试；若定理否定形式被证明，则确认存在缺陷；若上述两种情况均无法证明，则需人工介入。我们在真实后端系统上进行评估，发现该方法可形式化验证超过50%的测试需求，表明测试工程师的一半工作可被自动化。此外，基于仅2.19美元的平均API成本，LLM驱动的验证显著高于手动测试，具备通过并行执行实现的扩展潜力。这些结果表明，AI驱动的软件测试正朝着可扩展的方向发展，随着模型进步，将显著提升工程生产力。
引用
@article{arxiv.2506.10998,
title = {Towards Automated Formal Verification of Backend Systems with LLMs},
author = {Kangping Xu and Yifan Luo and Yang Yuan and Andrew Chi-Chih Yao},
journal= {arXiv preprint arXiv:2506.10998},
year = {2025}
}