元Axiom Math、Kimiの研究者が協力して起業、AIでチップ検証の難題を克服

動察 Beating AI 速報、チップ設計で最も恐れることの一つは、製造後に論理エラーを発見してしまうことだ。問題が発生すると、再設計や再テープアウトが必要になり、多大なコストを払うことになる。チップ検証とは、製造前にこうした隠れたエラーを可能な限り見つけ出すことである。

従来のチップ検証は主にシミュレーションテストに依存しているが、チップ内部の動作状態の組み合わせは天文学的な数に達する可能性があり、一つ一つテストすることは到底不可能である。形式検証は数学的手法を利用して、チップが規定条件下で常にある規則に従うことを証明する。例えば、本来同時にオンになってはならない二つの回路が、ある特殊な操作によって一緒にオンになってはならないということである。

この手法はすでに存在するが、複雑なチップの数学的証明は非常に困難である。多くの問題は専門家が手作業で処理する必要があり、既存のツールも計算規模が大きすぎるために結論を出せないことがある。

雷峰網の報道によると、Axiom Math の元形式検証責任者である張巨見氏と、月之暗面で AI 数学を研究していた劉俊杞氏が、北京有理数科技を設立し、AI を利用してより多くのチップ形式証明作業を自動で完了させる取り組みを行っている。同社はシードラウンドの資金調達を完了した。

両者とも数学的証明において強いバックグラウンドを持つ。張巨見氏は Mathlib と AxiomProver の開発に参加した。劉俊杞氏は Numina-Lean-Agent の核心的な著者であり、同システムは2025年プットナム数学競技会の全12問を証明することに成功し、Lean ツールを通じて証明プロセスを検証した。

現在、有理数は技術プロトタイプを完成させており、十数万行の RTL コードを含むチッププロジェクトにおいて、既存の EDA ツールでは判定できない一部のアサーションを検証した。チームはチップ顧客と協力し、この能力を商業化された検証サービスにすることを試みている。