通過證明遷移代碼：從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個字符，完全由機器檢查。