本研究探讨了使用自然语言提示生成 SystemVerilog 声明（用于硬件安全），研究了一种流行的大型语言模型的能力，并设计了一个评估框架来生成各种提示并创建基准套件，该套件由真实硬件设计和相应的黄金参考声明组成。

Jun, 2023

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

Nov, 2023

我们提出了一个基于逻辑推理的框架，用于将宣称或传言与证据分解为验证所需的原子推理步骤，并通过维基百科的合成数据集和在 Twitter 上流传的谣言的真实数据集对 GPT-3.5-Turbo 和 GPT-4（以下简称 ChatGPT）的推理能力进行评估，结果显示 ChatGPT 在因果推理方面存在困难，但通过使用手动 Chain of Thought（CoT）而不是 Zero Shot（ZS）和 ZS CoT 方法可以在一定程度上缓解这一问题。我们的研究为 ChatGPT 的推理过程不太可能与人类类似的推理过程相一致，并且指出 LLMs 需要在高风险的实际任务（如宣称验证）中进行更严格的评估，以区分炒作和实际能力。

Feb, 2024

我们探讨了如何通过进行辩论式的对话来测试大型语言模型（LLM）的推理能力，以此来衡量模型是否真正理解了问题的本质。对多个复杂的推理测试进行实验表明，尽管 ChatGPT 等模型一开始可以生成正确的解决方案，但在面对荒谬的无效论据时，它们无法保持对真理的信仰。

May, 2023

本文旨在演示通过大型语言模型与自然语言交互实现高效逻辑设计的自动化设计环境，其中展示了一个基于大型语言模型的四阶段零代码逻辑设计框架，并证明相较于现有工作及单一大型语言模型，ChipGPT 提高了可编程性、可控性和设计优化空间。

May, 2023

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

Mar, 2024

我们引入了 LogicAsker，它是一种自动方法，全面评估和改进基于命题和谓词逻辑的大型语言模型的逻辑推理能力，并揭示了 LLM 未能学好的逻辑规则。我们评估了 LogicAsker 在 GPT-3、ChatGPT、GPT-4、Bard、Vicuna 和 Guanaco 等主要的大型语言模型上，并展示了 LogicAsker 的测试用例在不同 LLM 中发现逻辑推理错误的比率从 25% 到 94% 不等。此外，LogicAsker 的测试用例可以进一步用于设计上下文学习的演示例子，有效提高 LLM 的逻辑推理能力，如 GPT-4 提高了 10%。据我们所知，我们的工作是首次基于测试结果创建提示来有效提高 LLM 的形式推理能力。所有的代码、数据和结果都将被公开以供复制和未来研究。

Jan, 2024

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

Jan, 2024

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

Oct, 2023

使用大型语言模型（LLMs）生成断言的有效性和适用性的定量评估。

Jun, 2024