形式検証によって、信頼できる量子時代を築く

量子計算の形式手法に関する研究室　
Laboratory on Formal Methods for Quantum Computing
講師：ド ミン カン（DO Minh Canh）

E-mail：
［研究分野］
形式手法、量子計算
［キーワード］
形式仕様、モデル検査、定理証明、量子計算、量子情報

研究を始めるのに必要な知識・能力

形式手法と量子計算に関心を持ち、高い意欲を備え、数学（特に数理論理と線形代数）に関する十分な知識と、強いプログラミング能力（C⁺⁺, Java, Python）を持つ学生を歓迎します。

この研究で身につく能力

本研究室では、量子システムを状態機械として形式化する方法、Maude や CafeOBJ などの形式仕様言語を用いて状態機械を記述する方法、そしてモデル検査や定理証明を用いて状態機械が望ましい性質を満たすことを形式的に検証する方法を学びます。これらの研究活動を通じて、学生は堅固な理論的基盤、高度な実践的スキル、そして従来技術と量子技術の双方を社会に役立つ形で発展させていく情熱を身につけることが期待されます。

【就職先企業・職種】 研究者、技術者

研究内容

近年、各国政府や大手企業による指数関数的な投資により、因数分解問題や離散対数問題を効率的に解くショアのアルゴリズムのような高度なアルゴリズムを実行可能な大規模量子コンピュータの構築は、ますます現実味を帯びてきています。しかし、その大きな可能性にもかかわらず、量子計算は量子力学のしばしば直観に反する原理に依存しているため、古典計算とは本質的に異なり、量子システムを正確に設計・実装することは容易ではありません。さらに、量子測定が非決定性や確率的な結果をもたらすため、従来のテスト技法は量子システムに対して大幅に効果が低下します。したがって、量子システムを実際に信頼して利用するためには、その正しさを保証する形式検証が不可欠です。私たちの研究は、量子計算のための形式手法に焦点を当てており、以下の研究テーマを含む（ただしこれらに限定されない）幅広い領域を対象としています。

「量子計算のための代数的仕様」

量子計算について記号的かつ厳密に推論することは形式検証に不可欠であり、代数的アプローチはその実現に向けた有望な方向性を提供します。本研究では、量子計算をモデル化し推論するための代数的仕様フレームワークを構築します。具体的には、複素数を厳密に表現するために環 D［ω］を用い、量子状態と量子操作を表現するためにディラック記法を採用し、さらに量子力学の法則やディラック記法で表される基底行列操作の法則を活用して、量子計算に関する推論を自動化します。この量子計算のための代数的仕様は、他の形式検証技法を構築するための基盤となる形式フレームワークとして機能することが期待されます。

「量子システムの形式仕様と形式検証のための、統一的で表現力が高く、かつスケーラブルなフレームワーク」

形式検証技法がシステムの正しさを判断するためには、システム仕様と性質仕様の両方が必要です。本研究では、並行性や通信を含む幅広い量子システムをモデル化できる強力な形式仕様言語と、モデル検査から定理証明までスケールする形式検証技法を開発します。特に、参加者間の並行動作や通信を論理的に記述するための枠組みとして Concurrent Dynamic Quantum Logic を導入します。さらに、量子計算のための代数仕様と各種最適化技法に基づき、検証プロセスを自動化し、並行性や通信によって生じる膨大なインターリーブを効果的に扱うことを可能にします。

「形式意味論に基づく検証可能な再帰的量子プログラミング言語」

手続きや再帰は、プログラムをモジュール的かつスケーラブルに構成するための基本的な機能です。本研究では、量子計算の特有の利点を損なうことなく、量子システムのモジュール設計を可能にし、その形式意味論に基づいて厳密な形式検証を行える再帰的量子プログラミング言語を開発します。具体的には、基本的な構成要素と再帰的手続き呼び出しをすべてサポートするための構文と操作的意味論を導入します。そして、この意味論に基づき、量子プログラムを記述し、その正しさを自動的に検証するためのフレームワークを構築します。

主な研究業績

1. Canh Minh Do, Adrián Riesco, Santiago Escobar, Kazuhiro Ogata. “Parallel Maude-NPA for Cryptographic Protocol Analysis”, IEEE Transactions on Dependable and Secure Computing, 12(6): 6714-6731, IEEE, 2025.
2. Canh Minh Do, Tsubasa Takagi, Kazuhiro Ogata. “Automated Quantum Protocol Verification Based on Concurrent Dynamic Quantum Logic”, ACM Transactions on Software Engineering and Methodology, 34(6): 1-36, ACM, 2025.
3. Canh Minh Do, Yati Phyo, Adrián Riesco, Kazuhiro Ogata. “Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way”, ACM Transactions on Software Engineering and Methodology, 32(6): 1-38, ACM, 2023.

使用装置

Maude（書換え論理に基づく仕様／プログラミング言語）
CafeOBJ（高度な形式仕様・検証言語）
MacPros（実験のための高性能計算環境）