逐步：用于自动化系统验证的神经符号证明搜索

摘要

基于交互式定理证明的形式化验证日益被用于确保关键系统的正确性，但构建大型证明脚本仍然高度依赖人工，限制了可扩展性。大语言模型（LLM）尤其是数学推理方面的进展，使其融入软件验证的前景日益可期。本文提出一个神经符号证明生成框架，旨在自动化系统级验证项目的证明搜索。该框架对证明状态执行最佳优先树搜索，反复向LLM查询下一个候选证明步骤。在神经侧，我们使用证明状态-步骤对的数据集微调LLM；在符号侧，我们集成一系列ITP工具来修复被拒绝的步骤、过滤与排序证明状态，并在搜索进展停滞时自动消解子目标。这种协同实现了数据高效的LLM适配以及基于语义信息的搜索空间剪枝。我们在一个新的Isabelle REPL上实现该框架，它暴露细粒度证明状态与自动化工具，并在FVEL seL4基准及其他Isabelle开发上评估。在seL4上，该系统证明了多达77.6%的定理，大幅超越先前基于LLM的方法与独立的Sledgehammer，同时求解了显著更多的多步证明。在更多Isabelle基准上的结果展示了强泛化能力，表明一条通往可扩展自动化软件验证的可行路径。

面向规模化系统软件验证的神经符号证明生成：论文配图 — 图 1：来自 seL4 项目的示例定理及其人工编写的证明，与 LLM 生成的尝试一起显示。人类编写的伊莎贝尔证明说明了软件验证中常见的程序性、策略驱动的推理风格。我们促使两个最先进的LLM Gemini 3 和 GPT-5.1 在受控条件下合成相同的证明，并禁用网络搜索以避免原始脚本的泄漏。尽管这两个模型都正确识别了证明上下文并调用了一些相关策略，但即使经过大约一分钟的内部推理，也没有成功产生有效的证明。他们的尝试经常滥用特定领域的 wp 策略，或者幻想不存在的引理。