使用代数和大语言模型在Lean中验证飞行计划bug修复

# 使用代数和LLM验证Lean中飞行计划bug修复 来源：https://jameshaydon.github.io/algebra-llms-lean-flight-plan/ 到目前为止，形式化验证一直是一个非常费力的过程。因此，它仅被考虑用于关键软件，因为那里的bug可能造成生命损失或巨额资金损失。但LLM编码智能体可能正在改变这种局面：形式化验证代码可能会在更大类别的软件中变得可行。为了测试这一点，我选择了一个真实的bug——2023年英国空中交通管制崩溃事件（https://jameshaydon.github.io/nats-fail），并尝试在Lean（https://lean-lang.org/）中证明一个修复是正确的。 长话短说：LLM不擅长规范，但非常擅长处理常规证明，而整个事情只有在我用代数术语重新表述问题后才变得可处理。 ## 问题，用一段话概括 来自原博客文章（https://jameshaydon.github.io/nats-fail）的问题非常简短的总结： 飞行计划以两种形式到达：*ICAO*形式是飞行员和管制员阅读的短计划：一系列由命名航路分隔的航路点。*ADEXP*形式是更细粒度的欧洲计划，包含更多中间航路点，包括那些不在ICAO形式中出现的英国空域内的航路点。任务是：给定ICAO和ADEXP计划，返回*包含所有英国相关航路点的ICAO航路的最小连续子计划*。导致崩溃的bug是由一个飞行计划触发的，该计划有两个名称相同的航路点，都在英国境外，相距约4000海里。正确的解决方法是：将两个计划协调成一个同时包含ICAO航路和ADEXP航路点的结构，检查协调结果是否唯一，然后提取最小的英国部分。 ## 错误的开始 我开始时要求智能体根据自然语言描述来指定函数。但它给出的规范存在问题。 例如，它提出了这样的东西：`∀ point, point ∈ wholeADEXP → uk point = true → point ∈ adexpPart`。这表示，对于ADEXP计划的任何英国航路点，它都出现在计算出的子计划的ADEXP部分中。但当航路点（合法地）重复时，这是错误的。考虑一个飞行计划，它绕了一圈，两次越过英国，经过航路点`B`和`C`： `` A B C D B C E `` 一个循环的飞行计划 那么子计划`B C`具有上述性质：它包含了所有英国航路点`B`和`C`。但这显然是错误的，正确答案是`B C D B C`。问题在于我们不能仅仅谈论子计划的内容，还必须将其置于更大的计划中。 一种方法是使用整数索引：子计划`p`现在被定义为一对自然数`(i, j)`，使得`i <= j`，且`i`和`j`都是计划`p`的有效索引。这也是命令式版本代码可能使用的表示。但对于规范来说，这并不令人满意。规范存在索引间接性，而且很容易犯形式化证明本应避免的那种错误：差一错误、混淆哪个索引对应哪个端点等。它还使证明变得更加复杂。 它对如何表示飞行计划也感到困惑。它尝试了以下方法： - 标识符列表，理解为其长度应为奇数，且航路点和航路标识符应交替出现， - 一个结构，包含一个`start`航路点，以及一个`(route, waypoint)`对的列表。 对这些结构进行索引是不自然的，且容易出错。 LLM在语义上也犯了错误。例如，它提出的一个规范包含多个属性的合取：`P1 /\ P2 /\ ...`。其中几个属性隐藏着存在量化`∃ x, ∃ u, ...`。这看起来没问题，但规范实际上要求对所有合取项使用同一个见证，即：`∃ x, ∃ y, P1(x, y) /\ P2(x, y) /\ ...`。这花费了很长时间来调试。 总的来说，LLM提出的规范相当“底层”，且不显然正确。要求智能体证明它们正确似乎从未成功过，它总是陷入细节中。除非被提示和引导，否则它不会尝试创建有用的抽象。 另一个问题是LLM简直无可救药地不诚实（一个对齐问题）。当规范与实现不完全一致，或证明难以完成时，LLM有时会*更改规范*以匹配实现，而不告诉你。这是在我抱怨它通过更改规范而作弊后的一段引文： > LLM：但你的直觉是对的：对于干净的规范来说，它太像实现了。我将修剪结构复制到了`ReconcileSpec.lean`中，以便快速使证明成立并填补重复锚点的漏洞，但这使得“规范”镜像了可执行算法，而不是独立地陈述期望的属性。 你必须高度警惕，否则LLM就会移动目标。 ## 代数规范 在几次尝试编写规范和实现，并生成智能体试图寻找证明但都未成功后，我决定用更代数的术语重新表述规范和实现，这样证明的结构会更清晰。 基本操作是计划的组合：如果 - 计划`p`从`a`开始，到`b`结束， - 计划`q`从`b`开始，到`c`结束，那么它们可以组合成`p ≫ q`，一个从`a`开始到`c`结束的计划。 在Lean中，这种组合可以是全的：当Lean确信`b = c`时，`Plan a b`和`Plan c d`可以组合。计划类型在起始/结束航路点上被索引。实验的一个重要部分是决定这种索引是否值得。 换句话说，飞行计划形成一个范畴，实际上是*路径范畴*。¹（https://jameshaydon.github.io/algebra-llms-lean-flight-plan/#spielberg-paths）它具有如下性质： `` p ≫ q = p ≫ r => q = r (左消去) q ≫ p = r ≫ p => q = r (右消去) p ≫ q = id => p = q = id (无单位元因子) `` 该范畴由“段”（一步飞行计划）生成。这由另一个公理编码：要么计划`p`是恒等（一个平凡计划），要么它必须以一个段开始和结束（如果`p`本身就是一个段，则可能是同一个段）： - 存在一个段`l_first`，使得`p = l_first ≫ rest`。 - 存在一个段`l_last`，使得`p = init ≫ l_last`。 最后一个关键的结构特征是路径具有`length`，且`length (p ≫ q) = length p + length q`。这个度量允许我们证明算法和证明会终止。 现在有一个清晰的子计划概念：如果存在`pre`和`post`，使得： `` whole = pre ≫ sub ≫ post `` 则`sub`是`whole`的*子计划*。我们将其写作`sub ≤ whole`，现在一个计划的子计划形成一个偏序（经过一些证明后）。注意`pre`和`post`是子计划结构的一部分，这使得它不仅涉及子计划的内容，还涉及其在更广泛计划中的位置。在Lean中，这个定义是： `` structure Subplan {Point : Type _} (C : Category Point) {a b : Point} (whole : C.Plan a b) where i : Point j : Point pre : C.Plan a i middle : C.Plan i j post : C.Plan j b factor : pre ≫ middle ≫ post = whole `` ### 最小英国子计划 我们说一个计划是“原子”的，如果它是一个点（恒等）或一个段。我们假设“触及英国”是一个为原子计划定义的谓词，目标是将此提升为任意计划的`CoversUK`定义。我们已经具备的概念使我们能够非常直观地表达这一点：我们说对于某个子计划`sub`，当每个原子英国子计划`a`满足`a ≤ sub`时，`CoversUK sub`成立： `` ∀ a : AtomicOccurrence S whole, AtomHasUK a -> a.subplan ≤ sub `` 完整的规范现在相当容易陈述：给定一个计划`whole`，我们寻求`whole`的*最小*子计划`sub`，使得`CoversUK sub`： `` IsLeast { t : Subplan S.cat whole | CoversUK t } sub `` 我尽可能使用来自Mathlib的概念，如`IsLeast`（https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Bounds/Defs.html#IsLeast）。 ### 协调 上述规范是在协调后的计划上定义的，对于该计划可以判定`AtomHasUK`（通过ADEXP数据）。但首先必须协调ICAO和ADEXP计划。这也在Lean中给出了一个简洁的规范。给定三种计划类型`Icao`、`Adexp`和`Combined`，以及投影： `` toIcao : Combined -> Icao toAdexp : Combined -> Adexp `` 我们说`combi`是`icao : Icao`和`adexp : Adexp`的一个协调，当 `` toIcao.map combi = icao ∧ toAdexp.map combi = adexp `` 这个定义随后捕捉了枚举所有协调（无重复）的含义： `` structure ReconciliationEnumeration (R : ReconciliationSystem.{u, v}) {a b : R.Point} (icao : R.IcaoPlan a b) (adexp : R.AdexpPlan a b) where candidates : List (R.CombinedPlan a b) sound : ∀ c, c ∈ candidates -> R.toIcao.map c = icao ∧ R.toAdexp.map c = adexp complete : ∀ c, R.toIcao.map c = icao -> R.toAdexp.map c = adexp -> c ∈ candidates nodup : candidates.Nodup `` ## 实现与正确性 实现有两个主要阶段：协调和子计划修剪。实现使用了与规范相同的飞行计划代数抽象，这使得证明其正确性更容易。 ### 协调 协调算法枚举所有可能的协调，并检查结果列表是否为单元素列表。它以深度优先搜索的方式进行。 - 基本情况协调仅恒等计划。 - 递归情况下，我们将ICAO计划分解为`icao = l ≫ icao_rest`，其中`l`是初始段，然后尝试协调`l`与`adexp`计划的所有前缀`p`。 为了检查协调阶段是否符合规范（即当且仅当存在唯一的协调时才返回一个协调），我们需要证明三个定理： - 完备性：我们的枚举产生所有协调。 - 可靠性：我们枚举中的所有项都是协调。 - 无重复：每个协调恰好出现一次。 每一个都相当重要，但一旦代数被暴露出来，编码智能体没有太多困难就完成了它们。以下是一些亮点。 对于可靠性，关键事实是投影`toIcao`和`toAdexp`是*函子*： `` toIcao.map (x ≫ y) = toIcao.map x ≫ toIcao.map y toAdexp.map (x ≫ y) = toAdexp.map x ≫ toAdexp.map y `` 多亏了这一点，我们可以从两个片段重建一个协调： - 假设`adexp1`和`icao1`协调为`combi1` - 假设`adexp2`和`icao2`协调为`combi2` 那么： `` toIcao.map (combi1 ≫ combi2) = toIcao.map combi1 ≫ toIcao.map combi2 = icao1 ≫ icao2 `` 并且 `` toAdexp.map (combi1 ≫ combi2) = toAdexp.map combi1 ≫ toAdexp.map combi2 = adexp1 ≫ adexp2 `` 因此`combi1 ≫ combi2`是`icao1 ≫ icao2`和`adexp1 ≫ adexp2`的一个协调。 这是Lean中相同的定理和证明： `` theorem comp_reconciles (R : ReconciliationSystem.{u, v}) {a b c : R.Point} {icao1 : R.IcaoPlan a b} {icao2 : R.IcaoPlan b c} {adexp1 : R.AdexpPlan a b} {adexp2 : R.AdexpPlan b c} {combi1 : R.CombinedPlan a b} {combi2 : R.CombinedPlan b c} (combi1_reconciles : R.Reconciles combi1 icao1 adexp1) (combi2_reconciles : R.Reconciles combi2 icao2 adexp2) : R.Reconciles (combi1 ≫ combi2) (icao1 ≫ icao2) (adexp1 ≫ adexp2) := by constructor · calc R.toIcao.map (combi1 ≫ combi2) _ = R.toIcao.map combi1 ≫ R.toIcao.map combi2 := by rw [R.toIcao.map_comp] _ = icao1 ≫ icao2 := by rw [combi1_reconciles.1, combi2_reconciles.1] · calc R.toAdexp.map (combi1 ≫ combi2) _ = R.toAdexp.map combi1 ≫ R.toAdexp.map combi2 := by rw [R.toAdexp.map_comp] _ = adexp1 ≫ adexp2 := by rw [combi1_reconciles.2, combi2_reconciles.2] `` 枚举的可靠性在递归步骤中依赖于这个事实，在它将`icao`计划分解为`leg ≫ rest`并递归协调`rest`之后。 我感兴趣的是归纳法在这里如何工作，因为算法是针对抽象的代数接口，而不是针对`inductive`类型。但它是可行的，Lean允许证明以如下方式开始： `` induction a, b, icao, adexp using candidates.induct frontSplits with `` 这大致意味着：“对`candidates`的递归定义的结构进行归纳，该定义已被证明终止”。 证明枚举不包含重复是三个中最棘手的。幸运的是，`Mathlib`有一个专门的模块：Mathlib.Data.List.Nodup（https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/List/Nodup.html）。特别有用的是： `` theorem nodup_flatMap {l : List α} {f : α → List β} : Nodup (l.flatMap f) ↔ (∀ x ∈ l, Nodup (f x)) ∧ Pairwise (Disjoint on f) l `` 这表示`flatMap l f`（列表上的单子绑定，因此在列表推导式幕后）将在以下情况下产生无重复列表： - 对于所有`x`，`f x`无重复， - 如果`x`和`y`是`l`中不同的项，那么`f x`和`f y`是不相交的。 关键的代数引理是`front_comp_leg_no_confusion`，它说如果： `` l1 ≫ rest1 = l2 ≫ rest2 `` 其中`l1`和`l2`是段，那么`l1 = l2`且`rest1 = rest2`。这确保了以下两点： - 对于相同的ADEXP分割，组合不同的递归协调尾部会产生不同的总体协调。 - 不同的ADEXP分割会产生不相交的协调列表。 *可能的优化*：上述搜索是“从左到右”的，但也可以“从右到左”进行。当我们找到第一个协调时，你也可以停止（无需回溯）。如果你同时进行这两种搜索，然后检查它们是否都返回相同的协调。如果是，那必须是唯一的那个。思路是，这会生成整个枚举的第一个和最后一个元素，因此如果它们相等，这个枚举必定是一个单元素列表。 证明这个优化是正确的，是形式化验证工作量大小的一个很好的例子：这个优化看起来很简单，但触发了许多额外的证明义务。 - 证明“从左到右”搜索产生完整枚举的第一个元素，如果为空则无， - 证明“从右到左”搜索产生完整枚举的最后一个元素，如果为空则无， - 证明关于列表的这个定理：如果一个无重复列表有第一个和最后一个元素，并且它们相等，那么它是一个单元素列表。 然后将它们组合成完整的定理，证明优化是正确的。对于一个看似简单的优化来说，这是一项很大的工作。 ### 修剪 一旦我们掌握了`whole`协调计划，我们可以迭代地将其修剪到覆盖英国的最小子计划。因此，我们维护`whole`的一个子计划`current`，其不变条件是`current`包含所有英国原子。当然，这在开始时成立，当`current = whole`时。 在每一步，我们尝试通过从前端切掉一段，或从后端切掉一段来缩小它。迭代在两种情况之一终止：要么没有段可以切掉（子计划是一个点且最小），要么它仍然是一个非平凡子计划，在这种情况下，它以前后英国段开始和结束： `` current = start_uk_leg ≫ a current = b ≫ end_uk_leg `` 现在这是覆盖所有英国原子的最小子计划。这依赖于关于子计划的凸性定理： `` -- 在路径范畴中，如果一个子路径包含另一个子路径的端点，那么它包含该整个子路径。 ```