用Ada/SPARK框架验证大模型生成的代码，提升可信度。
Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK
- 用大模型自动生成Ada/SPARK注解，支持形式化验证。
- GPT-4o在50.7%的测试案例中正确生成注解。
- 适合关注代码可靠性与形式化验证的研究者。
大型语言模型（LLMs）展现出强大的代码生成能力，但其生成代码的正确性无法保证。本文探讨了使用形式化软件验证（特别是Ada语言的SPARK框架）确保大模型生成代码可靠性的可行性。提出Marmaragan工具，利用大模型为现有程序生成SPARK注解，从而支持形式化验证。该工具在一组精选的SPARK程序上进行基准测试，通过有选择地移除注解来评估特定能力。实验结果显示，GPT-4o在基准测试中对50.7%的案例生成了正确的注解。这一结果为未来结合大模型与形式化验证的可靠性研究奠定了基础。
原文摘要 · Abstract (English)
Large language models (LLMs) have demonstrated remarkable code generation capabilities, but the correctness of the generated code cannot be inherently trusted. This paper explores the feasibility of using formal software verification, specifically the SPARK framework for Ada, to ensure the reliability of LLM-generated code. We present Marmaragan, a tool that leverages an LLM in order to generate SPARK annotations for existing programs, enabling formal verification of the code. The tool is benchmarked on a curated set of SPARK programs, with annotations selectively removed to test specific capabilities. The performance of Marmaragan with GPT-4o on the benchmark is promising, with correct annotations having been generated for 50.7% of the benchmark cases. The results establish a foundation for future work on combining the power of LLMs with the reliability of formal software verification.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。