数学AIのユニコーンHarmonicがEDA市場に進出、AI「Aristotle」がVerilogに対応

2026年10月27日、数学AIのユニコーン米Harmonicは、同社の数学的推論AI「Aristotle（アリストテレス）」がソフトウェアおよびハードウェアの形式検証に対応したことを発表した。

プレスリリース

Harmonicは2023年に設立された米国のAIスタートアップで、数学的な推論能力に特化したAIの開発を手掛けている。本社は米カリフォルニア州パロアルトに置き、従業員数は数十人規模ながら、2025年11月時点の企業評価額は14億5,000万ドルに達している。

共同創業者の一人は、米国の大手オンライン証券Robinhoodの共同創業者兼CEOであるVlad Tenev氏。同氏はスタンフォード大学で数学を学んだ経歴を持ち、Harmonicでは共同創業者兼エグゼクティブ・チェアマンを務めている。

もう一人の共同創業者でCEOを務めるTudor Achim氏は、自動運転向けAIソフトウェアを開発するHelm.aiの共同創業者で、同社のCTOを務めた人物。

Harmonicが掲げる開発目標は「Mathematical Superintelligence（MSI）」と呼ばれる、人間を超える数学的能力を備えたAIの実現だ。

同社が開発する数学AI「Aristotle（アリストテレス）」は、一般的なLLMのように確率的に回答を生成するだけでなく、数学的な証明を構築し、その正しさをコンピューターで検証できる点を特徴としている。2025年には国際数学オリンピックの問題6問中5問について形式的に検証可能な解答を生成し、金メダル相当の成績を収めたと発表している。

同社はSequoia Capitalをはじめとする有力ベンチャーキャピタルから多額の資金を調達しており、累計調達額は2億9,500万ドルに達し、2025年11月時点の企業評価額は14億5,000万ドルとされている。

AIによるフォーマル検証をC言語とVerilogに対応

今回Harmonicが発表したのは、数学の定理証明で培った「Aristotle」の推論・証明技術を、実際のソフトウェアや半導体の設計検証に応用するものだ。

具体的には、「Aristotle」が新たにC言語とVerilogに対応。AIによる検証プロパティの生成と数学的な証明を組み合わせることで、従来は専門知識を持つエンジニアが担っていたフォーマル検証の作業を効率化する。

ユースケースとしては、「Aristotle」が対象コードを読み込み、検証すべきプロパティを自動提案するとともに、それぞれについて証明が成立するかを確認。証明に成功した項目、反証された項目、結論が得られなかった項目を区別し、証明の前提条件も提示する。設計者は「Aristotle」が提案したプロパティを確認した上で、開発リポジトリに登録し、CI（継続的インテグレーション）環境でコードが更新されるたびに検証を実行できる。

対応する検証内容は、C言語では機能的な正しさや特定種類の未定義動作の排除、Verilogでは制御回路の安全性（Safety）や活性（Liveness）、データパスの数学的な性質などとなっている。

半導体企業Tensordyneで最大11万サイクル先のバグを検出

Harmonicは、「Aristotle」の半導体設計への適用事例として、AI推論システムを開発するTensordyneでの成果を公表している。

同社では、1,220万ゲート相当、124万フリップフロップ、45MbitのSRAMを含む設計ブロックを検証対象とした。312ページに及ぶ仕様書やRTLなどを「Aristotle」に入力したところ、合計241件のプロパティを検証し、185件を証明、56件について反例を提示したという。

241件のプロパティのうち100件は「Aristotle」が仕様書から生成したもので、残り141件は既存のRTLに記述されていたアサーションだった。

検証の結果、リセットから2万5,000～11万クロックサイクル後に現れる問題を検出。サブ・ブロックを対象とした検証結果も含め、次世代チップの開発初期段階で計8件の不具合を発見したとしている。

さらにTensordyneでは、仕様書から「Aristotle」にRTLを生成させ、論理合成結果をフィードバックしながら設計を最適化する試みも実施。ある共通ブロックの初期検討において、機能的な性質を再検証しながら、消費電力を約26％、セル面積を約19％削減したという。

これらの結果は、「Aristotle」が単なる検証支援にとどまらず、RTL生成から検証、PPA最適化までを支援する可能性を示している。

C言語のソフトウェア検証でも成果

ソフトウェア分野では、TclやDropbear SSHなどで利用される多倍長整数演算ライブラリ「LibTomMath」への適用成果を公表した。

「Aristotle」は同ライブラリの一部の関数から3件の不具合を発見・修正するとともに、2つの演算処理を最適化。修正・最適化後のコードが指定された仕様を満たすことを証明し、モジュラー指数演算のベンチマークでは従来比31～38％の性能向上を実現したとしている。

なお、形式的な証明の対象は一部の演算ルーチンとその関連関数であり、ライブラリ全体の正しさが証明されたわけではない。

EDA市場における新たなAI活用の方向性

「Aristotle」は既に提供が開始されており、利用量に応じた従量課金制を採用。企業向けにはオンプレミスやプライベートクラウドでの運用にも対応する。

Harmonicは、EDA市場に存在する古典的なEDAベンダと異なり、数学的な定理証明を得意とするAIを出発点として、半導体設計のフォーマル検証領域に進出してきた点が興味深い。

昨今、Harmonicのように異分野のAIをEDA分野に応用させる動きや、ChipAgentsのようにAIを中心にEDAフローの再構築を目指す動きが、北米AIベンチャーを中心に活発化しつつある。

AIベンチャーが半導体設計に目を向けているのは、半導体設計は革新する余地がまだ大きいと考えているからであり、その効果を見せやすく、ビジネス的に大きなリターンが見込めるためであろう。

Harmonicの実力は今後の評価を待つ必要があるが、数学AIから生まれた新たな技術がEDA市場にどのような影響を及ぼすか、注目していきたい。

Harmonic