本研究的主要作者是来自加州大学圣地亚哥分校的Kyle Thompson，以及来自葡萄牙里斯本大学INESC-ID及IST的Nuno Saavedra、帝国理工学院的Pedro Carrott、加州大学圣地亚哥分校的Kevin Fisher、马萨诸塞大学阿默斯特分校的Alex Sanchez-Stern和Yuriy Brun、里斯本大学INESC-ID及IST的João F. Ferreira、加州大学圣地亚哥分校的Sorin Lerner和Emily First。这项研究以论文形式发表，标题为“RANGO: Adaptive Retrieval-Augmented Proving for Automated Software Verification”，于2025年4月在加拿大大渥太华举行的第47届国际软件工程大会（International Conference on Software Engineering, ICSE）的会议论文集中发布。
此项研究的学术领域属于软件工程中的形式化验证与自动化定理证明，特别是与机器学习和大语言模型（Large Language Models， LLMs）交叉的前沿方向。研究的背景源于软件质量问题的巨大经济代价，以及形式化验证在保证软件正确性方面的卓越能力，例如唯一未发现错误的编译器CompCert就是通过Coq证明助手进行形式化验证的。然而，形式化验证过程需要大量专业知识和手动努力来编写证明，成本高昂。近年来，研究者们开始探索利用机器学习和LLMs来自动化证明合成。已有工作表明，识别相关的前提（如引理和定义）有助于合成。但先前基于检索增强生成（Retrieval-Augmented Generation, RAG）或检索增强证明（Retrieval-Augmented Proving, RAP）的方法未能充分利用证明过程中的局部信息，特别是未能持续利用当前项目中相似的证明作为灵感来源。因此，本研究旨在开发一种能自适应地检索并利用项目内已有证明和前提的自动化证明合成工具，以更有效地指导LLM生成证明步骤，从而提升自动化验证的效率和能力。研究的主要目标是提出RANGO方法和工具，创建一个用于训练和评估的大规模Coq数据集CoQStoQ，并通过系统性实验验证RANGO相较于现有先进工具的优势。
本研究的工作流程详尽而系统，主要包含几个核心部分：RANGO工具架构的设计与实现、CoQStoQ数据集的构建、模型的训练与微调，以及全面的评估实验。
首先，研究团队设计并实现了RANGO，一个用于Coq的完全自动化证明合成工具。RANGO的核心创新在于其自适应的检索增强证明架构。该架构包含两个主要子系统：策略生成器（Tactic Generator）和搜索器（Searcher）。策略生成器是核心，它由三个组件构成：证明检索器（Proof Retriever）、引理检索器（Lemma Retriever）和语言模型（Language Model）。在每个证明步骤，证明检索器会从当前项目的“证明库”中，使用BM-25稀疏检索技术，根据当前证明状态与库中证明状态的文本标识符相似度，检索出k个最相关的已完成证明。同样，引理检索器使用TF-IDF技术从“引理库”中检索出j个最可能被直接使用的引理陈述。然后，将这些检索到的相关证明和引理，连同当前定理陈述、已有的证明脚本和当前的证明状态，一起作为输入上下文，送入一个经过微调的、基于DeepSeek-Coder 1.3B参数模型的大语言模型中。该模型被训练来预测下一个应使用的战术（tactic）。为了处理LLM的令牌长度限制，研究中对各项输入都设置了最大令牌数并进行截断。搜索器则负责利用策略生成器来寻找完整的证明序列。它采用了一种名为“展开搜索”（rollout search）的简单而有效的过程：反复进行“展开”，每次展开中，从语言模型中采样一个战术，将其附加到当前证明尝试中，并由Coq检查结果。结果可能为“完成”、“无效”或“未完成”。若完成则搜索成功；若无效则开始新的展开；若未完成则继续当前展开。搜索持续进行直到找到证明或超时（研究中设定为10分钟）。这一工作流程的关键在于，检索是“在线”且“自适应”的，即在证明的每一步都重新检索，使模型能根据演变的证明状态和项目特定上下文动态调整其知识来源。
其次，为了有效训练RANGO，研究团队创建了一个全新的大规模数据集CoQStoQ。该数据集是从GitHub上挖掘的开源Coq项目集合。他们使用CoqPyt工具，基于截至2023年11月5日将Coq列为主要语言的所有开源仓库进行收集。他们尝试编译每个仓库，并仅包含在Coq 8.18版本下能无错误编译的有效文件。对于每个有效文件，使用CoqPyt提取每个证明步骤的文本表示、对应的证明状态及其上下文。最终，CoQStoQ包含了来自2,226个不同GitHub仓库的196,929个定理及其证明，共计2,225,515个证明步骤。研究人员将数据集划分为训练集、验证集和评估基准测试集。其中，基准测试集整合了先前基准CoQGym中能在Coq 8.18下编译的所有项目，并额外添加了CompCert和四个来自Coq社区、承诺长期维护的项目。训练集则包含其余所有数据。这种划分确保了评估的公正性，同时提供了充足的训练样本。数据集的规模（如训练集包含181,562个定理）和多样性为训练强大的模型奠定了基础。
第三，在模型训练与微调方面，研究人员使用从CoQStoQ训练集项目中构建的示例来微调预训练的DeepSeek-Coder 1.3B模型。每个训练示例的构建方式与推理时一致：在数据集的每个证明步骤运行证明检索器和引理检索器，然后用检索到的证明和引理构建提示，目标则是该步骤实际使用的下一个战术。他们使用LoRA技术和FSDP在4块NVIDIA A100 GPU上进行了60,000步的微调，并选择了在验证集上损失最小的检查点。优化器采用Adam，学习率为10^-3。输入上下文的令牌分配经过了精心设置：检索到的证明1024令牌，检索到的引理512令牌，定理和证明脚本512令牌，证明状态1024令牌，输出限制为128令牌。这些超参数的选择是为了在模型容量和上下文信息丰富度之间取得平衡。
第四，研究进行了广泛而深入的评估，以回答七个研究问题。实验设置中，RANGO使用单块NVIDIA RTX 2080进行推理，单个CPU配合16GB内存进行证明检查，超时10分钟，采样温度为1.0。
研究的主要结果在多方面体现了RANGO的优越性和其设计的有效性。
在回答RQ1（与其他工具对比）时，研究人员在CoQStoQ基准测试集的10,396个定理上比较了RANGO与三个当前最先进的Coq证明合成工具：Tactician、Proverbot9001和Graph2Tac。结果显示，RANGO成功合成了3,325个定理的证明，证明成功率为32.0%。这比Tactician（2,575个，24.8%）多证明了29%的定理，比Proverbot9001（2,007个，19.3%）多证明了66%。在与Graph2Tac的比较中（由于版本兼容性问题，仅在部分项目子集上可比），RANGO证明了4%更多的定理。此外，研究还评估了RANGO在两个预训练截止日期后创建的项目上的表现，以规避测试集污染问题，结果同样显示RANGO优于其他工具。这些数据强有力地支持了RANGO作为当前最先进的自动化证明合成工具的地位。
在回答RQ2（证明检索器和引理检索器的贡献）时，研究人员通过消融实验清晰地量化了各个检索组件的重要性。他们在从基准测试集中随机选取的500个定理子集（消融集）上测试了四个RANGO变体：完整RANGO、无引理检索器、无证明检索器、以及无任何检索（仅依赖微调后的LLM）。结果数据表明：完整RANGO的成功率为30.0%；移除引理检索器后降至29.0%（贡献较小）；移除证明检索器后大幅降至20.4%；而移除所有检索后仅为18.6%。这表明检索增强对RANGO的成功至关重要，共同贡献了61%的性能提升。其中，证明检索器单独贡献了47%的提升，显著大于引理检索器的贡献。这一结果直接支撑了本文的核心论点：在上下文中添加相关的证明（而不仅仅是引理）对于提升检索增强证明的性能极为重要。研究还通过跨文件分割的训练实验进一步证明，RANGO的证明检索器捕获了大量原本需要存储于LLM权重中的项目特定信息，从而使其在跨项目评估中表现更鲁棒。
在回答RQ3（证明检索算法的比较）时，研究评估了不同检索技术在证明检索器中的表现。在完整的基准测试集上，使用BM-25的RANGO证明了32.0%的定理，使用另一种稀疏检索技术TF-IDF的变体证明了31.7%，两者性能接近。然而，使用基于CodeBERT模型的稠密检索（通过计算证明状态嵌入的余弦相似度）的变体，性能大幅下降至22.0%。这一结果表明，对于证明状态相似性检索这一特定任务，基于词频统计的稀疏检索技术（如BM-25）比所测试的神经稠密检索方法更有效，可能因为后者未能充分捕获对证明步骤生成相关的语义特征。
在回答RQ4（与朴素检索变体的比较）时，研究人员探索了一种名为RANGO-Pre的朴素变体，它仅将定理所在文件中的前文行作为上下文，而不进行主动的跨项目检索。RANGO-Pre在基准测试集上证明了31.3%的定理，略低于完整RANGO。基于两者各有优势的假设（RANGO-Pre擅长利用邻近的、原生的上下文，而RANGO擅长检索远距离的相关信息），研究者创建了一个混合搜索过程RANGO-Hybrid，交替使用RANGO和RANGO-Pre进行展开搜索。结果显示，RANGO-Hybrid成功率为33.5%，比完整RANGO提高了4%，比RANGO-Pre提高了7%。这证明了结合不同检索策略的混合方法的有效性。
在回答RQ5（搜索器变体的比较）时，研究比较了RANGO使用的展开搜索与两种最佳优先搜索（Best-First Search）配置（分别使用集束解码和温度采样）。在消融集上的实验表明，展开搜索的成功率为30.0%，优于使用集束解码的最佳优先搜索（28.4%）和使用温度采样的最佳优先搜索（25.0%）。这确立了展开搜索作为一种简单而有效的证明搜索策略的价值。
在回答RQ6（理解RANGO的证明）时，研究进行了深入分析。他们发现，RANGO与其他工具一样，其证明成功率与人工编写证明的长度呈强负相关，证明越短越容易成功。此外，当定理所在文件具有大量依赖项（>100）时，所有工具的证明成功率都会下降，但RANGO凭借其检索机制仍然保持相对竞争力。研究还分析了RANGO所生成证明的质量。在RANGO、Tactician和Proverbot9001都能证明的1,252个定理集合中，RANGO生成的证明平均长度（4.5个战术）与Tactician相近，短于Proverbot9001，但比人工证明（4.0个）略长。更重要的是，通过计算与人工编写证明的字符串编辑距离，发现RANGO生成的证明平均比Tactician的证明更接近人工证明12个编辑操作，比Proverbot9001的证明接近21个编辑操作。这表明RANGO生成的证明风格更接近人类，可能更易于理解和维护。
研究的结论是，团队成功开发了RANGO这一自适应检索增强证明方法和工具，通过在每个证明步骤中动态检索并利用当前项目内的相关证明和引理，显著提升了自动化证明合成的能力。所创建的大规模数据集CoQStoQ为未来研究提供了宝贵的资源。全面的评估表明，RANGO在CoQStoQ基准上证明了32.0%的定理，性能超越了现有最先进的工具，其核心的证明检索机制带来了47%的性能提升。此外，混合检索策略和展开搜索也被证明是有效的优化手段。
本研究的科学价值和应用价值都非常显著。在科学上，它推进了检索增强生成在形式化验证领域的应用，首次系统地论证并实现了在在线、自适应环境下利用相似证明（而不仅仅是前提）来引导LLM生成证明步骤的有效性，为机器学习与定理证明的交叉研究提供了新思路和新方法。在应用上，RANGO作为一个实用的工具，能够直接降低形式化验证的成本和门槛，帮助开发者和验证工程师更高效地构建高可靠性软件，具有潜在的巨大经济和社会效益。论文也指出了未来工作的方向，如将RANGO方法应用于其他证明助手（如Isabelle, Lean），以及进一步探索更先进的检索和搜索算法。
本研究的亮点突出：第一，重要发现是证明了“检索相关证明”相比“仅检索引理”能带来大幅性能提升（47%），这是对先前RAP范式的关键扩展。第二，方法的新颖性在于提出了一个完整的、自适应的检索增强证明架构，将检索、LLM微调和搜索紧密集成，并在每一步实现上下文自适应。第三，研究对象的特殊性体现在创建并使用了迄今为止规模最大、经过精心整理的Coq证明数据集CoQStoQ，为领域内的可复现研究和公平比较奠定了坚实基础。第四，评估的全面性和深度值得称道，通过七个研究问题从多个维度深入剖析了工具的性能、组件贡献和生成证明的特性，并考虑了测试集污染等潜在问题，使得结论非常可靠。
其他有价值的内容包括：研究详细阐述了RANGO在CompCert等实际大型验证项目中的工作示例，直观展示了其如何利用跨文件的相似证明来合成新证明；研究还探讨了所生成证明更接近人类风格这一发现的意义，指出这可能有助于验证工程师后续的维护和修改，这是一个富有洞见的观察。最后，团队开源了RANGO工具、CoQStoQ数据集、所有训练好的模型以及复现实验所需的全部代码，充分体现了研究的可复现性和对开源社区的贡献。