北陸先端科学技術大学院大学(JAIST)は12月19日、「並行動的量子論理」を提案し、それに基づく「並行量子通信プロトコル」の完全な自動形式検証、つまりヒトによる補助(補題の発見と入力)を一切必要とせず、従来手法と比較して労力を大幅に削減することが可能な、完全な自動定理証明による形式検証に初めて成功したことを発表した。

同成果は、JAIST コンピューティング科学研究領域の緒方和博教授、同・髙木翼准教授らの研究チームによるもの。詳細は、ソフトウェア工学と方法論に関する全般を扱う学術誌「ACM Transactions on Software Engineering and Methodology」に掲載された。

プロトコルやプログラムなどにバグが一切ないことを数学的に証明することを“形式検証”という。形式検証は、それらに依拠する現代の高度IT社会における社会基盤の安全性の保障にとって本質的に必要な技術であり、特に量子コンピュータが実行する計算(量子計算)は、従来の計算機が実行する計算(古典計算)とは根本的に異なる原理を用いるため、その正しさを図や勘などで直観的に(数学的証明抜きで)示すことは困難だという。

これまでの研究においては、量子計算自体の形式検証は行われていたが、量子計算を制御する通信の同期スケジューリングに関する並行性まで含めた形式検証は、その背景となる論理体系が存在しなかったために困難とされていたとのこと。そこで研究チームは今回、並行量子通信プロトコルの形式検証を可能にする並行動的量子論理を提案することを目指したとする。

今回の研究では、オランダ・アムステルダム大学の数理論理学者らによって提案された、ノイマンらが提案した「量子論理」に量子計算の観点を取り入れることで生まれた「動的量子論理」に対し、並行性を扱える「プロセス代数(プロセス計算)」を組み合わせることで、並行量子通信プロトコルの形式検証を可能にする並行動的量子論理が提案された。なお並行性(並行計算)とは、複数の異なる計算を非決定論的に同時実行する計算のことで、各計算の開始・終了タイミングを通信によって操作する仕組みだ(並行性によって計算パターンが膨大に増加するため、人手による形式検証は困難となってしまう)。

また今回提案された並行動的量子論理に基づいて、自動的に正しさの証明を出力するツールも開発された。そして、いくつかの具体的な並行量子通信プロトコルに対し、高速に動作することが実証されたとする。この手法では、補題の発見と入力という人間の補助を一切必要としない完全な自動定理証明により形式検証が行われることが特徴であり、従来手法と比較して形式検証の労力を大幅に削減することが可能になったとした。

研究チームは今回の成果により、プロトコルやプログラムなどにバグが一切ないことを数学的に証明するという最大級の安全性を保障した高信頼量子計算の実現が可能になり、将来の安全・安心な量子ソフトウェア開発の基盤が整備されたとしている。