arXiv:2502.07728v1 Announce Type: cross 摘要：大型语言模型（LLMs）展示了令人瞩目的代码生成能力，但生成代码的正确性无法从根本上受到信任。本文探讨了使用形式软件验证，特别是Ada语言的SPARK框架，来确保LLM生成代码的可靠性的可行性。我们介绍了Marmaragan工具，该工具利用LLM为现有程序生成SPARK注释，从而实现代码的形式验证。该工具在一组精心策划的SPARK程序上进行了基准测试，并从基准中选择性地移除了注释以测试特定的功能。Marmaragan在基准测试中与GPT-4o结合使用的性能令人鼓舞，正确注释被生成了基准案例的50.7%。结果为未来结合LLM的强大功能与形式软件验证的可靠性奠定了基础。