arXiv:2502.01573v1 类型: cross 摘要: 最近的工作表明，大型语言模型（LLMs）不仅可以作为代码生成的合适工具，还可以生成基于注释的代码规范。这些方法的扩展可能允许我们为大规模软件系统推导出可证明的正确性保证。与其它LLM任务相比，演绎验证的应用领域的一个显著优势是可以提供一套严格的工具集来检查LLM生成的解决方案。这篇简短的文章提供了关于如何使用这套严格的工具集可靠地从不可靠的LLM先知中引出正确的规范注释的早期结果。