开发者用 Lean 形式化 Julia 源码，在 Base 库中发现 400 个 bug

我也尝试过为Julia本身做这件事——用Lean形式化完整的源代码。 是Base的全部源代码，还是Julia的全部源代码（包括编译器和C运行时）？ 这是目标，没错。仓库里有Base和部分stdlib的内容，其余的我还在本地继续做。C运行时那部分还处于相当早期的阶段。

这太了不起了。我自己也一直在用基于clanker的方式对我自己的包PortfolioOptimisers.jl做正确性检查。我觉得在完成检查并稳定库之后，这是一个很好的下一步。

Julia里很多抽象类型没有精确的接口定义。（比如，一个Number有哪些性质并不清楚。）没有这个，你怎么能证明接受这类类型的函数有什么性质？ 证明往往不是针对抽象类型的，因为正如你所说，它们很多时候没有精确的接口。

以下是目前正在做形式化的AI给出的更详细解释：

针对抽象类型的一般性证明是不可能的，这个项目也不尝试这么做。没有任何陈述是关于“每一个Number”或“每一个AbstractArray”的。泛型代码以两种方式之一出现。

1. 具体类型。大多数性质是关于具体的Base类型的：Int8到UInt128、Float64、UnitRange{Int}、StepRange、Dict、String等等。这些类型的行为完全已知，因为它们的方法定义在Base中，一直到底层内在函数。Lean模型逐行镜像这些方法体，所以关于length(::StepRange{Int8,Int8})的定理是关于真实代码的陈述。发现的大多数bug都属于这一类，比如typemin/typemax附近的溢出、空范围、错误的异常类型。

2. 在给定假设下的泛型函数。当一个Base函数调用用户定义的方法时，这些方法成为Lean模型的参数，定理会指明它需要它们具备哪些性质。例如，将isless扩展到missing（missing排最后）被证明对任意元素类型都是严格弱序，前提是该元素类型自身的isless是严格弱序： def IslessStrictWeak : Prop := ∀ (α : Type) (lt : α → α → Bool), StrictWeak lt → StrictWeak (islessM lt) 这个假设就是接口。如果文档从未说明它，定理会把它明确写出来，而违反它的用户类型就不在声明范围之内。

接口模糊的地方。有时不清楚docstring承诺了什么，或者一个反例需要的输入可能超出了预期契约。在这些情况下，bug报告会把疑问记录在maybe_intended字段中，而不是直接称之为bug。相当多的发现属于这一类，它们与明确的错误结果和崩溃报告分开保存。

所以这些证明对抽象接口本身没有任何说明。它们覆盖的是具体的Base代码，或者相对于对其所调用方法的明确陈述假设而言的泛型Base代码。

Lean的一个很酷的地方是，你可以把假设当作参数传给定理或定义，所以你可能只在该假设（一个hypothesis）下证明某个性质。

例如，在上面第(2)点中，lt是用户提供的任意排序。定理把“lt是严格弱序”作为假设，并证明建立在它之上的missing感知isless也是严格弱序。

但请注意，这不像Mathlib那样是纯数学。Lean是一个证明检查器，所以它可以检查关于任何东西的陈述，包括代码。它基本上就是在检查“如果我假设这个东西，以及另一个东西，而代码看起来是这样，那么这个一般性质是否满足？”

题外话，我的一个学生做了一个学习Lean的互动游戏：https://leangame.autumnofautumn.com/。我觉得它有助于更好地直觉理解Lean证明是如何工作的。

非常酷！我对它效果这么好感到震惊！

所以，对我来说关键问题是：形式化模型如何与代码库并存，并随之演进？

你花了大约5000美元的token，带回来一份非常令人印象深刻的bug列表。推测这种方法也会产生相当数量的假阳性（模型比代码的意图更雄心勃勃，即它把一个footgun标记为bug；注意，通常人类作者集体对此也没有共识！有时某件事是不是bug并没有客观真理）和假阴性（为了让它工作，需要相当多的假设——这不是“一直到RISC-V形式化模型”那种让LLM使形式化软件验证在更大规模上变得可行，也不是“一直到ZFC”那种纯数学的Navier-Stokes爆炸问题）。

对每个版本都从头做同样的事情扩展性不太好。扩展性很好、而且我认为是软件工程未来的做法，是让形式化模型+证明持久存在，实际上是作为代码库的一部分；这样比如一个PR或下游（即使用Julia Base的代码）可以低成本地被检查。

这需要一些机制（如果代码库随着一系列diff变化，我们如何“提升”这些diff，让模型/证明沿着这条路径迁移？）。

我认为这还需要中间一个额外的半形式化步骤：一个更人类可读的、自然语言版本的Lean模型。目前你是在“模糊的docstring/开发者意图”↔“形式化模型”之间走；我认为更有帮助的是走“模糊的docstring/开发者意图”↔“减少歧义的扩展docstring”↔“形式化模型”。

这把路径拆成了“推断/澄清代码的意图”和“对澄清后的意图进行形式化建模”；两步都是AI产出/AI辅助的，但两步所需的技能集非常不同，而且“澄清代码的意图”这件事如果不是完全形式化的Lean，在人与人之间讨论起来更容易。

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）