通过证明迁移代码：从F#到Python

我们构建了一个原型，通过定理证明而不是测试套件来验证代码迁移。一个编码代理将程序用另一种语言重写，一个确定性翻译器将原始代码和重写代码都转换为Lean，然后定理证明器证明两者在所有输入上计算结果相同。翻译器处理F#和Python的限制子集，并将它们的浮点数建模为精确实数（ℝ）；它不包含语言模型，因此Lean是每个源代码的忠实、可检查的渲染。

整个流程：两个实现都变成Lean，定理证明器证明它们在所有输入上等价。编码代理迭代直到证明成功。

这将代码迁移转化为证明义务。你不是希望重写行为正确，而是声明一个定理，即它在所有输入上与原始代码匹配，然后让机器解决：Logos Agent证明定理，或找到反例。

我们的运行示例是iCPPI，一种投资组合保险算法。我们从F#实现和编码代理编写的Python重写开始，用确定性翻译器将两者转换为Lean，陈述等价定理，并证明它。证明由我们的自动化证明系统产生，它将目标分解为引理蓝图并在Lean中处理每个；这里运行了约22,000个机器检查字符。

1. 问题：“我们重写了它，它仍然是同一个程序吗？”

迁移是常规操作，但很少让人放心。一个用F#编写的模型被移植到Python，以便数据科学团队维护；原型用更快的语言重新实现；旧服务在新运行时上重建。问题总是相同的：新东西和旧东西一样吗？

我们通常使用的工具回答的是比我们正在问的问题更弱的问题：

测试对输入空间进行采样。绿色套件表示两个程序在你想到要检查的输入上一致。破坏迁移的输入，恰恰是没有人编写测试的那个。

对历史数据输出差异有同样的差距（只有实际发生的输入），并且直到重写完成并连接后才能运行。

手动代码审查无法扩展到非平凡算法，并且给出的是确信而非证明。

我们想要说的是更强的：新程序对每个可能的输入返回与旧程序相同的答案。这不是测试；这是一个定理，一个对所有输入全称量化的陈述。要证明这样的定理，你需要两个程序作为同一逻辑中的数学对象，其中“在所有输入上相等”是一个机器可以检查的声明。产生这些对象，可重复且以你可以对照源代码检查的形式，是我们的翻译器所做的。

关于“相同”在此含义的说明，在§2中精确：我们将程序比较为实数上的函数，所以“相同”意味着相同的数学函数，而不是相同的浮点位模式。

1. 为什么是Lean，为什么是实数（ℝ）？

我们的目标是Lean 4与Mathlib，其大型形式化数学库。Lean是一个证明助手：你不断言两个函数相等，你证明它，内核检查每一步。Mathlib之所以重要，是因为真正的程序做真正的算术（比较、除法、根），而Mathlib已经拥有我们推理所需的实数理论。

第二个决定更具后果：我们翻译到精确实数（ℝ），而不是浮点数。

文字0.1变成精确实数1/10，而不是最近的IEEE-754双精度。模型中没有舍入，没有浮点非结合性使等价证明复杂化。

sqrt, exp, log变成真正的Real.sqrt, Real.exp, Real.log，它们的实数定理可用。

直白地说：在ℝ上推理证明算法等价性，即两个程序实现相同的数学函数，对于大多数迁移来说这正是问题（我们是否忠实地重新实现了算法？）。它不证明逐位浮点身份，而这两者是真正不同的声明：证明作为ℝ上的函数相同是一回事，而证明两个程序在目标抽象之下，在它们实际计算的方式上一致，是另一回事，且困难得多。

那个较低的差距不是浮点数能为你关闭的，即使在同一标准下。IEEE 754固定核心操作（加法、乘法、除法和平方根是正确舍入且可移植的），但有意将超越函数如exp和log留作实现定义，因此两个标准兼容的数学库可以对相同输入返回最后一位不同的结果（“制表者困境”）。因此，跨平台逐位身份甚至没有明确定义。在ℝ上建模故意跳过那一层，并问迁移通常需要的问题：两个程序是否表示相同的实值函数？当位本身是感兴趣的对象时，例如校验和或定点账本，你应该针对机器浮点数。

1. 运行示例：iCPPI

iCPPI是一种投资组合保险策略：管理账户，使其参与风险资产（权益）的上行，同时从不跌破保护底线。每个期间你按市值计价账户，更新高水位线，计算规则允许的风险敞口，并在权益和债券之间再平衡，但仅当隐含漂移足够大以保证交易时。细节很重要，一个周期偏差错误容易犯且难以捕捉。我们的转录遵循iCPPI规范的算法1。

在我们的迁移故事中，原始代码是F#，函数式风格：递归循环折叠价格列表，传递账户状态（h, ns, nb, v, b）通过每个周期。（摘录；…表示省略的绑定如em，以及辅助函数rmin/rmax/rabs定义在上面。）

F#

let rec loop (beta: float) (m: float) (emax: float) (delta: float) (rho: float) (h: float) (ns: float) (nb: float) (v: float) (b: float) (prices: float list) : float * float = match prices with | [] -> (v, h) | p :: rest -> let b = b * rho in let vm = ns * p + nb * b in let em = ns * p in let h = rmax h vm in let cm = vm - beta * h in let estar = if cm < delta then cm else emax * vm in let … = if (cm > delta) || (em > emax * vm) in … loop beta m emax delta rho h ns nb v b rest

重写是Python，命令式：带有可变状态的for循环遍历价格序列。（摘录；…表示省略的初始分配nS, nB，以及循环中的B, Em, g。）

