FVEL：基于定理证明的大型语言模型互动式形式验证环境
内容提要
本研究提出了一种基于大型语言模型（LLMs）和自动推理的程序验证方法，结合形式化描述和验证器，提高了程序生成的准确性。通过对VHDL语言的形式推理和自动生成验证代码，显著提升了证明率和准确性。此外，开发了FOLK方法，实现复杂声明的验证与解释生成，实验结果显示其优于传统模型。
延伸解读
形式验证与LLM结合的技术路径
文章展示了多种将大型语言模型与形式验证结合的方法。例如，通过代码模型采样生成程序，再用后验验证器重新排序，提高正确性；或利用LLMs将自然语言数学问题翻译为Isabelle/HOL形式化说明，提升定理证明成功率。这些方法共同表明，LLM的生成能力与自动推理的严谨性可以互补，但具体效果依赖于验证器的质量和形式化描述的准确性。
FOLK方法的可解释性优势
FOLK方法通过将复杂声明转化为一阶逻辑子句，并利用知识库问答进行推理，不仅做出真实性预测，还能生成解释决策过程。这种可解释性使模型在验证任务中更透明，实验也显示其在三个数据集上优于强基线。对于需要高可信度的应用场景，这种结合逻辑与知识的方法提供了新思路，但需注意其依赖知识库的质量和覆盖范围。
实际应用中的验证框架与工具
文章提到基于Rust的形式验证框架Verus原型，通过分解验证任务、迭代查询GPT-4并结合静态分析，显著减少了编写证明代码的人力。类似地，LLM4PLC利用用户反馈和外部验证工具改善生成代码的可验证性。这些实践表明，将LLM嵌入现有验证工作流能提升效率，但工具成熟度和对特定语言（如VHDL）的支持仍是落地时的考量因素。
Q&A
FVEL方法的主要创新点是什么？
FVEL方法结合了大型语言模型和自动推理，提升了程序生成的准确性和证明率。
FOLK方法的功能是什么？
FOLK方法用于复杂声明的验证和解释生成，利用一阶逻辑进行推理。
如何提高VHDL语言的形式推理准确性？
通过对VHDL语言进行形式推理和自动生成验证代码，可以显著提升准确性。
该研究如何利用大型语言模型处理数学问题？
研究表明，大型语言模型可以将自然语言的数学问题翻译为形式化说明，从而提升定理证明的成功率。
Verus框架的优势是什么？
Verus框架通过将验证任务分解为小任务，显著减少了编写证明代码的人力工作。
FVEL方法在实验中表现如何？
实验结果显示，FVEL方法在多个领域取得了最优的生成效果。
