使用大型语言模型的检索增强 TLAPS 证明生成
Retrieval-Augmented TLAPS Proof Generation with Large Language Models
AI总结：
本文提出结合子义务分解与检索增强生成的 LLM 方法，用于 TLAPS 自动证明生成，并验证其对中等复杂度义务有效。
摘要：
我们提出了一种使用大型语言模型（LLM）为 TLA+ Proof System（TLAPS）自动生成证明的新颖方法。该方法结合了两个关键组成部分：一个子证明义务生成阶段，用于将复杂的证明义务分解为更简单的子义务；以及一个证明生成阶段，利用带有已验证证明示例的检索增强生成。我们使用不同复杂度级别的证明义务评估该方法，范围从基础算术性质到算法性质。实验表明，尽管该方法能够成功为中等复杂度的义务生成有效证明，但在处理更复杂的定理时存在局限。这些结果表明，我们的方法能够有效辅助某些类别性质的证明开发，有助于实现将 LLM 集成到形式化验证工作流中的更广泛目标。
英文摘要：
We present a novel approach to automated proof generation for the TLA+ Proof System (TLAPS) using Large Language Models (LLMs). Our method combines two key components: a sub-proof obligation generation phase that breaks down complex proof obligations into simpler sub-obligations, and a proof generation phase that leverages Retrieval-Augmented Generation with verified proof examples. We evaluate our approach using proof obligations from varying complexity levels of proof obligations, spanning from fundamental arithmetic properties to the properties of algorithms. Our experiments demonstrate that while the method successfully generates valid proofs for intermediate-complexity obligations, it faces limitations with more complex theorems. These results indicate that our approach can effectively assist in proof development for certain classes of properties, contributing to the broader goal of integrating LLMs into formal verification workflows.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
