北陸先端科学技術大学院大学(JAIST)は12月19日、「並行動的量子論理」を提案し、それに基づく「並行量子通信プロトコル」の完全な自動形式検証、つまりヒトによる補助(補題の発見と入力)を一切必要とせず、従来手法と比較して労力を大幅に削減することが可能な、完全な自動定理証明による形式検証に初めて成功したことを発表した。
同成果は、JAIST コンピューティング科学研究領域の緒方和博教授、同・髙木翼准教授らの研究チームによるもの。詳細は、ソフトウェア工学と方法論に関する全般を扱う学術誌「ACM Transactions on Software Engineering and Methodology」に掲載された。
プロトコルやプログラムなどにバグが一切ないことを数学的に証明することを“形式検証”という。形式検証は、それらに依拠する現代の高度IT社会における社会基盤の安全性の保障にとって本質的に必要な技術であり、特に量子コンピュータが実行する計算(量子計算)は、従来の計算機が実行する計算(古典計算)とは根本的に異なる原理を用いるため、その正しさを図や勘などで直観的に(数学的証明抜きで)示すことは困難だという。