EMNLPOct, 2023

为程序验证评级 LLM 生成的循环不变量

PDF
TL;DR利用大型语言模型合成归纳循环不变量是自动化程序验证的基础。本研究观察到，大型语言模型（如 gpt-3.5 或 gpt-4）能够在 0-shot 设置下为一类程序合成循环不变量，但需要多个样本来生成正确的不变量，这可能导致大量调用程序验证器以建立不变量。为解决这个问题，我们提出了一种对生成结果进行重新排名的方法，设计了一个能够根据问题定义区分正确的归纳不变量和错误尝试的排名器，该排名器被优化为对比排名器。实验结果表明，这种重新排名机制显著提高了正确不变量在生成的候选项中的排名，从而显著减少了对验证器的调用次数。
发现论文，激发创造
  • 利用大型语言模型发现归纳循环不变量

    本文通过使用大语言模型，探索了在自动程序验证中找到归纳循环不变量的新方法，并证明了其可以改进目前的技术水平。

    Nov, 2023

  • 在 Rust 中利用大型语言模型进行自动证明合成

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

    Nov, 2023

  • 基于大型语言模型的自然语言生成从逻辑形式的重新排序研究

    通过提出一种新颖的生成和重新排序的方法，本研究强调大型语言模型在自然语言生成中的出色能力，并解决了从逻辑形式（LFs）生成自然语言时遇到的一些问题，该方法能够提高生成输出的语义一致性和流畅性，经过多项实验验证了其有效性。

    Sep, 2023

  • 利用大型语言模型引导枚举式程序合成

    本文评估了预训练大型语言模型在解决正式综合基准测试中的能力，并提出了一种将语言模型与枚举综合算法相结合的新颖算法，结果显示该方法在性能上明显优于独立使用语言模型或枚举综合器，以及在 SyGuS 竞赛中取胜的工具。

    Mar, 2024

  • LLM-RankFusion：基于 LLM 的排名中内在不一致问题的缓解

    使用语言模型比较并排序排名的矛盾问题，我们提出了一种使用 LLM-RankFusion 的方法，它有效地减少了排序的不一致性，提高了排名质量。

    May, 2024

  • Rank-without-GPT: 基于开源大型语言模型构建独立的 GPT - 无关的列表排序器

    通过消除对 GPT 模型的依赖，本研究首次构建了有效的零阶科学可复现性的无需 GPT 依赖的排序器，能够在通行回收实验中表现出 13% 超越基于 GPT-3.5 的排序器，并达到了基于 GPT-4 构建的排序器的 97% 有效性。研究结果还显示，现有的点对点排序训练数据对于构建此类基于列表的排序器是不足够的，需要高质量的基于列表的排序数据，呼吁进一步建立人工标注的列表数据资源。

    Dec, 2023

  • 不要相信：验证 - 用自动形式化证明 LLM 定量推理的基础

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

    Mar, 2024

  • Lean4 中自动形式化的评估基准

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

    Jun, 2024

  • 通过学习细化搜索策略来学习查找证明和定理 - 循环不变式合成的案例

    我们提出了一种新的自动定理证明方法，其中使用 AlphaZero 风格智能体自我训练来改进表达为非确定性程序的通用高级专家策略，同时具有类似的教师代理机自我训练来生成适当相关性和难度的任务以供学习者解决，利用最小领域知识来解决合成训练数据不可用或难以合成的问题，具体举例来说，我们考虑了用于命令程序的循环不变量合成，并使用神经网络来改进教师和求解策略。

    May, 2022

  • 无需真实标准的大型语言模型排名

    大语言模型的评估和排名是一个重要的问题，本研究提出了一种新的方法，在没有任何参考数据的情况下，通过考虑三元组模型相互评估来排名这些模型，实验证明该方法可靠地恢复接近真实的排名，为实际使用提供了可行的低资源机制。

    Feb, 2024