メリーランド大学とZapata Quantum, Inc. (OTC: ZPTA)は、量子ソフトウェア開発における形式的検証を実装するための研究協力を開始した。このパートナーシップは、手動による誤りが生じやすいコーディングを超えて、量子アルゴリズムがスケールする際に正しく動作することを保証するために数学的証明を使用することを目指している。この取り組みは、ミッションクリティカルな古典コンピューティングでは標準的な実践である「検証ファースト」モデルを確立することを目指しているが、量子アプリケーション開発においてはこれまで黎明期の分野であった。
量子ハードウェアが耐障害性時代に移行するにつれ、複雑な数式を物理的な量子回路に変換することが重大な障害点となっている。形式的検証は、高レベルアルゴリズムが実行される量子回路と一致することを数学的に証明し、量子ビットやゲート深度などのハードウェアリソースに対する検証済みベンチマークを提供し、古典シミュレーションでは検証できないほど複雑なアルゴリズムの開発を可能にすることで、この問題に対処する。この協力による最初の主要な成果は、ショアの因数分解アルゴリズムの形式的に検証された実装となり、チームはこれを量子化学、材料科学、最適化、金融などの他の高価値領域のための基礎テンプレートとして機能させることを意図している。
このプロジェクトは、Zapata Quantumの共同創設者であるYudong Caoと、メリーランド大学の助教授であり量子情報・コンピュータサイエンス共同センターのフェローであるRunzhou Taoが主導している。唯一の上場企業であるハードウェア非依存の量子ソフトウェア企業として、Zapata Quantumは検証済みのショアの実装とリソース推定を公開し、より広範な研究・エンジニアリングコミュニティによる独立した検証と再利用を可能にする計画である。このアプローチは、業界における「集合行為問題」を橋渡しすることを意図しており、アプリケーションの実証への体系的な投資不足がこれまで商業的実現可能性への道を妨げてきた。
Zapata Quantumからの公式発表は同社のウェブサイトで確認できる。
2026年1月12日
