通过评估 OpenAI 的 GPT-4 等大型语言模型与传统的静态代码分析器（如 Snyk 和 Fortify）在检测软件漏洞方面的能力，我们发现 GPT-4 能够识别出大约四倍于其他模型的漏洞，并提供可行的修复方案，同时显示出较低的误报率。未来研究应当探索系统级漏洞，并整合多个静态代码分析器，以获得对大型语言模型潜力的全面视角。

Aug, 2023

自动事实核查（使用机器学习来验证主张）已经变得至关重要，因为虚假信息已经超出了人类事实核查的能力范围。大型语言模型（LLMs），如 GPT-4，越来越受人们的信任，可以验证信息并撰写学术论文、诉讼文件和新闻文章，强调了它们在分辨真假和能够验证其输出的重要性。在这里，我们通过让 LLM 代理人表达查询、检索上下文数据和做出决策来评估 LLMs 在事实核查中的使用。重要的是，在我们的框架中，代理人解释他们的推理并引用检索到的相关来源。我们的结果显示，在配备上下文信息的情况下，LLMs 表现出更强大的能力。GPT-4 优于 GPT-3，但准确性取决于查询语言和主张的真实性。虽然 LLMs 在事实核查方面显示出前景，但仍需要谨慎使用，因为准确性不一致。我们的调研呼吁进一步研究，以更深入地了解代理人何时成功以及何时失败。

Oct, 2023

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

Jan, 2024

通过自动生成验证的形式化 Isabelle 代码，我们的方法能够自动排除具有内在一致性问题或与形式化问题陈述不一致的解，并在多个数据集和模型大小上比以前最佳方法 — 普通多数投票 — 提高了 12% 以上的准确性。

Mar, 2024

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

Oct, 2023

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

Oct, 2023

使用 GPT4、Coq 和 Coqhammer 实现的 LLM4PR 工具将正式程序细化技术与非正式 LLM 方法相结合，通过将规范转换为前置条件和后置条件，基于细化演算自动生成提示，并与 LLM 进行交互以生成代码，最后验证生成的代码是否符合细化演算的条件，从而确保代码的正确性。

Jun, 2024

通过在三个领域（24 点游戏，图着色，STRIPS 规划）对 GPT-4 的表现进行实证研究，我们观察到自我评估导致性能显著下降，而外部验证则带来显著性能提升；然而，评估内容对系统性能并不重要，事实上，简单地使用一个可信的验证器重新提问可以保持大部分优势。

Feb, 2024

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

Jun, 2024

基于大规模合成数据，使用 Lean 4 proof 数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高 LLMs 中的定理证明能力的潜力。

May, 2024