用严谨工具从不可靠大模型中提取正确代码注释。
Next Steps in LLM-Supported Java Verification
- 用验证工具反向检验大模型生成的代码规范
- 在无标注数据下实现高准确率规范提取
- 适合关注代码安全与自动化验证的研究者
近期研究表明，大型语言模型（LLMs）不仅适用于代码生成，还能生成基于注释的代码规格说明。扩展这些方法有望为大规模软件系统推导出可证明的正确性保证。与其他 LLM 任务相比，演绎验证的应用领域具有显著优势：提供严格的工具来验证 LLM 生成的解决方案。本文报告了初步成果，展示如何利用这一严格工具集，从不可靠的 LLM 代理中可靠地获取正确的规范注释。
原文摘要 · Abstract (English)
Recent work has shown that Large Language Models (LLMs) are not only a suitable tool for code generation but also capable of generating annotation-based code specifications. Scaling these methodologies may allow us to deduce provable correctness guarantees for large-scale software systems. In comparison to other LLM tasks, the application field of deductive verification has the notable advantage of providing a rigorous toolset to check LLM-generated solutions. This short paper provides early results on how this rigorous toolset can be used to reliably elicit correct specification annotations from an unreliable LLM oracle.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。