Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair

あなたは、デジタル・レゴ・ブロックを使って巨大で複雑な城を築いているところだと想像してください。これが、エンジニアがコンピュータ・チップを設計するときに行っていることです。彼らは、トランジスタがどのように振る舞うべきかを指示するRTL（レジスタ転送レベル）と呼ばれるコードを記述します。しかし、ここには落とし穴があります。もし、たった一つのブロックでも置く場所を間違えると、電源を入れた瞬間に城全体が崩壊してしまうかもしれないのです。こうした間違いをチェックすることは、この仕事の中で最も困難な部分であり、しばしば作業時間の半分以上を占めます。伝統的に、エンジニアは自分の成果を確認するために、主に2つの方法を用いてきました。1つ目は「テスト走行」のようなもので、チップにいくつかの特定のシナリオを実行させて、壊れないかを確認します。2つ目は「形式検証」です。これは、単にテストしたシナリオだけでなく、「あらゆる可能な条件」において城が立ち続けることを保証する、超数学的な証明のようなものです。しかし、この超証明メソッドは通常、大企業にしか手が届かないような、高価でクローズドなソフトウェアを必要とします。

そこに、新しい登場人物が現れました。大規模言語モデル（LLM）です。彼らは、物語やコードを書くことができるAIチャットボットとして知られています。最近、人々はこう問いかけ始めました。「AIは、壊れたデジタル上の城を修理する建築家になれるだろうか？」という問いです。大きな疑問は、AIが間違いを見つけるだけでなく、高価なソフトウェアのライセンスを購入することなく、数学的に完璧であると証明された方法で、それを修正できるかどうかという点です。この論文は、まさにその問いに深く切り込み、AIの創造性と、厳格で揺るぎない論理的数学との間に架け橋を築こうとする試みであり、それには無料のオープンソース・ツールのみを使用しています。

AI探偵とオープンソースの道具箱

この研究において、研究者の Ha Trung Tran は、壊れたチップ設計の修理チームとして機能する、巧妙なAIエージェントのチームを構築しました。それは、ハイテクな探偵隊がループの中で働いているようなものです。一つのAIがすべてを一度に行おうとするのではなく、チームは役割分担されています。設計図を読むエージェント、チップが「どうあるべきか」というルールを書くエージェント、作業をチェックするエージェント、そして実際にコードを修正するエージェントです。

ここでの秘訣は、間違いをどのようにチェックするかという点にあります。ほとんどのAI修理ツールは、チップが動作するかどうかを確認するために、単にいくつかのテスト走行（シミュレーション）を行うだけです。しかし、このチームは「形式的なバックエンド」を使用しています。これは、Yosys、SymbiYosys、Z3 と呼ばれるツールで構成された、無料のオープンソースの数学エンジンです。このエンジンは単に推測するのではなく、チップが正しいことを数学的に証明しようと試みます。もしチップが失敗した場合、エンジンは単に「壊れている」と言うだけではありません。それは、どのようにして城が崩壊したのかを示すビデオ再生のような、具体的な「反例（カウンターエキザンプル）」をAIに提示します。AIはそのビデオを見て、何が間違っていたのかを理解し、修正を試みます。彼らは、数学がチップの完璧さを証明するか、あるいは試行回数が尽きるまで、「チェック、クラッシュの発見、修正、再チェック」というプロセスを繰り返します。

朗報：うまくいった（時もある）

研究者たちは、単純な計算機パーツ（ALU）から、より複雑なトラフィックコントローラーやメモリユニットに至るまで、6種類の異なるデジタル設計に対してこのシステムをテストしました。結果は、勝利と明確な限界が混在したものでした。

主役は、チップの計算機脳のような役割を果たす ALU（算術論理演算装置）でした。研究者たちは、意図的に「AND」演算を「OR」演算に置き換えることで、設計を壊しました。AIチームは即座にエラーを検知しました。チェックと修正のわずか2ラウンドで、彼らはコードを修理しました。さらに重要なことに、オープンソースの数学エンジンは、チップが処理し得るあらゆる数値に対して、その修正が正しいことを100%の確信を持って証明しました。これは5回のテスト走行すべてで発生し、平均わずか16.5秒でした。これは、アイデアが機能することを証明しました。つまり、AIがオープンソースの数学ツールに導かれることで、数学的な保証を伴って本物のバグを見つけ、修正できるということです。

