提出了一种名为 ALGO 的框架，该框架使用 LLM 生成的神谕来引导算法程序的创建和验证。实验表明，与 Codex 和 CodeT 等现有领先模型相比，在处理未知问题时，使用 ALGO 可获得 8x 和 2.6x 的更好的一次提交通过率。

May, 2023

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

Oct, 2023

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

Feb, 2023

本文提出一种基于自监督的零次学习框架 ——Self-Checker，旨在解决基于特定数据集进行事实检查的计算负担问题。实验结果表明，该框架在低资源环境下能够快速且高效地构建事实检查系统，其能力仍有待进一步提高。

May, 2023

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

Oct, 2023

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

Jan, 2024

提出了一种名为自验证的方法，该方法使用推理链的结论作为条件建立新的样本，并要求大型语言模型重新预测原始条件，从而降低了多任务精度误差。经过大量实验验证，此方法可以使大型语言模型避免出现不正确的推理链干扰，并实现具有竞争力的推理性能，可用于算术和逻辑推理数据集的有限次学习。

Dec, 2022

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

Feb, 2024

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

Jun, 2024

几乎不存在自我评估的大型语言模型能够成功地在迭代模式下验证或自我批评其候选解决方案的推理问题中。该研究评估了一种利用大型语言模型进行计划生成和验证的计划系统，发现自我批评似乎削弱了计划生成的性能，并且系统的可靠性受到 LLM 验证器产生的显著错误结果的影响，二进制或详细反馈对计划生成几乎没有影响。总体而言，这些结果对于 LLMs 在计划任务的自我批评迭代框架中的有效性产生了质疑。

Oct, 2023