VeriBase把验证成功的代码与定理一起泛化：通用库让任务成功率从63.0%升到73.0%
核心概要
软件验证的证明往往比写代码更费力，而已完成的验证成果很难自动变成可复用定理库。VeriBase把代码与其关联定理当作一个声明族，经证明、泛化、收割三个阶段自动构建Lean库，并在接口变化时同步更新依赖声明。由4,191个独立程序构建的通用库把三个单文件基准、三个后端模型上的平均任务成功率从63.0%提升到73.0%，平均完成时间缩短13.2%。
深度剖析
VeriBase让一次成功的软件验证不再只服务那一道题，而是被整理成后续任务可直接调用的代码与定理库。 此前把验证成果转成库需要专家识别可复用功能、设计通用接口并整合依赖，这类定理库在软件验证领域相对稀少。 在Verina、FVAPPS、VeriContest三个单文件基准与三个后端模型共九种组合上，由基准外4,191个程序构建的通用库把宏平均任务成功率从63.0%提高到73.0%。
库的构建分三步：先让智能体在Lean中把任务做对，再把实现和证明中的中间事实抽象成通用形式，最后把各任务的重叠声明合并进同一套接口。 泛化以代码为先、定理为后，代码接口改动后依赖的定理陈述与证明随之改写，并由Lean检查。 收割阶段按来源任务分批整合，对候选声明执行新增、跳过或合并，并在每批之后编译受影响模块；最终通用库含1,609个代码声明和3,239条定理。
在仓库级证明任务上，自动构建的库能接近人工编写的支撑定理所起的作用。 VeriSoftBench原本依赖人工开发的支撑定理，评估时先移除这些定理再构建库。 移除人工支撑定理后，构建的库把三个后端的平均成功率从56.3%提高到77.0%；以GLM 5.2为例，自动库达到81.0%，原始支撑定理为84.0%。
启示与展望
展示范围是Lean 4中的软件验证任务：三个单文件基准与一个仓库级基准，配合DeepSeek V4 Pro、GLM 5.2、Qwen 3.7 Max三个后端模型，库在评估期间保持固定。对C、Rust等其他语言的软件，复用还需要建立源程序与其Lean表示之间的语义联系。
API成本随后端模型而异：接入通用库后DeepSeek V4 Pro的成本上升18.3%至33.3%，GLM 5.2与Qwen 3.7 Max则增减不一，检索增加输入上下文而复用声明减少后续生成。通用库规模实验显示，构建语料超过500个任务后效率提升趋于饱和，而任务覆盖率仍继续上升。