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

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

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

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

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

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

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