並行動的量子論理による並行量子通信プロトコルの
完全な自動形式検証に世界で初めて成功

【ポイント】

• 従来の動的量子論理に並行性を追加することで、並行量子計算の正しさの数学的証明（形式検証）を可能にする新たな論理体系を考案しました。
• その論理体系に基づいて自動的に正しさの証明を出力するツールを開発しました。
• そのツールを用いて高速に形式検証を行えることをいくつかの具体的な並行量子通信プロトコルに対して実証しました。

【研究背景と内容】

　プロトコルやプログラムなどにバグが一切ないことを数学的に証明すること（形式検証）は、それらに依拠する現代の高度IT社会における社会基盤の安全性の保障にとって本質的に必要な技術です。特に、量子コンピュータが実行する計算（量子計算）は従来の計算機が実行する計算（古典計算）とは根本的に異なる原理を用いているため、その正しさを図や勘などで直観的に（数学的証明抜きで）示すことは困難です。
　従来の研究では量子計算自体の形式検証は行われていましたが、量子計算を制御する通信の同期スケジューリングに関する並行性まで含めた形式検証は、その背景となる論理体系が存在しなかったために困難とされていました。本研究では、アムステルダム大学の数理論理学者らによって既に提案されていた動的量子論理^[*1]に対して、今回新たに並行性^[*2]を扱えるプロセス代数を組み合わせることで、並行量子通信プロトコルの形式検証を可能にする並行動的量子論理を提案しました。
　また、提案した並行動的量子論理に基づいて自動的に正しさの証明を出力するツールを開発し、いくつかの具体的な並行量子通信プロトコルに対して高速に動作することを実証しました。この手法では、人間の補助（補題の発見と入力）を一切必要としない完全な自動定理証明により形式検証が行われます。これにより、従来の手法と比較して形式検証の労力を大幅に削減することが可能になりました。
　本研究成果により、プロトコルやプログラムなどにバグが一切ないことを数学的に証明するという最大級の安全性を保障した高信頼量子計算の実現が可能になり、将来の安全・安心な量子ソフトウェア開発の基盤が整備されました。

　本成果は、2024年12月12日にソフトウェア工学分野のトップジャーナル「ACM Transactions on Software Engineering and Methodology」誌（ACM発行）のオンライン版に掲載されました。なお、本研究は、JAIST Research Grant for Fundamental Research、国立研究開発法人科学技術振興機構（JST）SICORP（JPMJSC20C2）、日本学術振興会（JSPS）科学研究費助成事業JP23K28060、JP23K19959、JP24K20757、JP24KK0185、JP24K23858の支援のもと行われたものです。

【論文情報】

【用語説明】

令和6年12月19日