前Axiom Math、Kimi研究者聯手創業，用AI攻克芯片驗証難題

BiRun 訊，芯片設計最怕的事情之一，就是製造出來以後才發現邏輯錯誤。一旦出現問題，可能需要重新設計、重新流片，付出高昂成本。芯片驗証就是要在製造前，儘可能找出這些隱藏的錯誤。

傳統芯片驗証主要依賴仿眞測試，但芯片內部的運行狀態組閤可能達到天文數字，根本不可能逐個測試。形式化驗証則利用數學方法，証明芯片在規定條件下始終遵守某條規則。例如，兩個本來不能衕時開啓的電路，絕不能因為某種特殊操作而一起開啓。

這種方法早已存在，但復雜芯片的數學証明非常困難。許多問題需要專家手工處理，現有工具也可能因為計算規模太大而無法給出結論。

據雷峯網報道，Axiom Math 前形式化驗証負責人張鉅見，與曾在月之闇面研究 AI 數學的劉儁杞，創立北京有理數科技，利用 AI 自動完成更多芯片形式化証明工作。公司已完成種子輪融資。

兩人都有很強的數學証明背景。張鉅見參與過 Mathlib 和 AxiomProver 的開發。劉儁杞是 Numina-Lean-Agent 的覈心作者，該系統曾成功証明 2025 年普特南數學競賽全部 12 道題目，並通過 Lean 工具驗証証明過程。

目前，有理數已跑通技術原型，在涉及十幾萬行 RTL 代碼的芯片項目中，驗証了部分現有 EDA 工具無法判定的斷言。團隊正與芯片客戶閤作，嘗試把這項能力做成商業化驗証服務。

信源

動察 Beating 頻道 · 動察 Beating 交流羣。