Python

def icppi(V0: float, beta: float, m: float, emax: float, delta: float, rho: float, S: list[float]) -> tuple[float, float]: H = V0 nS = Estar / S[0] # 初始；Estar刚刚计算 … for t in range(1, len(S)): B = rho ** t Vm = nS * S[t] + nB * B Em = nS * S[t] H = max(H, Vm) Cm = Vm - beta * H if Cm < delta or Em > emax * Vm … return V, H # (最终值，最终高水位线)

两者之间的对应关系不明显。它们范式不同（递归折叠 vs. 变异循环），计算形状也不同。F#循环乘性地滚动债券因子（每个周期b := b * rho，从初始1.0开始），而Python将其重新计算为B = rho ** t。这些碰巧表示相同的值，但你必须检查。这就是关键：两个诚实、习惯的实现，人类必须费力地信任。它们是否是相同的函数？§5将其变为定理。

（为减少符号摩擦：相同数量在三种设置中有不同名称，所以Python V0/S/H是F#/Lean v0/prices/h。它们分别表示初始值、价格序列和高水位线。）

1. 确定性翻译及其作用（和不能作用）

4.1 流水线

两个前端共享一种形状。源代码被解析为语言无关的JSON AST；一个小型Lean读取器将其转换为类型化的Lean数据；一个发射器打印Lean，浮点数建模为ℝ：

Python前端重用CPython自己的ast.parse。输入实际上是有效的Python（同一文件在CPython下运行），我们从未重新实现Python的语法；Python的解析器是真相来源。发射器产生命令式Lean模型（Id.run do with let mut/for/if）。

F#前端没有等价物：F#没有通用的独立AST导出器，所以我们为支持的子集编写了一个小型标记器和Pratt（优先级爬升）解析器。它发射递归Lean def with match。

4.2 生成的Lean的样子

输出不是不透明的：它是可读的Lean，缩进，每个源定义对应一个定义。这里是F#的rmin辅助函数和循环折叠的开头，完全按照发射的样子：

Lean

noncomputable def rmin (a : ℝ) (b : ℝ) : ℝ := if (decide (a < b)) then a else b

noncomputable def loop (beta m emax delta rho h ns nb v b : ℝ) (prices : List ℝ) : ℝ × ℝ := match prices with | [] => (v, h) | p :: rest => let b := (b * rho) let vm := ((ns * p) + (nb * b)) let h := (rmax h vm) … loop beta m emax delta rho h ns nb v b rest

你可以对照F#逐行阅读，对应关系一目了然；这就是支持忠实性论点的可检查性。类型直接映射：float → ℝ, int → ℤ, bool → Bool, list t → List t, tuples → ×。由于F#对float和int使用相同的运算符，F#翻译由所需的类型注释驱动：float变成ℝ，这固定了其上的每个运算符的含义。（decide (…) 包装出现是因为ℝ上的顺序不可计算，所以像a < b这样的比较是一个Prop；在open scoped Classical下，decide 将其转换回Bool。）

4.3 两个正确性后盾

我们并不要求你盲目相信发射器。每个生成的规范背后都有两个独立检查。

它针对Mathlib进行类型检查。构建规范时通过Lean的精化器针对真实的Mathlib运行。翻译错误，无论是错误的元数、类型不匹配还是格式错误的项，都无法编译。这免费排除了一大类翻译错误（当然，它不能捕捉一个类型正确但语义错误的翻译）。

已证明的健全性引理。对于辅助函数，我们进一步证明生成的Lean意味着它应该的含义：F#的rmin/rmax/rabs变成Lean函数，我们证明它们是ℝ上的min、max和绝对值：

Lean

lemma rminEqMin (a b : ℝ) : rmin a b = min a b := by unfold rmin rw [min_def] simp only [decide_eq_true_eq] split_ifs with h1 h2 h2 first | rfl | linarith

这个引理已完全检查，没有sorry。这是一个机器验证的陈述，即发射器对比较和分支的渲染表示了意图的函数。

1. 通过证明迁移：定理及其证明方式

这里是成果。

翻译后，iCPPI的两个版本都是具有相同签名的Lean函数：

(v0 beta m emax delta rho : ℝ) (prices : List ℝ) : ℝ × ℝ

即六个实数参数和一个价格列表输入，一个（值，高水位线）对输出。（机械点：F#生成的定义位于命名空间FSharp下，因此两个icppi可以共存于一个文件中而不会发生名称冲突。）

迁移正确性声明是一个定理。它引用了实际生成的规范，即来自Python翻译的顶级icppi和来自F#翻译的FSharp.icppi，而不是任何改写：

Lean

-- icppi : from examples/icppi.py (the Python rewrite) -- FSharp.icppi: from examples/icppi.fs (the original F#)

theorem icppi_agrees (v0 beta m emax delta rho : ℝ) (prices : List ℝ) : FSharp.icppi v0 beta m emax delta rho prices = _root_.icppi v0 beta m emax delta rho prices

仔细阅读该陈述。变量是全称量化的：该等式对于六个参数和每个价格列表的每种组合都成立，包括任何长度和任何值，甚至空列表。没有抽样，没有代表性数据集。它表明F#和新Python在算法可能看到的每个输入上计算相同的（值，高水位线）对。

证明是如何产生的

我们没有手动编写这个证明。它由我们的自动化证明系统产生，该策略是首先用对原程序的结构归纳来引导证明，然后用一些算术推理来完成。整个证明大约22,000个字符，完全由机器检查。