Imandra 推出 CodeLogician：用數學形式化推理防程式碼幻覺

現在的 AI 程式設計助手最讓人頭疼的地方，不是它寫不出程式碼，而是它寫的程式碼猛一看毫無破綻，跑起來卻在看不見的角落裡悄悄爆雷。

做自動化推理系統的初創公司 Imandra 想從根子上解決這個問題。3 月 26 日，Imandra 釋出了名為 CodeLogician 的 AI 程式設計助手。和 GitHub Copilot 這類單純依賴大語言模型的程式碼補全工具不同，CodeLogician 走了一條叫「神經符號 AI」的路子，把大模型和嚴謹的數學形式化驗證綁在了一起。

把它寫出來的程式碼，先扔進數學模型裡驗一遍

Imandra 以前做的事情就挺硬核。他們的核心推理引擎 ImandraX 專門用來給金融機構、政府甚至國家級證券交易所審計極其關鍵的基礎系統，容錯率基本為零。

這次的 CodeLogician 本質上就是把這套工業級審計能力搬到了日常寫程式碼的流程裡。它基於 LangGraph 框架搭建，工作方式分為兩步：大模型生成程式碼後，系統會把程式碼自動轉換成數學模型，交由底層的 ImandraX 引擎去分析和證明。

它還會針對生成的程式碼自動構造測試用例，直到能在數學邏輯上證明這段程式碼確實按預期工作，沒有留下安全漏洞。Imandra 聯合執行長 Grant Passmore 直言，現有的生成式 AI 程式設計工具有硬傷，程式碼表面看著沒問題，卻經常以微妙且致命的方式出錯。

技術細節上，CodeLogician 依靠一種叫做「狀態空間探索」的機制。通過符號區域分解，它能窮舉大模型在解決問題時的可能狀態與行為，摸清模型到底在怎麼想，再用智慧測試來驗證正確性。

首發版本目前只支援 Python，後續會加入對 Java 和 COBOL 的支援。這意味著它未來還能用來幫金融和傳統大機構重構古老的遺留系統。目前 CodeLogician 已經對早期測試者開放申請排隊，未來會推出 API 和 VS Code 外掛。

為什麼重要

我們認為，CodeLogician 代表了 AI 程式設計工具從「看著像能跑」走向「絕對不能崩」的一個重要轉折。

普通開發者用 Copilot 寫個小指令碼，報了錯自己改改無所謂，但在金融交易、醫療裝置、航空航天這類容錯率為零的場景下，沒人敢直接用大模型生成的程式碼。CodeLogician 如果真能做到自動數學證明，就能把這類嚴苛領域的工程師從極其繁重的逐行人工審查中解脫出來。

從技術路徑看，它非常聰明地避開了硬卷大模型引數的陷阱。單純靠擴大模型引數很難徹底消滅幻覺，而把大模型的生成靈活性與符號推理的嚴謹確定性結合起來，用外部數學引擎給大模型當「監工」，是目前看來最靠譜的一條路。正如其聯席 CEO Denis Ignatovich 提到的，比爾·蓋茨曾把軟體開發的形式化方法稱為「聖盃」，現在符號 AI 正在把它平民化。

不過挑戰也很現實。嚴格的數學形式化驗證往往計算開銷極大，面對複雜的真實世界業務邏輯時，狀態空間可能會急劇爆炸。它在小規模 Python 指令碼上跑得通，到了幾十萬行、依賴複雜的企業老系統裡還能不能保持足夠快的響應速度，依然需要打個問號。但無論如何，能讓 AI 程式碼接受數學檢驗，行業就已經往前邁了一大步。