BriefGPT - AI 论文速递 · 2025-02-11T00:00:00Z 在软件验证背景下验证LLM生成的代码与Ada/SPARK 💡 原文英文，约100词，阅读约需1分钟。 📝 内容提要 该研究提出了工具Marmaragan，利用大型语言模型为程序生成SPARK注释，以实现代码形式验证。实验结果显示其能正确生成50.7%的注释，为未来结合LLM与形式验证奠定基础。 🏷️ 标签 Marmaragan SPARK注释 ada llm spark 代码生成 大型语言模型 形式验证 阅读原文 生成长图 分享链接 已复制链接
