CAPRI 这个名字最近出现在 Isabelle 交互式定理证明相关的讨论里核心指向的方向是“契约感知的证明修复”。如果只看字母缩写可能会误以为它是一个自动补全证明的通用工具。实际上它解决的问题很具体当 Isabelle 理论里的函数、谓词、定义或规范契约发生变化后旧依赖这些证明的记录实现任务会大量失败CAPRI 这类系统要做的就是让失败定位和重建过程具备对契约变化的感知而不是只知道“这一步过不去”。先给出我的总体判断如果你正在维护一段长期演进的形式化验证代码里面有函数规格、接口契约和成片依赖的 lemma那么“契约感知的证明修复”会是一个非常值得关注的思路。它的价值不在于替你写出一个新发明而是在你删改一行定义导致二十处证明失败后帮你更快找出哪些失败是真需要改契约哪些失败只是旧证明步骤在实现层不匹配。这篇文章我会从实际工程体验出发拆解 CAPRI 术语背后的思想、Isabelle 证明失效的原因、本地复现实验时该准备的前提条件以及你在引入这类方法前应该关注的风险点。1. 先理解 CAPRI 与 contract-aware 的关系1.1 CAPRI 不是“万能补证明器”不少人在 Isabelle 项目里遇到一堆 lemma 变红时第一反应是找个工具自动跑一遍看能不能把错误状态消掉。这是把证明修复想得太简单了。CAPRI 所属的“proof repair”方向关注的是证明文本在某次理论变更后失去合法性时的自动化处理过程。它处理的不是某局部语法报错而是结果失效。旧证明曾经能被 Isabelle 完整检查过现在因为环境变了导致原来的证明状态在某一位置无法推进或某条引理无法满足当前条件约束。CAPRI 的输入通常是三样东西变更前的旧理论、变更后的新理论、变更前后的契约对应关系。它做的并不是把旧证明删除然后跑到任意库里去试探。它更愿意保留旧证明中仍然有效的结构只把受契约变化波及的部分挑出来重新调整证明策略、中间状态和前置假设。1.2 contract-aware 是“契约感知”不等于普通接口推断很多关于自动修复的讨论只关心接口签名比如函数从两个参数改成三个参数然后生成函数替换。契约感知比这个更深处一层。在 Isabelle/HOL 的形式化表达里契约可以表现为前置条件、后置条件、类型约束、归纳定义规则、函数终止规则、不变量、状态转换关系等。你在证明一个函数满足某个性质时经常不是因为函数名的拼写变了导致失败而是函数所遵守的契约变化了。举个例子一个step函数原本保证任何输入都会前进一步经某次重构后它加入边界控制大于等于某值的输入不再变化。这时候原先证明x step x所依赖的简单展开关系已经不再成立真正需要修复的其实是证明前提要加一个阈值约束变成x threshold ⟹ x step x。这就是让 CAPRI 需要感知的内容哪些性质与契约中的前置条件绑定哪些只需要改变方法调用顺序。如果系统不理解这种语义映射它只能机械地把旧 proof script 重播一遍最后告诉你在某一行失败对维护的实际帮助非常有限。1.3 与手动修复和通用重写的差别手动修复当然可行但对于大型理论库来说成本很高。尤其当一次接口更新会牵动数百个依赖引理时纯手工检查每一个 apply 步骤的状态几乎不可维持。通用重写工具的问题则相反它往往太“激进”不了解哪些旧证明结构对新契约依然有意义。修正时可能生成一个能让当前目标闭合的证明却没有保留证明的结构语义或者为了过某个 lemma擅自弱化原命题最后产生的结论根本不是用户本意想维护的性质。CAPRI 这类契约感知方案提供的是中间态利用契约变化前后的对应关系把失败限制在特定的证明片段上再针对契约失效原因从知识库、已有引理和可选择性原语中构建新的证明片段最终生成一个可审阅、可回放、可维护的成果。它解决的核心矛盾始终只有一个在验证工程中代码和契约在演进而手工同步所有证明的成本正在快速上升。2. 实际中哪些项目会被这类证明修复问题卡住2.1 长期演进项目最容易遇到“证明烂尾”Isabelle 并不只存在于学术 demo。操作系统模型验证、编译器语义、并发算法、分布式协议形式化、程序逻辑和小型函数式语言的设计验证都会把 Isabelle 作为长期验证环境。这类项目往往需要数月甚至数年的迭代真正能撑到最后的团队都知道一件事代码结构变化是常态证明跟着适应才是复杂度最大的来源。我在本地方案中遇到过一种典型状态定义更新之前某个理论文件还处于绿色状态验证耗时也就几十秒。然而某次为了调整一个数据结构字段改动后的契约不再支持原来的不变量结果并没有集中在定义那一处而是顺着引用网络跑到了别的文件里。一个 lemma 失败后后面所有依赖它的 theorem 也开始连片变红滚动页面时都不太容易看出最初的错误发生在哪里。CAPRI 所针对的场景正是这种。它关心“下游证明为什么会坏”并要求你提供契约变化前后的框架好让工具在大量下游失败中区分共同原因而不是逐个去修复表象。2.2 适合使用的前置条件不是所有 Isabelle 项目都适合跑契约感知修复。我建议先做三个检查。第一项目里需要存在相对稳定、命名清晰的契约结构。如果全部是自由定义的辅助函数每个都没什么语义约束那契约变化其实很难界定。第二你对历史版本有版本管理。修复的前提是比较没有变更前后快照很难区分某项证明失败到底来自哪一次契约改动。第三理论文件的可构建性要好。依赖关系混乱、互相循环导入、文件构建顺序不固定会让自动修复系统接收到大量低质量信号修复效果会明显下降。这里至少有一个判断底线如果一个项目连当天完整编译一遍都要碰运气那你最需要的其实不是自动修复而是先把项目构建链理顺。2.3 边界情况不要过度硬套契约感知修复不擅长处理完全推翻重写的理论。如果整个证明和契约领域已被替换很多旧证明片段保留不了有价值的信息再去做修复跟从零写证明的差别不大。它也不适合用来掩盖漏写的证明。一台自动修复系统为了把状态闭合可能会给出一种没经过语义风险审查的证明看起来通过了 Isabelle 的类型检查却把原本要证明的边界条件给回避了。这种情况下如果你缺少足够的契约 review 环节自动修复带来的风险比你手写一个稍慢的证明还要更危险。更现实的应用方式是“分路径修复”对于改动十分局部的函数启用自动修复让系统补齐受影响的 lemma对于涉及核心安全性质的主定理要求人工逐步审阅。等到自动修复结果在多条分支上都产生可复用的新模式再放开限制应用到更大范围。3. Isabelle 中旧证明为什么“集体烂掉”3.1 证明是叠积木式依赖链Isabelle 里每个 lemma、theorem、inductive case 都会形成一个被证明库正式承认的事实。后来的证明可以使用前面的定理进行重写、解算条件、触发推理因此后续证明天然建立在一张依赖图谱上。如果上层某个定义发生变化但旧定义的可简化规则仍然保留部分低层证明可能还看不出问题。真正的问题通常出现在一个引理被某条件削弱后所有引用它作为辅助步骤的证明都会面临触发条件不匹配进而集体失败。单纯看某一行报错很难定位到源头是第 100 行的定义还是第 1300 行由匿名中间 lemma 添加的约束条件。自动修复系统要做的是顺着这条依赖链反向检查而不是停在首次报错的位置。3.2 失败状态有几种常见样态契约变化后旧证明文件报错状态并不总是千篇一律。我通常会观察以下特征作为判断失败来源的参考现象更可能的源头某处simp或auto找不到重写规则相关定义被调整可简化性质或原 rewrite lemma 不再是前提apply 步骤执行后还有剩余子目标问题逻辑前提比旧契约多证明方法无法覆盖新增分支by ...直接报“无法证明”引理结论在新契约下已经不成立真正需要写新性质后面大量 lemma 因前置 lemma 失效而级联失败先回到依赖源头逐层修好公共定理证明在induction分支上进展异常递归函数结构或终止规则变化归纳假设不再匹配这五类情况并不互斥。CAPRI 做分析时往往会先看失败目标中最先出现的现象因为越早失效的状态通常意味着更靠近真实源头等到后面出现的大量失败是直接依赖关系被破坏后产生的传播效应。3.3 为什么“把 auto 重跑一遍”不够受启发有人写过自动把失败证明里的by smt替换成by auto的经验。问题是当契约真的变化了简单地重跑 auto 并不能解决根源。auto、simp这类方法只会在当前上下文的已知定理和定义里自动搜索它们并不会去判断你是不是需要新增一个前置假设。新旧契约在语义上不再是等价的关系映射重跑推理方法只会重复失败区别只是失败点或输出消息更加不透明。而且自动重跑很容易制造假阳性信心。你可以看到一个 lemma 变成了绿色以为修复成功了操作权限却没有注意这个 lemma 的广义相对性是否被暗中改变了。没有契约感知的话这种自动“成功”并没有把你带向目标。更让人担心的是若干次自动重跑后代码里累积了大量只针对当前版本可过的引用技巧再次演进时旧证明几乎完全没有参考价值。4. 本地实验 CAPRI 前建议你准备的复现环境4.1 环境准备不复杂但要做三件事这里不谈具体版本号只给通用顺序因为你拿到的工具和 Isabelle 发行版未必完全匹配。落地时以你本地实际依赖为准。先安装 Isabelle 本体并确认命令行里能调用到对应可执行文件。再建一个干净的目录当作试验场把待修复理论、依赖脚本和日志目录都放在同一层。最后用 git 或等价工具记录一次“变更前”的 baseline。记录 baseline 有个特别实际的好处你可以在坏掉之后快速跑出两个清单。一个清单是旧版本里可以完整训练的 lemma 数量另一个是改动后可以训练的数量。两边做 diff帮助 CAPRI 这类工具缩小修复范围。4.2 设计一个能复现的最小理论我会用一版最小可运行的 Isabelle/HOL 示意代码来说明失败机制。这里的边界很关键不同版本 Isabelle 支持的语法细节不同建议你把它当成结构示意不要直接复制到生产库。theory ContractDemo imports Main begin (* 第一个契约版本step 对所有输入都前进一步 *) fun step :: nat \Rightarrow nat where step x x 1 (* 旧证明任意输入增加 *) lemma step_increase: x step x by simp (* 第二次契约调整加入边界控制 *) fun step :: nat \Rightarrow nat where step x (if x 10 then x 1 else x) (* 旧证明继续执行会失败 *) lemma step_increase: x step x by simp (* 契约感知修复后的思路 结论不再全称成立需要把 x 10 拆成前置条件写清楚 *) lemma step_increase_under_contract: x 10 \Longrightarrow x step x by auto end注意在同一理论里同名fun定义即使不允许重复上述代码只是为了说明当函数契约从“无条件递增”改成“阈值内递增再不变”时旧证明不能直接复用而修复不能只靠切换证明方法完成关键在于把新契约纳入定理前置条件。如果你要测试的工具比手工改 lemma 更自动化输入最好直接使用新旧两个理论文件并且用 diff 生成契约变更位置列表让系统先尝试匹配哪些定义在旧版本里的证明结论仍然与新版本语义可对齐。4.3 验证修复是否真成功用什么标准很多人只关心 Isabelle 是否回了个绿灯。但对一个维护任务来说验证标准至少要包括五层。第一层是可复现。同一个修复命令再次执行结果稳定。第二层是范围边界。修复后的 lemma 数量、新增的假设数量、对输入文件外部依赖的改变量都能被输出出来。第三层是证明可理解性。你能否看出它到底用了哪条引理、哪个前置条件把目标推过去的。第四层是旧证明保留度。如果这次修复把所有 lemma 全部推倒重建虽然系统任务最终过了但维护上的价值很可能不高。理想的修复应该尽量保留没有涉及契约变化的旧证明路径。第五层是回归风险。修复之后旧版本代码里原本依赖旧契约的证明是否受影响如果影响有没有统一记录。这五个标准也是评测 CAPRI 时比较关键的观测点。若只看工具自身是否成功结束很容易错过隐藏的语义漂移。5. 把自动修复机制拆成四个理解单元5.1 将“契约变化”与“证明失败”对齐契约感知的第一步是做对齐。系统把旧版本中函数的定义、类型、前置条件和后置条件项作为旧契约把新版本中对应的项作为新契约然后将旧证明中每一步所依赖的契约分量映射到新版本。这一步的复杂度在于 Isar 证明里往往存在大量匿名假设和中间态。系统要判断某个问题的失败是因为契约新增条件导致前提不可达还是因为契约的结论本身已经变弱或变强抑或是一个旧 proof 方法触发了不同语义的重写规则。这样对齐完才能把修复对象缩小到某个子目标上。如果没有这一步修复脚本只能在失败位置尝试一个动作列表无法理解哪些地方值得保留哪些地方必须重建。这也是许多“证明修复插件”看似集成方便、效果却很有限的原因。5.2 在证明文本里定位断裂点对齐后系统可以给出失效范围图谱。旧的 lemma 本来依赖 A、B、C 三条引理契约调整后 A 变了B 没变C 只是被新版本的 A 间接影响。修复系统会识别出第一个真实断裂点。有的断裂发生在证明开头比如 lemma 加入assumes后直接导致现有证明上下文发生变化。有的断裂发生在中间某个apply (subst ...)步骤因为重写引理被移除。还有的断裂发生在终点by auto虽然把旧目标几乎推完但新契约下多了个分支需要再补一步展开。断裂点粒度非常重要。一个apply (auto simp: ...)可以接纳二十个引理一旦失败你很难只靠外层报错判断如何补。CAPRI 类机制会再次尝试把该步骤展开为若干小步骤从失败状态中提取出没有目标闭合的分支再交给下一阶段去修复。5.3 为受影响的证明片段构造新路径定位完成后进入真正意义上的 proof repair。系统会尝试在失败子目标上匹配可用的定义扩张、simp 规则、已有定理、条件激活性、归纳结构等信息。与纯粹的sledgehammer使用不同CAPRI 不是把整条目标传给外部求解器而是在保留旧证明路径上下文的前提下对局部目标搭建一条新路径。如果目标只是缺了一个前置条件系统会修改 lemma 的头部把该条件写入assumes如果目标来自函数的递归结构变化系统会把证明风格从apply auto改成apply (induction ...)并在相应分支补条件如果问题源于重写规则缺失它可能生成一个新引理把新的定义展开式制作成 rewrite rule插在旧失败点之前。从代码库维护者的角度这里最有价值的不是那些已经能自动提示的 lemma 名称而是系统建议修改的点。一个靠谱的修复成果应该看起来像旧证明中 80% 的步骤不变只在新契约外增加少量步骤或前置条件并且在注释里标明为什么要加。这比生成一大段复杂到人肉无法审阅的 Isar 脚本要实用得多。5.4 产出仍要经过人工思考一道由于 CAPRI 来自定理证明研究的延伸当前不建议把它输出的修复结果当成最终成果。至少在关键性质上需要做一次人工 review。原因是证明修复的语义并不只是“让所有目标收到done”。尤其在前置条件变化的情况下工具更容易配合全称量词变化、前置条件调整等整体上合法的修改。人工 review 可以分三步查看修复涉及的契约头变更确认是否与期望的 API 演进方向一致只审阅工具新生成或新增改的证明片段跳过完全未改变的旧路径最后跑一遍完整回归观察修复前后所有被引用文件的导出性质。只要维护者能说清“这次输入系统允许调整的是哪个契约项”修复过程就是可控的。这也正是 contract-aware 与暴力重写相比的本质区别。6. 我在实际评测和使用前会确认的清单6.1 先把版本和导入关系摸清楚带 Isabelle 概念的设计很容易忽略依赖版本变化、理论导入结构调整、外部库更换这些也可能导致证明失败。表面上你会看到 lemma 红掉但根因其实不在你自己的契约改动上。因此测试 CAPRI 之前我会先跑一次环境基线。确认在当前 Isabelle 版本下不修改任何契约的代码能否被完整验证。如果能再引入契约变更。接着检查导入关系避免修复工具在指定目录外访问到同名的旧理论。最后把自动生成的报告和 diff 日志保存下来。若失败出现在某个文件里而该文件的契约其实没变优先修复它的上游依赖。6.2 不要只盯单条 lemma要看批量结果如果系统需要同时处理几十个失败证明建议给每次修复定义一个批量结果表检查项说明可接受信号成功率新理论中需要修复的 lemma 总量里能被完整构建的数量越高越好但要有失败记录变更幅度修复后与旧证明 diff 的行数和被改 lemma 数同一问题下变化越集中越正常新增假设数工具通过给 lemma 添加前置条件来绕开契约变化新增假设与契约调整目标一致外部依赖变化修复时是否改动被其他文件导入的公共定理对公共定理的改动需要重点 review人工审阅成本新生成证明片段的可读性和注释完整性约低越好不适合只丢一个巨型求解命令回归稳定性整个理论库连续执行两次的结果输出结果和耗时无明显差异批量任务中最常踩的坑是并发跑多个修复时所有 lemma 同时使用同一个“以前可用的引理”而公共引理在修复过程中被自动改写。这样你会得到一片绿油油的结果但项目整体语义偏离很远。所以修复顺序也要保证依赖目录没有丢失。6.3 基于我踩过的一些坑给出几条第一原则如果需要用一个句子反映什么值得用什么不值得我会这样描述把 CAPRI 当成一个把失败范围收窄到可控修复对象的研究性工具而不是一键解决所有验证工程问题的正式软件依赖建议先从规模较小的契约边界入手观察它对简单函数重构的修复情况。之后每次升级尽量将“代码变化”和“契约变化”分开提交。当 a 和契约同步改动时CAPRI 类工具的映射难度会急速上升。你可以在版本管理中先把契约名、类型表达式和引理头记录进说明文件的 metadata让修复系统之后能更容易对齐。还有如果你不是理论证明维护者而只是一个临时被征调来补证明的工程师我给你的建议是先不打 CAPRI。先去看对应文件里契约当前承诺什么再判断旧证明的失败是环境升级造成的语法问题还是真实现的语义变化。后者的修复往往需要在断言层面重新取舍自动工具只能帮你处理大量重复、耗时的机械旋转部分。今天记录这些主要是想让人看到“契约感知证明修复”为什么值得理解。它的核心不是把apply auto换成另一个更强方法而是用一种能反映用户意图的方式维护长期验证工程。我认为这条路代表着 Isabelle 等证明助手走向大规模实践的必要方向。等这类工具真正支持普通理论库规模的运行维护成本才可能真正被降下来。