理論計算機科学の静かで抽象的な世界において、研究者たちはしばしば「等価性」という問題に取り組んでいる。それは、見た目が異なる二つの構造が、実際には同じ根底にある実体を表現しているかどうかを判断することである。機械を組み立てるための指示書を想像してみてほしい。その指示を、長くうねった段落として書くこともできれば、図解を用いた箇条書きのリストに分解することもできる。もし両方の指示書が、全く同じように機能する全く同じ機械を作り出すのであれば、たとえ見た目が全く異なっていても、それらは等価である。この概念は、プロセスを図（ボックスとそれをつなぐ線）として描く「図式的推論（diagrammatic reasoning）」と呼ばれる分野の中心的なものである。これらの図は、電気の流れから量子コンピュータの挙動に至るまで、複雑なシステムをモデル化するために使用される。量子コンピューティングの領域では、機械が日常的な直感に反する方法で情報を操作するため、二つの異なる回路図が同じ動作を行うことを検証することは、極めて重要な安全確認となる。もしコンピュータが、二つの設計が同一であることを証明できないのであれば、将来のテクノロジーを支えるハードウェアを最適化したり検証したりすることを信頼することはできない。

フランスとドイツの研究チームは、現代の自動推論ツールがこの特定の種類の等価性をどの程度扱えるかをテストするために設計された、新しい一連の課題を導入した。彼らの研究は、「図式的等価性」と呼ぶ一連の問題に焦力しており、それは単純な問いを投げかける。すなわち、与えられた二つの異なる回路図に対し、固定された一連のルールを用いて、それらを互いに変形させることができるか、という問いである。研究者たちは単に問いを投げかけただけでなく、この問題のユニークで困難な例を数千個生成するための「工場」を構築した。彼らは、ワイヤーの入れ替えのみを含む簡略化されたバージョンから、様々な種類の電子部品を含む複雑なバージョンまで、三つの異なる難易度レベルを作成した。各レベルにおいて、彼らは視覚的な図をコンピュータが読み取れる言語へと翻訳し、世界最先端の自動定理証明器や論理ソルバーのための厳格なテスト場を作り上げた。

研究者たちはまず、ゲームのルールを定義することから始めた。彼らのシステムにおいて、回路は「生成子（generators）」と呼ばれる基本的な構成要素から構築され、それらはワイヤーによって接続される。これらの接続は、二つの方法で行われる。一つは、鎖のように次々と続く形式であり、もう一つは、並行するトラックのように並列で行われる形式である。問題の核心は、同じ回路であっても、多くの異なる方法で描かれ得るという点にある。文章が意味を変えずに組み替えられるのと同様に、回路図は「コヒーレンス方程式（coherence equations）」として知られる特定の数学的法則に従って、ねじられたり、引き伸ばされたり、あるいは再構成されたりすることができる。コンピュータにとっての課題は、全く異なって見える二つの図を見て、それらが果たしてルールに基づいた同一のオブジェクトであるかどうかを判断することである。これをテスト可能にするため、チームは三つのバリエーションの問題を作成した。第一の、最も一般的なものは、あらゆる種類のコンポーネントを許容する。第二のものは、すべてのコンポーネントを取り除き、ワイヤーの入れ替えのみを残すことで、実質的に問題を置換（permutation）の問題へと変える。第三のものは、第二のものの簡略版であり、より扱いやすい、とはいえ依然として困難なパズルを作るために、最も基本的な構成要素のみを使用している。

データを生成するために、チームは「回路設計者」として機能するコンピュータプログラムを作成した。これらのプログラムは空白のグリッドから始まり、コンポーネントとワイヤーをランダムに配置する。その後、ワイヤーをねじったり、隣接するブロックを入れ替えたりといった一連の変換を適用することで、最初の回路と数学的に同一でありながら、見た目が異なる第二の回路を作成する。プログラムは、構築の過程において二つの結果として得られる図が等価であることを保証している。つまり、答えは常に「イエス」であるが、それを証明するための経路は図の複雑さの中に隠されている。研究者たちは、入力ワイヤーの数や図のサイズを変化させることで、数千組のこれらのペアを生成し、難易度のスペクトラムを作り出した。その後、彼らはこれらの視覚的なパズルを、科学界で使用されている二つの標準的なフォーマットにエンコードし、あらゆる自動推論ツールが解決を試みることができるようにした。

研究者たちがこれらのベンチマークをテストする際、彼らはそれらを現代で利用可能な主要な自動推論ツールと対決させた。彼らは二つの特定のシステムを選択した。一つは算術的および論理的な制約の処理に長けているものであり、もう一つは一般的な論理的演繹における強力なシステムである。結果は、性能の明確な隔たりを明らかにした。算術的制約を扱うように設計されたシステムは、単純および中程度の難易度のパズルの大部分を解決し、著しく高い能力を発揮した。このシステムは、多くの場合、最大20本のワイヤーと数百のコンポーネントを持つ回路の等価性を検証することができた。しかし、一般的な演繹システムは、極めて苦戦した。それは複雑な問題のほとんどを解くことができず、比較的小さな回路に対しても行き詰まってしまった。研究者たちは、問題の難易度は、ワイヤーの数と図における総接続数の二つの主要な要因によって駆動されていることを見出した。これらの数値が増加するにつれて、ツールが解を見つける能力は急激に低下した。

この研究は、自動推論の分野における重大なボトルネックを浮き彫りにしている。コンピュータはますます強力になりつつあるが、算術的推論と複雑な構造的ルールの操作という特定の組み合わせは、依然として手強い課題である。研究者たちは、最も優れたパフォーマンスを示したツールは、ワイヤーを支配する数学的制約を純粋に論理的なステップのみを通じて演繹しようとするのではなく、それらをネイティブに理解できるツールであったことを観察した。このことは、図式的等価性を効率的に解決するためには、将来のツールが算術的推論をそのコアロジックにより深く統合する必要がある可能性を示唆している。この研究は、量子回路の検証問題を解決したと主張するものではないが、重要なストレス・テストを提供した。標準化された挑戦的な問題を提供することで、チームは科学界に対して、進歩を測定するための明確な方法を与えた。これらのベンチマークは、現在の自動化ツールの限界を映し出す鏡であり、複雑な図式ベースのシステムの検証を信頼できる現実のものにするために必要な、具体的な改善の方向性を示すものである。