Jane Street 正式方法與自主編碼

Jane Street 已經改變了長期以來對正式方法的懷疑態度，宣布成立一支專門的團隊，將這些技術整合到其軟體開發生命週期中。此變化是由自主編碼的興起所驅動，該技術透過降低撰寫證明的門檻，並提升對 AI 生成程式碼進行嚴格驗證的必要性，從而改變了正式驗證的成本效益分析。

自主編碼作為正式方法的催化劑

自主編碼從根本上改變了正式方法的經濟與技術可行性，主要表現在兩個方面：降低證明構建的成本，以及提升對嚴格驗證的需求。

降低證明成本

歷史上，正式方法的成本高得令人卻步。例如，seL4 微核心需要 25 人年的人力來驗證 8,700 行 C 程式碼，每行程式碼大約需要 23 行證明以及半個人日的工作量。現在 AI 代理人充當了力量倍增器，自動化將證明概念編碼到特定證明系統的繁瑣工作，使得人類程式設計師能專注於高層策略，而非技術語法。

解決驗證瓶頸

隨著 AI 代理人在撰寫功能性程式碼方面變得更為熟練，出現了「驗證瓶頸」。雖然模型能有效達成即時目標，但它們常會產生「冗餘」——程式碼過於複雜、包含微妙的邊緣案例錯誤，且違反關鍵的程式碼庫不變式。正式方法提供了一種可擴展的方式來減輕此負擔，將人類的角色從編寫程式碼轉變為驗證生成的程式碼是否符合嚴格的數學規格。

強化代理回饋迴路

AI 代理人依賴精確的回饋而茁壯。雖然基於屬性的測試與模糊測試很有價值，但它們無法覆蓋程式的全部狀態空間。正式方法提供了普遍的保證（$\forall$ 量詞），讓開發者能徹底消除整類錯誤——例如資料競爭或跨站腳本漏洞。這種高保真回饋使得代理人能更可靠地解決更困難的問題。

Jane Street 的實施策略

Jane Street 正在利用其內部基礎設施與文化來實施這些技術，著重於語言設計與驗證之間的協同效應。

語言控制與 OxCaml

由於 Jane Street 對其使用的語言（OxCaml）擁有深度控制權，他們可以直接修改語言本身，以更好地支援以證明為導向的技術。可能的方向包括：

• 將屬性的模組化規格直接整合到型別系統中。
• 為所有權與可變性加入型別層級的限制。
• 將證明技術直接嵌入語言語法。

型別系統採用的文化

與許多組織需要說服開發者採用新 PL（程式語言）特性不同，Jane Street 的使用者群已對複雜的型別系統功能抱持熱忱。這為實驗即時改進與長期驗證軟體願景提供了肥沃的環境。

與外部工具的整合

在建構內部能力的同時，Jane Street 計畫將 OxCaml 與現有的正式驗證基礎設施整合，包含如 Lean、Dafny、Rocq（前稱 Coq）、Agda 與 Iris 等工具。

社群觀點與反論點

從業者之間的討論凸顯了此方法的潛力與限制。

大型語言模型在證明助理中的角色

一些開發者報告稱，使用前沿模型（如 GPT-4 或 Claude）在 Rocq 與 Lean 4 中完成手動證明取得了顯著成功。某位使用者指出，AI 常能透過迭代在數分鐘內證明一個引理，而人類則需要更長時間，這暗示維護證明的成本差距正在縮小。

「地圖與領域」問題

批評者認為正式方法受到一個根本限制：數學模型（地圖）與實際領域（領土）之間的差距。

「理論上，理論與實踐沒有差別。實踐中……」

對於確定性演算法而言，映射通常是 1:1，但對於使用者介面或探索性工作，映射則較不明確，使得正式方法在這些領域的適用性降低。

「變通」的風險

有人擔心過度的數學嚴謹會導致「防禦式程式設計」，開發者會想出技巧繞過借用檢查器或證明系統以維持開發速度，若未妥善管理，可能會引入新的風險。

規格的驗證

另一個爭議點是，若驗證程式碼由 AI 生成，是否會變得「粗糙」。此方法的成效取決於是否有非粗糙的智慧（人類或 AI）能確認規格與目標系統精確匹配，因為規格本身仍是潛在的失敗點。