使用 LLM4nl2post 将非正式自然语言转化为形式化方法的后置条件，并通过验证度量在质量和生成的后置条件的可区分性方面进行比较。结果显示，这些后置条件通常是正确的且能够区分错误的代码，并且通过 LLMs 进行 LLM4nl2post 有潜力在实践中发挥重要作用，在 Defects4J 中成功捕获了 70 个真实世界历史 BUG。

Oct, 2023

提出 LLM4PLC 的用户引导迭代流程，通过用户反馈和外部验证工具来改善大型语言模型（LLM）生成的代码的可验证性，提高成功生成的比例并提高代码质量。

Jan, 2024

通过结合 LLMs 的代码理解能力和自动推理程序，我们提出了一种通用方法论来进行自动程序验证，通过一组导出规则进行形式化描述并证明其合理性，从而实现了在一系列合成和竞争基准测试中的实际改进。

Oct, 2023

我们提出了一种称为变质提示测试的新颖解决方案，用于解决由大型语言模型生成的代码质量和正确性所引发的挑战，并在 HumanEval 评估中显示，该方法能够检测到由 GPT-4 生成的错误程序的 75％，误报率为 8.6％。

Jun, 2024

利用大型语言模型（LLMs）迭代改进和修复源代码已成为一种流行的方法，该方法被称为细化，可生成过于复杂无法一次构建的程序。我们发现细化代码暴露了探索与利用的权衡：通过改进通过测试用例的程序进行利用，或通过改进较少考虑的程序进行探索。我们将其视为一种获取臂的赌博机问题，并用汤普森采样解决。得到的基于 LLM 的程序合成算法具有广泛的适用性：在循环不变量合成、视觉推理谜题和竞赛编程问题中，我们发现我们的新方法可以在更少的语言模型调用下解决更多问题。

May, 2024

基于大型语言模型（LLMs）和静态分析相结合，开发了一个基于 Rust 的形式验证框架 Verus 的原型。通过将验证任务分解为多个较小的任务，迭代地查询 GPT-4，并将其输出与轻量级静态分析相结合，这个原型显著减少了编写入门级证明代码的人力工作。

Nov, 2023

探索最新的大型语言模型在代码生成方面的能力，调查提示和微调方法，并分析大型语言模型生成测试的结果。

Oct, 2023

本文探讨了使用 Large Language Models 进行程序合成时，实现 Synthesize，Execute，Debug 方法的方法，包括替换或修复故障程序，以及不同基于模板和基于模型的提示生成技术，取得了比传统方法更好的表现。

Apr, 2023

大型语言模型 (LLMs) 具有彻底改变自动形式化的潜力。引入数学编程语言 Lean4 为评估 LLMs 的自动形式化能力提供了前所未有的机会。本文介绍了一种专为 Lean4 设计的新型评估基准，将其应用于测试包括 GPT-3.5、GPT-4 和 Gemini Pro 在内的最先进的 LLMs 的能力。我们全面的分析发现，尽管最近有所进展，这些 LLMs 在自动形式化方面仍存在局限性，尤其是在更复杂的数学领域。这些发现强调了需要进一步发展 LLMs，以充分发挥它们在科学研究和开发中的潜力。本研究不仅为当前的 LLM 能力设立了基准，还为自动形式化的未来增强奠定了基础。

Jun, 2024

本研究探讨了将大型语言模型（LLMs）如 GPT-3.5 和 GPT-4 整合到本体修正过程中，特别关注 OntoClean 方法论。研究通过采用两种提示策略的 LLMs，证明了在标注过程中可以获得高准确性，并提出了开发插件软件以促进本体工具整合的潜力。

Mar, 2024