前Axiom Math、Kimi研究者联手创业，用AI攻克芯片验证难题

动察 Beating AI 快讯，芯片设计最怕的事情之一，就是制造出来以后才发现逻辑错误。一旦出现问题，可能需要重新设计、重新流片，付出高昂成本。芯片验证就是要在制造前，尽可能找出这些隐藏的错误。

传统芯片验证主要依赖仿真测试，但芯片内部的运行状态组合可能达到天文数字，根本不可能逐个测试。形式化验证则利用数学方法，证明芯片在规定条件下始终遵守某条规则。例如，两个本来不能同时开启的电路，绝不能因为某种特殊操作而一起开启。

这种方法早已存在，但复杂芯片的数学证明非常困难。许多问题需要专家手工处理，现有工具也可能因为计算规模太大而无法给出结论。

据雷峰网报道，Axiom Math 前形式化验证负责人张巨见，与曾在月之暗面研究 AI 数学的刘俊杞，创立北京有理数科技，利用 AI 自动完成更多芯片形式化证明工作。公司已完成种子轮融资。

两人都有很强的数学证明背景。张巨见参与过 Mathlib 和 AxiomProver 的开发。刘俊杞是 Numina-Lean-Agent 的核心作者，该系统曾成功证明 2025 年普特南数学竞赛全部 12 道题目，并通过 Lean 工具验证证明过程。

目前，有理数已跑通技术原型，在涉及十几万行 RTL 代码的芯片项目中，验证了部分现有 EDA 工具无法判定的断言。团队正与芯片客户合作，尝试把这项能力做成商业化验证服务。