| 研究課題/領域番号 |
22KJ1483
|
|---|
| 補助金の研究課題番号 |
22J23575 (2022)
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 基金 (2023)
補助金 (2022) |
|---|
| 応募区分 | 国内 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 東京工業大学 (2023)
北陸先端科学技術大学院大学 (2022) |
|---|
研究代表者 |
高木 翼 東京工業大学, 情報理工学院, 特別研究員(PD)
|
|---|
| 研究期間 (年度) |
2023-03-08 – 2025-03-31
|
| 研究課題ステータス |
中途終了 (2023年度)
|
| 配分額 *注記 |
2,500千円 (直接経費: 2,500千円)
2024年度: 800千円 (直接経費: 800千円)
2023年度: 800千円 (直接経費: 800千円)
2022年度: 900千円 (直接経費: 900千円)
|
|---|
| キーワード | 量子論理 / 動的論理 / Maude / 形式検証 / 量子プログラム / 量子プロトコル / 線形時相論理 / 様相論理 / 動的代数 |
|---|
| 研究開始時の研究の概要 |
本研究は、1936年以来量子計算とは無関係に発展してきた量子論理を量子計算の形式検証の補助という観点から見直し、現代的な論理に生まれ変わらせることを目的とする。具体的には、動的論理の発想（プログラムの実行を様相演算子により表現する）を取り入れ、動的量子論理を定式化する。また、その有効性を示すため、具体的な量子プロトコル、例えば超密度符号化、量子テレポーテーション、量子秘密分散、量子もつれスワッピング、量子ゲートテレポーテーション等の仕様記述を動的量子論理によって行い、それに基づく形式検証を自動化するツールを開発する。さらに、以上の成果を発展させ、量子通信ネットワークの仕様記述・形式検証を行う。
|
| 研究実績の概要 |
本年度は簡略化された動的量子論理(Basic Dynamic Quantum Logic, BDQL)に基づいて量子プログラムを形式検証する手法を提案した。また、その手法に基づいて自動的に形式検証を実行するツールをプログラミング言語Maudeによって実装した。さらに、ケース・スタディとして、超密度符号化、量子テレポーテーション、量子秘密分散、量子もつれスワッピング、量子ゲートテレポーテーションの5つの量子プロトコルに加え、それらの変種である、量子リレースキーム、双方向量子テレポーテーション、二量子ビットテレポーテーション、量子ネットワークコーディングの4つの量子プロトコルの自動形式検証に成功した。本ツールは、動的量子論理に基づく実装としては世界初の実装であり、従来の手法と比較して高度な自動化が達成されている。つまり、補題やヒューリスティクスによって定理証明を人間が誘導（補助）する必要は一切なく、量子プログラムと仕様（満たすべき性質）を入力するだけで自動的にそのプログラムが仕様を満たすかどうかの判定が行われる。また、いずれのプロトコルも数秒以内に検証が完了しており、ツールの実行速度としては十分満足できるものになった。特に、今回検証した最大のプロトコルである量子ネットワークコーディングは14量子ビットのプロトコルであり、その検証は4秒程度で完了した。計算機に依存しない指標である書き換えステップ数については約1000万ステップとなった。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初の予定通り、前年度に構築した数理論理体系に基づいて、今年度は具体的な量子プログラムの検証を行うことができた。また、当初想定していたよりも多くの量子プログラムの検証を行えたため、進捗としては十分なものになったといえる。
|
| 今後の研究の推進方策 |
今後は本年度の成果をさらに発展させ、検証可能な量子プログラムの種類を増やしていくことを目指す。
|
