Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
Rango利用检索增强的自动证明，结合项目相关证明提升自动化水平，达成32%的证明成功率。
核心发现
方法论
Rango采用基于微调的深度学习模型（DeepSeek-Coder 1.3B参数）结合检索机制，动态选择相关证明和引理，利用BM-25和TF-IDF算法实现证明和引理的检索。模型输入包括当前证明状态、已检索的证明、引理和目标定理，逐步生成证明策略。检索机制确保模型在每个证明步骤都能获取项目中最相关的资源，从而实现自适应证明策略。通过构建CoqStoq数据集，涵盖2226个开源项目和196,929个定理，训练和评估模型性能。
关键结果
- 在CoqStoq基准测试中，Rango成功合成32.0%的定理证明，优于Tactician（占比29%），提升29%。在包含CompCert和长期维护项目的测试集中，证明成功率分别达到了37.2%和35.8%。引入相关证明后，证明成功数提升47%，验证了检索机制在动态证明中的关键作用。
- 与其他SOTA工具Proverbot9001和Graph2Tac相比，Rango在所有测试项目中表现优越，证明数分别多出66%和29%。在大规模数据集上，Rango展现出更强的泛化能力和适应性。
- 通过引入多模态检索（BM-25和TF-IDF），模型在证明效率和准确率上均显著提升。 Ablation研究显示，检索引理和证明的结合是性能提升的核心因素。
研究意义
该研究突破了自动化定理证明的瓶颈，将检索机制与大语言模型深度融合，实现对项目内相关知识的动态利用。此技术不仅提升了自动证明的成功率，也为软件验证自动化提供了新思路，有望推动形式验证在工业中的广泛应用，降低人工成本，提升软件质量。
技术贡献
创新点在于引入多模态检索机制（BM-25和TF-IDF）结合微调的LLM，动态选择相关证明和引理，形成自适应证明策略。模型在每个证明步骤都能根据上下文实时调整，显著优于传统静态方法。提出的CoqStoq数据集为未来研究提供了丰富的训练和评估资源。技术上实现了在有限上下文中高效利用项目知识，增强了模型的推理能力和适应性。
新颖性
首次将检索机制与大语言模型结合，用于动态证明生成，强调在每个证明步骤都引入相关证明和引理，提升证明成功率。不同于以往只在证明开始时检索资料的静态方法，Rango实现了全过程的知识动态融合，具有较强的创新性。
局限性
- 模型对极大项目或复杂定理的表现仍有限，尤其在证明链较长或引理缺失时效果下降。
- 检索机制依赖特定算法（BM-25、TF-IDF），在某些语义相似但词汇不同的场景下效果有限。
- 训练成本较高，模型微调和检索机制的结合对硬件资源要求较大，未来需优化效率。
未来方向
未来将探索更先进的检索技术（如神经检索），提升模型对语义的理解能力。还计划扩展数据集，涵盖更多工业场景中的复杂证明，增强模型的泛化能力。同时，将结合形式验证工具链，推动自动证明在实际软件开发中的应用落地。
AI 总览摘要
随着软件系统日益复杂，确保其安全性和可靠性变得尤为重要。传统的形式验证方法虽能提供高保证，但其高昂的人工成本和技术门槛限制了其普及。近年来，利用大规模预训练模型（LLMs）辅助自动证明成为研究热点。本文提出的Rango系统，结合检索机制与微调的深度学习模型，实现了在每个证明步骤中动态引入相关证明和引理，从而显著提升自动证明的成功率。
Rango的核心创新在于引入多模态检索机制（BM-25和TF-IDF），在项目中实时检索相关证明资源，结合模型生成策略，形成自适应证明流程。通过构建包含2226个开源项目和196,929个定理的CoqStoq数据集，模型在多个工业级和开源项目中验证了其优越性能。在基准测试中，Rango的证明成功率达到了32.0%，比最先进的Tactician高出29%。引入相关证明后，成功率提升了47%，验证了检索机制的有效性。
该技术不仅推动了自动化定理证明的边界，也为工业软件验证提供了新的解决方案。未来，结合更先进的检索技术和扩展数据集，有望实现更高效、更智能的自动验证系统，推动软件工程向更高可靠性迈进。局限方面，模型在极大项目和复杂证明中的表现仍需优化，硬件资源消耗较大，未来将持续改进算法效率与适应性。
深度分析
研究背景
形式验证作为确保软件正确性的重要手段，近年来取得显著发展。早期方法依赖手工证明，效率低下，难以推广。随着自动定理证明（Automated Theorem Proving, ATP）技术的兴起，诸如Coq、Isabelle等交互式证明助手逐渐成为主流。近年来，结合大语言模型（如GPT系列）辅助证明生成的研究逐步展开，旨在降低人工门槛，提高自动化水平。代表性工作包括Tactician、Proverbot9001和Graph2Tac，它们通过不同的学习策略实现部分自动化，但在复杂证明和项目适应性方面仍存在局限。现有方法多依赖静态资料检索或规则驱动，缺乏动态知识融合能力。本文在此背景下提出Rango，旨在突破这一瓶颈，将检索机制与深度学习模型结合，实现全过程的知识动态利用。
核心问题
当前自动证明工具在复杂证明场景中表现有限，尤其是在面对长链证明或缺乏引理的情况下，成功率明显下降。传统方法多依赖静态资料检索或预定义策略，难以适应项目的局部变化和证明状态的动态演变。这限制了自动化水平的提升，阻碍了形式验证在工业中的广泛应用。如何在保证效率的同时，动态引入项目相关知识，提升证明的成功率，成为亟待解决的核心问题。
核心创新
本研究的创新点在于引入多模态检索机制（BM-25和TF-IDF），实现对项目中相关证明和引理的实时动态检索。结合微调的深度学习模型（DeepSeek-Coder），在每个证明步骤中根据检索结果生成下一步策略，形成自适应证明流程。不同于以往只在证明开始时检索资料，Rango在每个步骤都能根据证明状态调整知识输入，极大提升了模型的推理能力和适应性。此外，构建的CoqStoq数据集为模型训练和评估提供了丰富资源，推动了自动证明技术的持续发展。
方法详解
- �� 采用深度微调模型（DeepSeek-Coder 1.3B参数）结合检索机制，动态选择相关证明和引理。• 使用BM-25算法对项目中的证明状态进行相似性匹配，检索最相关的证明资源。• 利用TF-IDF算法检索项目中的引理，确保引理的相关性。• 在每个证明步骤，将检索到的证明和引理作为模型输入，结合当前证明目标和状态，生成下一步策略。• 构建CoqStoq数据集，包含大量项目和定理，用于训练和评估模型性能。• 设计基于rollout的搜索策略，结合模型预测，逐步构建完整证明。• 通过多轮实验优化检索参数和模型超参数，确保系统的鲁棒性和效率。
实验设计
采用CoqStoq数据集进行训练和评估，包含2226个项目和196,929个定理。模型在多个工业和开源项目上进行测试，比较基线包括Tactician、Proverbot9001和Graph2Tac。指标包括证明成功率、证明数目和平均时间。采用10分钟超时限制，评估模型在不同项目中的泛化能力。还进行了消融实验，验证检索机制对性能的贡献。模型超参数包括学习率10^-3、批次大小16，利用GPU加速训练。测试环境为单GPU推理，确保实际应用的可行性。
结果分析
在CoqStoq基准中，Rango实现了32.0%的证明成功率，比Tactician高出29%，在CompCert和长期维护项目中分别达37.2%和35.8%。引入检索机制后，证明数提升47%，验证了知识动态引入的有效性。与Proverbot9001和Graph2Tac相比，Rango在所有测试中表现优越，证明数分别多出66%和29%。 Ablation研究显示，结合证明和引理检索的策略显著优于单一检索方案，验证了多模态检索的优势。
应用场景
该技术可广泛应用于工业软件验证、自动化测试和安全关键系统的形式验证。只需提供项目的证明资料和目标定理，系统即可自动生成证明脚本，降低专业门槛。未来，结合持续集成（CI）流程，有望实现自动化验证的实时集成，提升软件开发效率和可靠性。
局限与展望
模型在极大规模项目或复杂证明中仍存在性能瓶颈，尤其在证明链较长或引理缺失时效果有限。检索机制依赖特定算法（BM-25、TF-IDF），在语义相似但词汇不同的场景下表现不足。训练成本较高，硬件资源消耗大，未来需优化算法效率和模型压缩技术。
通俗解读 非专业人士也能看懂
想象你在厨房里做菜，菜谱上写着各种步骤，但每次你做菜时，可能会忘记一些细节。于是，你会找一本类似的菜谱，看看别人是怎么做的，然后根据自己的情况调整。Rango就像这个厨房助手，它会在你做菜的每一步，帮你找出最相关的菜谱和技巧，告诉你下一步怎么做。它会不断地从厨房里的所有菜谱中检索最合适的内容，帮你做出更好吃的菜。这样一来，即使你是新手，也能做出专业水平的菜肴。这个系统让复杂的证明变得像做菜一样简单，靠不断找灵感，逐步完成任务。
简单解释 像给14岁少年讲一样
想象你在学校里写作文，有时候不知道下一句话怎么写。你可以偷偷看看朋友之前写的好句子，或者找一些范例，借鉴他们的表达。Rango就像一个聪明的朋友，它会在你写作文时，帮你找到别人写过的精彩句子和段落，然后告诉你下一步怎么写。每次你写一点点，它都会帮你找出最相关的例子，帮你继续写下去。这样，你的作文就能变得越来越棒，不用担心写不出来。它就像一个会帮你搜集灵感的超级助手，让写作变得轻松又有趣。
术语表
Proof Assistant (证明助手)
一种软件工具，用于帮助用户构建和验证数学证明，确保逻辑正确性。
论文中提到的Coq就是一种证明助手。
Large Language Model (大语言模型)
基于深度学习的预训练模型，能理解和生成自然语言，应用于自动证明生成。
Rango中的核心模型是微调的LLM。
Retrieval-Augmented Generation (检索增强生成)
结合信息检索技术与生成模型，提升内容的相关性和准确性。
Rango采用此技术增强证明生成。
BM-25
一种信息检索算法，用于衡量文本之间的相关性，常用于文档检索。
用于检索证明状态的相似性。
TF-IDF
一种文本特征提取方法，用于衡量词语的重要性，帮助检索相关引理。
用于引理的相关性评分。
开放问题 这项研究留下的未解疑问
- 1 如何进一步提升模型在长链复杂证明中的表现仍未解决，尤其是在引理缺失或证明链较长的情况下，模型的推理能力和检索机制需要优化。
应用场景
近期应用
工业软件验证
利用Rango自动生成软件关键部分的证明，降低人工成本，提升验证效率。
自动化测试辅助
结合证明自动化，增强软件测试的覆盖率和可靠性，适用于安全关键系统。
远期愿景
智能软件开发助手
未来可集成到开发环境中，实时辅助程序验证，推动自动化软件工程。
原文摘要
Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual effort to write proofs. Recent work has explored automating proof synthesis using machine learning and large language models (LLMs). This work has shown that identifying relevant premises, such as lemmas and definitions, can aid synthesis. We present Rango, a fully automated proof synthesis tool for Coq that automatically identifies relevant premises and also similar proofs from the current project and uses them during synthesis. Rango uses retrieval augmentation at every step of the proof to automatically determine which proofs and premises to include in the context of its fine-tuned LLM. In this way, Rango adapts to the project and to the evolving state of the proof. We create a new dataset, CoqStoq, of 2,226 open-source Coq projects and 196,929 theorems from GitHub, which includes both training data and a curated evaluation benchmark of well-maintained projects. On this benchmark, Rango synthesizes proofs for 32.0% of the theorems, which is 29% more theorems than the prior state-of-the-art tool Tactician. Our evaluation also shows that Rango adding relevant proofs to its context leads to a 47% increase in the number of theorems proven.