數學與軟體工程中的語意對齊模型

TL;DR

• 問題:autoformalization——把自然語言數學(英文、法文…)翻譯成形式語言數學(Lean 或其他定理證明語言)。動機是人寫的證明常常不完整(缺步驟,而數學家自己可能沒察覺),更糟的是有時根本是錯的;翻成形式語言後就能用 Lean 定理證明器實際檢查定理是否真的被證明了。
• 目標設定很銳利:做一個比前沿模型至少小 1000 倍的模型,而且在 autoformalization 這單一任務上要贏過最大的前沿模型。
• 關鍵性質:semantic alignment——同一個物件用不同模態表示、語意內容相同時,要在模型的 embedding 空間中靠近;語意內容不同就要遠離。訓練配方叫 semantic contrastive learning;帶來的直接好處是檢索(retrieval)階段效率大幅提升。
• 不只數學:同樣的性質適用於程式語言間的翻譯、規格 → 電路、以及連結不同數學領域的定義以發現新關係——而且可以用小模型做到。
• 正在做的延伸:COBOL → Python 的遺留程式碼翻譯。因為輸入程式本身就是規格,不需要另外寫 spec;他們用 LLM 驅動的符號執行(symbolic execution) 從輸入程式生成測試集,再用它驗證輸出程式與輸入是否語意等價。

重點整理

什麼是 autoformalization,以及為什麼需要它(約 01:18–01:19)

他自我介紹:Georgia Tech 計算機科學教授,研究領域涵蓋形式化方法與數學、物理、程式的 neuro-symbolic AI。他明確說明自己的題目和前兩位講者不同。

Autoformalization = 把自然語言數學翻譯成形式語言數學。 自然語言數學指用英文、法文等語言寫的數學;形式語言指 Lean 或其他定理證明語言。

為什麼要翻?因為自然語言數學有兩個問題:

1. 人寫的證明常常不完整——缺了步驟,而且寫的數學家自己可能不知道。
2. 更糟的是,有時候證明根本是錯的。

翻成形式語言之後,就可以把 Lean 定理證明器開下去,實際檢查那個定理到底有沒有被證明。

什麼叫「等價」(約 01:19–01:20)

他們要造的是一個盒子:輸入自然語言數學,輸出等價的形式語言數學。這裡的等價指的是 semantic equivalence(語意等價):輸入的畢氏定理的語意內容,必須和輸出的 Lean 程式的語意內容相同——它必須在講直角三角形,而且那個關係必須一樣。

任務設定:做出這樣一個盒子,而且要比前沿模型至少小 1000 倍,甚至更小;問題是——要怎麼訓練這樣一個模型,讓它在 autoformalization 這一個任務上贏過外面最大的前沿模型?

Semantic alignment 與 semantic contrastive learning(約 01:20–01:22)

他提出的性質叫 semantic alignment。這個概念本身不新,很多場景都有人談過,但在數學裡它有特定意義:

兩個物件以不同模態表示,若它們的語意內容相同,就要在模型的 embedding 空間中彼此靠近;若語意內容不同,就要彼此遠離。

把這個性質灌進模型之後,模型在 autoformalization 上就有效得多——他特別點名在檢索(retrieval)的時候效率高出很多。

這個性質的價值不限於「自然語言數學 → 形式語言數學」,還包括: - 程式語言之間的程式碼翻譯 - 規格 → 電路 - 連結不同數學領域的定義,看出跨領域定義之間的關係,從而發現新數學

而且——這是他反覆強調的重點——用非常小的模型就能做到,不必有前沿模型的存取權。

訓練配方叫 semantic contrastive learning:把上述性質灌進模型(語意相同 → embedding 靠近)。結果是在他們測試的所有 benchmark 上都比前沿模型強得多。

延伸到程式碼翻譯(約 01:22–01:23)

他們正把這個想法帶到程式碼翻譯:建一個工具,把 COBOL 這類遺留語言的程式翻成 Python,並在輸入程式上部署驗證工具與自動化測試工具。

這裡有個很漂亮的設計論點:在這個情境下不需要規格,因為輸入程式本身就是規格。他們用 LLM 驅動的符號執行從輸入程式生成一組測試集,有了測試集之後就能拿去跑輸出程式,檢查輸入輸出兩個程式是否語意等價。他也直言這件事有很強的商業誘因。

結論(約 01:23–01:24)

他的總結:在任何你能取得形式化物件的場景中——做形式物件之間的翻譯、或把非形式物件翻成另一個模態的形式物件——把 semantic alignment 這個性質灌進模型,是打造一個能 scale 的系統的好方法;而且模型規模可以小很多,卻仍能擴展到非常大的程式碼庫。

金句

"Often human-written proofs are incomplete, meaning they are missing steps, and the human mathematicians may not be aware of that. Worse, sometimes the proofs are incorrect."(約 01:19)

autoformalization 的真正動機不是形式主義潔癖,而是人類證明本來就會出錯。

"If two objects which are represented in different modalities have the same semantic content, then we want them to be close by in the embedding space of the model."(約 01:21)

一句話定義 semantic alignment。

"In this setting, we don't need specifications because the input program is the specification."(約 01:23)

程式碼翻譯之所以比一般形式化容易的關鍵洞見。