我々は、テストスイートではなく証明によってコード移行を検証するプロトタイプを構築しました。コーディングエージェントがプログラムを別の言語に書き換え、決定論的トランスレータが元のコードと書き換えコードの両方をLeanに変換し、定理証明器が両者がすべての入力で同じ結果を計算することを証明します。トランスレータはF#とPythonの制限されたサブセットを処理し、浮動小数点数を正確な実数（ℝ）としてモデル化します。言語モデルは含まれていないため、Leanは各ソースコードの忠実で検査可能なレンダリングです。
エンドツーエンドの流れ：両方の実装がLeanになり、定理証明器がすべての入力で等しいことを認定します。コーディングエージェントは証明が成功するまで反復します。
これにより、コード移行は証明義務に変わります。書き換えが正しく動作することを期待するのではなく、すべての入力で元のコードと一致するという定理を述べ、機械に解決させます：Logos Agentが定理を証明するか、反例を見つけます。
実行例はiCPPIです。これはポートフォリオ保険アルゴリズムです。F#実装とコーディングエージェントが書いたPythonの書き換えから始め、決定論的トランスレータで両方をLeanに変換し、等価定理を述べて証明します。証明は自動証明システムによって生成され、目標を補題の青写真に分解し、各補題をLeanで処理します。ここでは約22,000文字の機械検証が実行されました。
- 問題：「書き換えたが、まだ同じプログラムか？」
移行は日常的でありながら、安心できるものはほとんどありません。F#で書かれたモデルがデータサイエンスチームによって保守されるためにPythonに移植されたり、プロトタイプがより高速な言語で再実装されたり、古いサービスが新しいランタイム上で再構築されたりします。質問は常に同じです：新しいものは古いものと同じですか？
通常使用するツールは、私たちが尋ねている質問よりも弱い質問に答えます：
テストは入力空間をサンプリングします。緑色のスイートは、チェックしようと考えた入力で2つのプログラムが一致することを示します。移行を壊す入力は、定義上、誰もテストを書かなかったものです。
過去のデータに対する出力の差分も同じギャップがあり（実際に発生した入力のみ）、書き換えが存在して接続されるまで実行できません。
手動コードレビューは非自明なアルゴリズムにはスケールせず、確信ではなく証明をもたらします。
我々が言いたいことはもっと強いです：新しいプログラムは、すべての可能な入力に対して古いプログラムと同じ答えを返します。これはテストではありません。定理であり、すべての入力に対して全称量化されたステートメントです。そのような定理を証明するには、両方のプログラムを1つの論理内の数学的オブジェクトとして必要とし、「すべての入力で等しい」という主張を機械がチェックできるようにします。これらのオブジェクトを再現可能かつソースコードに対して検査可能な形で生成することが、トランスレータの役割です。
ここでの「同じ」の意味については、§2で正確に述べられています：プログラムを実数上の関数として比較するため、「同じ」は同じ数学関数を意味し、同一の浮動小数点ビットパターンではありません。
- なぜLeanか、なぜ実数（ℝ）か？
ターゲットはLean 4とMathlib、その大規模な形式化数学ライブラリです。Leanは証明アシスタントです：2つの関数が等しいと主張するのではなく、証明し、カーネルがすべてのステップをチェックします。Mathlibが重要なのは、実際のプログラムが実際の算術（比較、除算、根）を行うため、Mathlibが既にそれらを推論するために必要な実数の理論を持っているからです。
2番目の決定はより重大です：浮動小数点ではなく正確な実数（ℝ）に翻訳します。
リテラル0.1は、最も近いIEEE-754倍精度ではなく、正確な実数1/10になります。モデルに丸めはなく、等価証明を複雑にする浮動小数点の非結合性もありません。
sqrt、exp、logは、真のReal.sqrt、Real.exp、Real.logになり、実数の定理が利用可能です。
率直に言えば、ℝ上で推論することはアルゴリズムの等価性を証明します。つまり、2つのプログラムが同じ数学関数を実装していることを証明します。これはほとんどの移行でまさに問題となることです（アルゴリズムを忠実に再実装したか？）。ビット単位の浮動小数点の同一性は証明せず、これら2つは真に異なる主張です：ℝ上の関数としての同一性を証明することと、ターゲットの抽象化の下で、実際に計算する方法で2つのプログラムが一致することを証明することは別物であり、はるかに困難です。
その下位のギャップは、たとえ1つの標準の下でも、浮動小数点では埋められません。IEEE 754はコア演算（加算、乗算、除算、平方根は正しく丸められ移植可能）を固定しますが、expやlogなどの超越関数は意図的に実装定義のままにしており、したがって2つの標準準拠の数学ライブラリは同じ入力に対して最後のビットが異なる結果を返す可能性があります（「テーブルメーカーのジレンマ」）。したがって、ビット単位の同一性はプラットフォーム間で明確に定義すらされていません。ℝ上でのモデル化はその層を意図的にスキップし、移行が通常必要とする質問をします：2つのプログラムは同じ実数値関数を表していますか？ビット自体が関心の対象である場合、例えばチェックサムや固定小数点台帳などでは、代わりにマシン浮動小数点数をターゲットにするでしょう。
- 実行例：iCPPI
iCPPIはポートフォリオ保険戦略です：リスク資産（株式）の上昇に参加しつつ、保護されたフロアを決して下回らないように口座を管理します。各期間、口座を時価評価し、ハイウォーターマークを更新し、ルールが許可するエクスポージャーを計算し、株式と債券の間でリバランスしますが、暗黙のドリフトが取引を正当化するほど大きい場合のみです。詳細は重要であり、期間を1つずらすミスは簡単に犯しやすく、見つけにくいです。私たちの転写は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として再計算します。これらはたまたま同じ値を表しますが、チェックする必要があります。これがポイントです：2つの誠実で慣用的な実装であり、人間は目を細めて信頼しなければなりません。それらは同じ関数ですか？§5でそれを定理にします。
（表記の摩擦を減らすため：同じ量が3つの設定で異なる名前を持ちます。PythonのV0/S/HはF#/Leanのv0/prices/hです。それぞれ初期値、価格系列、ハイウォーターマークを表します。）
- 決定論的翻訳、そしてそれがもたらすもの（もたらさないもの）
4.1 パイプライン
両方のフロントエンドは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とmatchを出力します。
4.2 生成されたLeanの外観
出力は不透明ではありません：インデントされた読みやすいLeanで、ソース定義ごとに1つの定義があります。以下は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 2つの正しさのバックストップ
エミッタを盲目的に信頼するよう求めているわけではありません。各生成仕様の背後には2つの独立したチェックがあります。
Mathlibに対して型チェックされます。仕様を構築すると、実際のMathlibに対してLeanのエラボレータを通過します。間違ったアリティ、型の不一致、不正な項など、翻訳ミスはコンパイルできません。これにより、多くのクラスの翻訳エラーが無料で排除されます（もちろん、型は正しいが意味的に間違った翻訳をキャッチするわけではありません）。
証明された健全性補題。ヘルパーについてはさらに進み、生成された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はありません。エミッタの比較と分岐のレンダリングが意図した関数を表すという、機械検証されたステートメントです。
- 証明による移行：定理とその証明方法
ここが成果です。
翻訳後、iCPPIの両バージョンは同じシグネチャを持つLean関数になります：
(v0 beta m emax delta rho : ℝ) (prices : List ℝ) : ℝ × ℝ
つまり、6つの実数パラメータと価格リストを入力として、（値、ハイウォーターマーク）のペアを出力します。（機械的な点：F#生成の定義は名前空間FSharpの下に存在するため、両方のicppiが名前の衝突なく1つのファイルに共存できます。）
移行正しさの主張は1つの定理です。これは、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
ステートメントを注意深く読んでください。変数は全称量化されています：等式は6つのパラメータとすべての価格リストのすべての組み合わせに対して成立し、任意の長さと任意の値、空リストを含みます。サンプリングも代表的なデータセットもありません。F#と新しいPythonが、アルゴリズムが見る可能性のあるすべての入力に対して同一の（値、ハイウォーターマーク）ペアを計算することを述べています。
証明の生成方法
この証明を手動で書いたわけではありません。それは私たちの自動証明システムによって生成されました。戦略は、まず元のプログラムの構造的帰納法で証明を導き、次にいくつかの算術推論で完成させることです。証明全体は約22,000文字で、完全に機械検証されています。