透過證明遷移程式碼：從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個字元，完全由機器檢查。