Verified Pauli-Product Measurement Compilation for Fault-Tolerant Quantum Computation

量子コンピュータは、複雑な暗号の解読から新材料のシミュレーションに至るまで、現在の最も強力なスーパーコンピュータでも不可能な問題を解決することを約束しています。しかし、これらのマシンは非常に壊れやすいものです。熱や振動によるわずかな乱れでさえ、計算を崩壊させてしまう可能性があります。生き残るために、科学者たちは、情報を保護するための特別な誤り訂正符号を用いた、フォールトトレラント（耐故障性）量子コンピュータを構築しています。データを単一の繊細な粒子に保存するのではなく、これらのシステムは情報を多くの粒子に分散させ、常に間違いをチェックして修正します。課題は翻訳にあります。つまり、ハイレベルなアルゴリズムを、これらの誤り訂正されたマシンが実際に実行できる特定の低レベルの操作へと、どのように変換するかという点です。

これらの将来的なマシンの多くで用いられる標準的な手法には、「ラティス・サージェリー（格子手術）」と呼ばれる技術が含まれています。コンピュータのメモリを表す大きな布のシートを想像してください。計算を行うには、単にスイッチを切り替えるのではなく、この布の断片を精密なパターンで縫い合わせたり、引き離したりします。これらの「縫い目」は物理的な糸ではなく、粒子のグループ間の結合測定です。コンピュータは、これらのグループが互いにどのように関連しているかを測定し、その結果を単純なビットデータとして記録し、そのデータに基づいて次に何をすべきかを決定します。パウリ積測定（Pauli-product measurement）として知られるこのプロセスは、これらの将来のマシンの基本言語です。問題は、人間が設計したアルゴリズムをこの言語へと翻訳するために使用されるソフトウェアツールが、未検証であったことです。もしコンパイラが翻訳中にミスを犯せば、計算全体が失敗する可能性があり、そのプロセスがあまりに複雑であるため、どこでエラーが発生したのかを知ることは困難です。

カリフォルニア大学ロサンゼルス校の研究チームは、翻訳が正しいことを数学的に証明するシステムを開発することで、この空白を埋めました。彼らは、これらの測定ベースのプログラム専用の新しい言語を開発し、標準的な量子回路をこの言語へと翻訳するコンパイラを構築しました。決定的なのは、彼らが単にコードを書いたのではなく、Leanと呼ばれる形式検証ツールを使用して、コンパイラが元のアルゴリズムの挙動を保持することを保証する厳格な数学的証明を構築したことです。これは、コンパイラが行うすべてのステップにおいて、出力が入力として意図されたものと正確に一致することを保証する証明書が存在することを意味し、結果の特定の確率に至るまで正確です。

研究者たちは、主に「ローアリング（低レベル化）」と「最適化」という2つのタスクに焦点を当てました。ローアリングとは、回転や論理ゲートのような標準的な量子ゲートを取り上げ、それをラティス・サージェリー・ハードウェアで必要とされる一連の測定と補正へと分解するプロセスです。最適化とは、プロセスをより速く、より効率的にするために測定を再配置することです。彼らの研究において、彼らは、コンパイラが回路を取り込み、それを測定命令へと翻訳し、最終的な結果を変えることなくそれらの命令を融合および再配置するルールを適用できることを証明しました。また、彼らはコンパイラが「マジック状態（magic states）」――特定の種類の計算を実行するために必要な特別なリソース――を正しく扱っていること、そして、プライベートな測定結果を外部から隠しつつ、パブリックな結果はアクセス可能であることを維持していることを検証しました。

彼らがこのシステムを35個の小規模な量子回路のスイートでテストした際、結果は具体的かつ測定可能なものでした。検証済みのコンパイラは、すべての有効な入力を正常に翻訳し、その翻訳が正しいことを確認する証明書を生成しました。パフォーマンスの面では、彼らが検証した最適化技術により、これらの回路を実行するために必要な論理測定ラウンドの数が、中央値で17.9パーセント減少しました。特定の回路では、この減少率はさらに高く、29パーセント近くに達しました。この削減は重要です。なぜなら、これらのフォールトトレラント・システムにおいて、すべての測定ラウンドは時間を消費し、リソースを消費するため、ラウンド数を減らすことは直接的にコンピュータの高速化と効率化につながるからです。

チームはまた、完全な数学的回転を正確に構築できない場合に必要となる、近似計算を扱う方法も示しました。彼らは、これらの近似によって導入される誤差を制限する方法を作成し、最終的な結果がユーザー定義の制限内に留まることを保証しました。彼らは、候補リストの中から最適なバージョンの回路を選択し、エラー制限を満たしながら最小のリソースを使用するシステムを示しました。この選択プロセスも検証されており、つまり、コンピュータが誤って不正確すぎる、あるいは遅すぎる回路を選択してしまうことがないようにしています。

この研究は、「コンパイラが機能することを期待する」ことから「コンパイラが機能することを知る」ことへの転換を意味しています。コンパイリング・パイプライン全体に対して機械検証済みの証明を構築することで、研究者たちは大規模な量子コンピューティングへの道のりにおける大きな不確実性の源を取り除きました。彼らは、複雑なアルゴリズムを取り、それを誤り訂正ハードウェアの特定の言語へと翻訳し、さらに速度のために最適化しながら、論理が損なわれないという数学的な保証を維持することが可能であることを示しました。システムは最大433個の量子ビットを持つ回路を正常に処理し、このレベルの検証が相当な規模の問題にもスケールできることを証明しました。これらの回路を実行するための物理的なハードウェアはまだ開発段階にありますが、このソフトウェアの基盤は、マシンが登場したときに、送られる指示が信頼できるものであることを保証しています。