本研究提出了一种基于语言到代码生成的方法，利用预先训练好的代码语言模型的采样程序生成，再利用后验验证器对生成的程序进行验证，对程序进行重新排序，从而提高最终程序的正确性，实验结果表明该方法在多个领域取得了最优的生成效果。

Feb, 2023

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

Oct, 2023

该研究通过定义 Isabelle/HOL 中的 VHDL 语言的形式模型，并构建 VHDL 仿真器，实现了对 VHDL 语言进行形式推理的目的。

Feb, 2022

本文研究了自动形式化的过程，并发现大型语言模型可用于将自然语言的数学问题翻译为 Isabelle/HOL 的形式化说明，证明了这种方法的实用性，并通过训练预先介绍的神经定理证明器使改进了 MiniF2F 定理证明基准的证明率从 29.6% 提高到 35.2%。

May, 2022

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

Mar, 2024

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

Jun, 2024

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

Nov, 2023

人工智能在数学领域发现引起了广泛关注，这项研究探索了大型语言模型与定理证明系统的结合，旨在提供一种从研究论文中提取和形式化数学定理的自动化工具。

Oct, 2023

我们使用交互式定理证明器 Isabelle/HOL 对一种近似策略迭代算法在因子化马尔可夫决策过程上进行了形式验证。接着，我们展示了如何将形式化的算法细化为可执行的验证实现。所开发的实现方案经过了基准问题的评估，表明其实用性。作为细化的一部分，我们开发了经过验证的软件以认证线性规划解法。该算法基于丰富的形式化数学库，并推动了交互式定理证明器的现有方法的极限。我们讨论了验证项目的过程以及为形式验证所需的算法修改。

Jun, 2024

本研究论文介绍了一种名为 FOLK（First-Order-Logic-Guided Knowledge-Grounded Reasoning）的方法，用大型语言模型（LLMs）进行复杂声明的验证和解释生成，同时不需要基于人工标注的证据。该方法通过将声明转化为由谓词组成的一阶逻辑子句，每个谓词对应需验证的一个子声明，并利用一组知识基础的问答对进行一阶逻辑引导的推理，从而做出真实性预测并生成解释以说明其决策过程，使模型高度解释性。实验结果表明，FOLK 在涵盖各种声明验证挑战的三个数据集上优于强基线模型。

Oct, 2023