开一场代码评审会时有人把一个 PR 丢进仓库改动只有几行把 Isabelle/HOL 里的一个递归函数边界条件改了意图是“让 0 不再被视为一个合法特例”。你下意识觉得这种改动最多影响一两处调用。结果 CI 跑完屏幕上出现了一排红色 lemma原本能通过的证明全部失守。更麻烦的是它们并不是语义写错只是原来依赖的证明路径断了。在形式化验证项目里这可能是我见过最真实的痛点修改规范和定理证明的“维护成本”并不和代码行数成正比。哪怕只改了一个 case可能在另一条证明链上引起连锁反应。这就是所谓 Proof Repair证明修复问题。今天想借“CAPRI: Contract-Aware Proof Repair for Isabelle”这个题目聊清楚一个关键判断自动证明修复要想走出玩具阶段不能只靠搜索策略还必须理解“契约”。这篇文章不会教你背 CAPRI 的命令行接口也不保证它已经公开了开箱即用版本。因为 CAPRI 这个方向的真正价值是“设计思路”它可以被复用到任何 Isabelle/HOL 项目里。我会先讲清楚 Proof Repair 解决什么问题再用一个能直接跑的最小 Isabelle 例子演示契约变化导致证明破裂的全过程最后梳理 Contract-Aware 为什么比传统修复方法更本质。1. Isabelle 的 Proof Repair到底在解决哪种痛苦很多 CSDN 读者第一次接触 Isabelle是在论文里看到类似theorem add_commute这样的花哨证明。于是会形成一种错觉定理证明器就是把定理输进去自动出新定理其实真实工程不是这样的。Isabelle/HOL 里的理论文件.thy更像一份“可验证的代码库”。你既写fun、definition、datatype也用lemma和theorem表达你想证明的性质。每次运行isabelle build这些证明都会被重新检查一遍。问题在于数学函数定义一旦变化原先的证明脚本不一定还能工作。这类问题的本质是软件演化。在普通程序中重构之后有类型系统检查和单测兜底在定理证明项目中类型系统能抓类型错误但不能自动修复定理证明。一个 lemma 之所以成立往往依赖函数定义的递归结构、case分支顺序、某个simp规则是否可用。你改的不只是代码还是证明的“证据链”。Proof Repair 要做的事情可以定义得很朴素给定原理论 T、原证明 P以及变更后的理论 T’当 P 无法在 T’ 中证明原目标时自动生成一个能够在 T’ 中通过的新证明 P’。但朴素定义背后是一个高难度问题。普通程序修复可以只看语法和类型证明修复必须保证生成结果仍然是一个“合法证明”。这比普通代码修复多了一个不可协商的限制正确性是形式化的。所以 Isabelle 社区对这个方向非常感兴趣但成熟工具很少。早期做法很大程度依赖人工打开红了的 lemma观察报错尝试sledgehammer、try0、blast…… CAPRI 这个标题里的关键词就是在给“修复”加约束。它不打算盲目猜证明而是先找出“这次变更影响了哪些契约”再有目的地修复。2. 基础概念契约、Isabelle/HOL 与 Proof Repair要理解 CAPRI先要把这几个词拆开。2.1 Isabelle/HOL不只是证明编辑器Isabelle 是一个交互式定理证明框架最常用的对象逻辑是 HOL高阶逻辑。它采用 LCF 架构所有定理必须经过一个小核心检查。这意味着你不能“骗”过证明器就算用自动策略生成了证明脚本最终通过的定理依然是被核心验证过的。这带来一个工程后果一旦 lemma 失败失败原因不是“程序运行崩溃”而是“该证明策略无法在给定目标上构造出合法证明”。Isabelle 给出的错误信息通常比较底层经常需要从证明脚本一层层往前查。2.2 什么是“契约”软件工程里的契约通常指接口双方都要遵守的约定。把函数看成一个组件前置条件调用方必须满足什么条件例如x 0。后置条件函数保证返回什么性质例如result x。类型约束输入输出必须是什么类型。不变式在对象生命周期内始终成立的性质。在 Isabelle/HOL 里这些契约并不是某个专门的魔法字段它们由assumes、shows、definition、locale、class、fun方程共同表达。举个例子definition add_positive :: int ⇒ int ⇒ int where add_positive x y x y lemma add_positive_post: assumes 0 x and 0 y shows 0 add_positive x y unfolding add_positive_def using assms by auto这里assumes 0 x and 0 y是前置条件shows 0 add_positive x y是后置条件。有趣的是Isabelle 中一个 lemma 既是对源码规格的陈述也构成模块对外承诺的契约。当函数实现变化这条 lemma 能不能继续成立直接决定这个“承诺”有没有被打破。2.3 Proof Repair 与传统代码修复的差异传统代码修复面对的行为对象是“运行结果不符合测试预期”修复目标是让代码跑对。Proof Repair 面对的是“证明脚本和新的理论不一致”修复目标可能出现在多处函数定义写错了应该修代码。lemma 的后置条件太强新实现根本不能满足需要削弱结论或加强前置条件。lemma 的证明策略过期了目标其实成立但原本的auto/induct路径已经无法覆盖新的 case。第三种情况里如果 CAPRI 只是换一个更强的证明策略那它和sledgehammer没本质区别。它真正出彩的地方应该是识别出“这次契约变了所以你要判断到底是改代码、改规范还是改证明过程”。CAPRI 这个题目里的 Contract-Aware准确表达了这种判断能力。它不是把修复当成纯语法匹配而是把修复放到“契约变更”这个解释框架内。3. 一个“改了几行就让证明失效”的最小例子我们直接来做一个能跑通的实验。它会清晰展示一个看起来很小、甚至更加“合理”的函数修改如何让旧证明直接崩溃。3.1 原始理论先定义一个函数nextNat输入自然数 n输出 n1。theory CapriDemo_Original imports Main begin fun nextNat :: nat ⇒ nat where nextNat n n 1 lemma nextNat_atLeast_1: 1 ≤ nextNat n by simp end这很自然自然数加 1肯定大于等于 1。在这个版本里by simp可以轻松证明。假设我们的业务契约是nextNat的输出总是至少为 1。这条 lemma 就是该契约的抽象表达。3.2 一次“优化”现在产品经理说0 不是一个有意义的输入希望程序在输入 0 时返回一个“默认错误值”并对其它正常输入保持原来的行为。开发者随手把它改成输入 0 时返回 0输入Suc n时返回n 2。theory CapriDemo_V2 imports Main begin fun nextNat :: nat ⇒ nat where nextNat 0 0 | nextNat (Suc m) m 2看这个定义对于 n≥1它依然能保证输出≥1。你可能会觉得这条改动非常“局部”。但原来的 lemma 现在变成了什么它要求对所有自然数 n 都成立1 ≤ nextNat n而当n 0时nextNat 0 0结论显然不成立。所以在 V2 里原证明写进理论文件会直接失败lemma nextNat_atLeast_1: 1 ≤ nextNat n by simp即使simp能自动处理很多情况它也无法证明一条在新实现下为假的命题。这是形式化证明真正残酷的地方它不会像测试那样给你一个“反例警告”之后继续跑而是会把构建直接停在失败点。4. 修复该怎么做先判断契约而不是急着换 tactic如果你只是在编辑器里看到红第一反应可能是把simp换成auto或者上sledgehammer。但对这个案例来说换任何自动策略都没用因为命题为假。更理性的修复路径是问新实现是否仍然承诺“输出至少为 1”如果不是那么原来的契约就要更新。4.1 修复方向一加强前置条件如果产品语义允许n 0作为合法输入那我们可以把原 lemma 更新为如下形式lemma nextNat_atLeast_1_v2: assumes 0 n shows 1 ≤ nextNat n using assms by (cases n) simp_all这里的关键变化不是证明方法从simp换成了cases n而是我们在逻辑上新增了一条假设。也就是说契约从“对所有 n 输出 ≥1”变成了“当输入合法时输出 ≥1”。这个例子里cases n实际上只是在告诉 Isabelle考虑n 0和n Suc m两种情形。assumption排除掉n 0后剩下的情形交给simp_all自动处理。这种修复使得 lemma 依然成立但它其实是“约束调用方”。如果你不知道这是契约变化只把simp换成更强的sledgehammer是永远得不到通过结果的。4.2 修复方向二承认实现违反原契约如果合法输入包括 0那就不是证明的问题而是函数实现本身违反契约。此时正确的产出应该是反例而不是一个强行凑出来的证明。我们可以清楚地展示反例lemma counterexample_when_input_is_zero: nextNat 0 0 by simp text ‹因此在 n 0 时原契约 1 ≤ nextNat n 为假。›一个 Contract-Aware 的 Proof Repair 系统最该做的事就是在上面两种方向里做判断。如果修复候选给出一堆虽然能通过、但严重改变 original lemma 语义的证明反而会埋下更大的坑。这才是 CAPRI 标题中 “Contract-Aware” 的分量。普通程序修复系统可以只关心“能不能跑绿”定理证明修复系统必须关心“这个修复是否违背了原本的模块契约”。5. CAPRI 这类系统的一般处理流程因为 CAPRI 是一个研究型题目我不会假设你已经拿到了可执行包。下面这套流程是从论文标题和 Isabelle 工程实践里能提炼出的最合理抽象。CAPRI 如果按这个思路实现那么它的输入输出大致会是输入变更前的理论文件或提交版本。变更后的理论文件。一个或多个失败的 lemma 标识。契约信息通常由assumes、shows、函数定义、locale等结构提供。输出针对失败 lemma 的可执行修复建议对应一个能通过 Isabelle 核心检查的新证明脚本。如果实现违反了契约则输出反例或“契约冲突”提示而不是强行修复。处理过程大概可以拆成下面几步。5.1 第一步失败定位理论上Isabelle 可以一次性告诉你哪些 lemma 失败但失败原因往往没有精确到“哪一行定义变化导致”。第一层要做的是把失败目标、失败前已应用的 proof method、以及当前使用的定义和前置条件完整收集起来。5.2 第二步契约差异分析这一步是 Contract-Aware 的核心。对比变更前后函数定义如果从“无递归分支”变成“有特殊 case”那么旧证明中所有依赖“全称输入”的结论都可能被破坏。对比nextNat n n1与nextNat 0 0 | nextNat (Suc m) m2会发现新实现给 0 单独开了一个异常 case。后置条件在异常 case 下不再被满足。函数结果的“最低值”下限变了。系统如果把这种语义变化抽象出来就不会盲目尝试对所有目标应用auto而会先把受影响的范围缩小到与 0 case 相关的 branch。这就把搜索空间砍掉一大块。5.3 第三步生成候选修复修复不只是生成一个 tatic而是生成一个“语义可解释的补丁”如果原有 lemma 是新实现下的假命题返回“不建议在证明层修复”。如果加前置条件后成立则建议用户更新assumes。如果证明策略过时则重放证明脚本逐个策略段替换失效步骤。如果函数定义有多个构造 case考虑是否需要调整induct/cases策略。5.4 第四步核心验证与信息回滚候选修复最终仍要送进 Isabelle 核心做严格校验。只有通过验证的补丁才能作为最终输出。这个回滚机制很重要自动修复系统不能“几乎正确”一旦通过就必须是真正可以在理论文件里工作的证明。从这套流程也可以看出CAPRI 并不是要替代 Isabelle 现有自动策略。它是更高一层“修复调度器”。它决定要不要修、修代码还是修契约、用哪种策略修。而最终底层证明还是离不开 Isabelle 的策略引擎。6. 为什么 Contract-Aware 比通用“证明搜索”更关键有读者可能会问sledgehammer现在不是已经很能打了吗为什么还需要 CAPRIsledgehammer的原理是把当前目标发给多个外部自动证明器搜索后把结果翻译回 Isabelle 可验证的 tactic。它擅长“在目标已明确且成立的情况下找到一条可行证明路径”。但它的定位是“我帮你把证完的最后一公里跑完”它不会回答“这个 lemma 应不应该存在”。Proof Repair 真正难的一点是语义歧义。目标变红时可能有两类原因目标在新理论下其实成立只是没找到证明。目标本身在新理论下已不成立因为某个前置/后置条件被悄悄破坏了。前者是策略问题后者是契约问题。如果一个修复工具只处理前者它会浪费大量算力去尝试验证一个根本不成立的命题直到穷尽所有自动策略。如果一个修复工具能感知契约它能很快把你引到正确的元问题上。打个不严谨但容易记的比方普通程序测试挂了可能是测试代码写错也可能是被测代码写错。一个合格的工具不会只知道“重新跑测试”。对一个 Isabelle 项目而言auto、simp、blast、sledgehammer都像执行测试的 worker但 project 级别的 Proof Repair 需要的是一个能理解“合约是否被打破”的指挥者。CAPRI 的价值主张正是把它放到第一优先级。7. 工程建议把 Isabelle 证明维护纳入持续验证如果你看到这里说明你已经在把 Isabelle 当成严肃工程来使用。这时候最好的状态是不要等问题爆发再手工打开编辑器红色一片而是把证明维护纳入日常验证。一个最小目录结构可以是这样capri-demo/ ├── CapriDemo_Original.thy ├── CapriDemo_V2.thy └── ROOT其中ROOT文件定义一个 session把两个理论都放进去session CapriDemo HOL theories CapriDemo_Original CapriDemo_V2在本地可以用下面命令在 jEdit 里打开单个理论isabelle jedit -l HOL CapriDemo_V2.thy要跑整个 session可以执行isabelle build -d . CapriDemo这是把定理证明放进 CI/commit 前检查的基础。你可以建一个很小的脚本#!/usr/bin/env bash set -euo pipefail isabelle build -d . CapriDemo || { echo Isabelle proof check failed exit 1 }这只是最基本的“证明回归”检查。除了把构建跑绿还有几个实战建议。7.1 把契约集中表达方便 diff在代码中不要把所有约束都藏在by auto的实现细节里。尽量用assumes/shows把它们显式化。这样每次改动后git diff能显示契约变化的位置也让未来的自动修复系统更容易定位。7.2 优先写结构化 Isar 证明直接用apply (auto)堆策略前期很爽后期很难维护。结构化 Isar 证明虽然写起来长一点但每一个 proof step 都对应清晰的逻辑关系。举例同样是修复 V2 中的 lemma如果写成 Isar 风格会更容易看出“我加了前置条件排除了 n0 分支”lemma nextNat_atLeast_1_isar: assumes n ≠ 0 shows 1 ≤ nextNat n proof - obtain m where n Suc m using assms by (cases n) auto then show ?thesis by simp qed这样的证明即使以后函数再变人也能快速看出为什么需要n ≠ 0因为只有非 0 输入能保证后置条件。7.3 使用 Quickcheck/Nitpick 做反例检测当某个 lemma 在新实现下失败不一定马上冲去改证明。先用反例工具验证它本身是否还成立。lemma nextNat_atLeast_1_false: 1 ≤ nextNat n nitpick oopsnitpick会为n 0生成反例。看到反例你就能明白这不是证明技巧不够而是陈述本身在新实现下已经不成立。这种前置判断能省下大量无效尝试。8. 常见问题与排查思路下面整理几个在实际使用 Isabelle 和维护证明时最容易遇到的问题问题现象可能原因排查方式解决方案lemma 在函数定义改动后变红新实现改变了某个 case 的语义查看 git diff确认改动的是前置条件还是定义分支先判断原陈述是否仍为真为假则更新契约为真则调整证明策略加by auto依然过不了目标需要归纳证明或引入额外引理对变量尝试induct n或cases n按递归结构拆分 case必要时把关键性质先单独证明by simp失败但sledgehammer能搜到证明缺少中间引理或外部证明器找到了某种组合路径用try0、sledgehammer搜索候选证明可在本地生成证明但建议把关键中间命题显式化成 lemma修复某个 lemma 后另一个 lemma 又失败证明之间存在依赖关系查看后续 lemma 是否using了旧版本说明按依赖顺序自底向上修复优先证明更基础的性质nitpick/quickcheck给出反例当前目标在给定公式中并不成立审视前置条件是否过弱或函数实现是否违反契约优先修正前置条件或回滚函数实现排查 Proof Repair 问题时最高效的口诀是先判断陈述的真假再判断策略是否有效最后才是改证明脚本。顺序一旦反了很容易在假命题上浪费几个小时。9. 总结与后续学习方向CAPRI 这个工具虽然名字里带 Isabelle但它真正值得学习的地方是方法论自动修复证明时系统必须感知契约变化并据此决定是改代码、改契约、还是改证明策略。这是从“搜索证明”上升到“理解软件演化”的一步。如果你手头没有现成 CAPRI release也别急着写“求安装包”。更好的实践路径是先熟悉 Isabelle/HOL 的基本理论文件结构和lemma/fun/definition写法。把一个实际项目中的函数定义改动和 lemma 失败记录下来观察失败模式。用nitpick先排除假命题。再尝试sledgehammer和结构化 Isar 修复。最后把这些经验抽象成自己的 Proof Repair 检查清单。形式化验证一旦进入长期维护阶段“证明修复”就是一个无法回避的工程成本问题。CAPRI 开了一个好头它让我们重新思考自动修复不能只看 strategy更要看 contract。后续值得继续关注 Isabelle 社区在这一块的演变也要警惕“工具能自动修证明”这句话的另一面如果一条证明在新实现下已经不再为真最该修的不一定是证明而是那段悄悄改变了世界的新代码。