難題：AIが行き詰まった場所

しかし、物語は完全な勝利ではありません。研究者が同じプロセスを他の5つの設計に試みたとき、AIチームは壁にぶつかりました。彼らはそれらを信頼性を持って修正することができなかったのです。論文では、AIにとっての罠となる4つの明確な「失敗モード」を特定し、なぜ失敗したのかを注意深く分析しています。

1. 「深すぎる」罠（有界被覆空虚性 / Bounded-Cover Vacuity）: あるケース（カウンタ）では、修正自体は正しかったにもかかわらず、数学エンジンは「FAIL」と判定しました。なぜでしょうか？ その設計が特定の状態に到達するために256サイクル実行する必要がありましたが、ツールは256サイクル分までしか見ていなかったからです。それは、車が国を横断できることを証明しようとして、わずか1マイルしか走っていないようなものです。ツールは目的地を見ることができず、諦めてしまいました。論文では、これはツールの限界であり、AIの限界ではないと述べています。
2. 「混乱した指示」の罠（仕様の曖昧さ / Specification Ambiguity）: 別の設計（アービター）では、AIは書かれたルールに従おうとしましたが、そのルールは（時計なしで変化する信号機のように）不可能なことを要求していました。AIは忠実に不可能な指示に従い、行き止まりに突き当たりました。
3. 「タイムトラベル」の罠（時間論理バグ / Temporal Logic Bugs）: 2つのケース（UART送信機とFIFOメモリ）では、複数のタイムステップにわたって発生するイベントがバグに関係していました。AIは単一ステップの論理（計算機のような）を修正することには長けていましたが、時間の経過とともに起こるイベントのシーケンスについて推論することには苦戦しました。
4. 「ルールが多すぎる」罠（マルチプロパティ圧力 / Multi-Property Pressure）: 最後のケース（AXI Liteスレーブ）では、チップが同時に満たさなければならないルールがあまりに多く、一つのルールを修正すると別のルールが壊れてしまうという状況でした。AIは、全員を満足させる解決策を見つけることができず、ループに陥りました。

道具箱に隠されたグリッチ

また、オープンソースのツール自体に関する驚くべき発見もありました。研究者たちは、コードを処理するのに役立つ Yosys というツールには、隠れた癖があることを発見しました。「bind」と呼ばれる特定の方法を使用して設計に安全チェック（アサーション）を付加しようとすると、ツールはそれを黙って無視してしまうのです。それは、部屋にセキュリティカメラを設置したものの、カメラのプラグが抜けているようなものです。カメラが一度も映像を捉えないため、システムはすべてが正常であると判断してしまいます。研究者たちは、数学エンジンが実際にチェックを認識できるように、チェックをコードに直接「注入（インジェクト）」する方法に変更する必要がありました。これは、これらの無料ツールを使用する任何人にとって非常に役立つヒントです。

結論

この論文は「実現可能性調査（フィジビリティ・スタディ）」であり、これは「私たちは試してみた。その結果、どこで機能し、どこで壊れるのかを正確に特定した」という、少し凝った言い回しです。主な発見は、オープンソースのツールを使用し、かつ問題が複雑すぎない場合に限り、AIを使用して数学的な正当性の証明を伴うチップ設計の修正を行うことは可能であるということです。

著者は限界についても正直に述べています。このシステムは、単純で即時的な論理エラー（計算機のような）を修正することには優れていますが、複雑なタイミングの問題、深いメモリ状態、あるいは矛盾するルールを持つ設計には、現時点では苦戦します。彼らはチップ修理の問題を解決したと主張しているのではなく、AIが機能する「安全圏」と、迷ってしまう「危険地帯」を示す明確な地図を描いたのです。無料のツールのみを使用することで、彼らはこのような研究への参入障壁を下げ、信頼性の高いハードウェア設計の未来を築き始めるために、百万ドルもの予算は必要ないということを証明しようとしています。