| 研究課題/領域番号 |
22KJ1483
|
|---|
| 配分区分 | 基金 |
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
高木 翼 東京工業大学, 情報理工学院, 特別研究員(PD)
|
|---|
| 研究期間 (年度) |
2023-03-08 – 2025-03-31
|
| キーワード | 量子論理 / 動的論理 / Maude / 形式検証 / 量子プログラム / 量子プロトコル |
|---|
| 研究実績の概要 |
本年度は簡略化された動的量子論理(Basic Dynamic Quantum Logic, BDQL)に基づいて量子プログラムを形式検証する手法を提案した。また、その手法に基づいて自動的に形式検証を実行するツールをプログラミング言語Maudeによって実装した。さらに、ケース・スタディとして、超密度符号化、量子テレポーテーション、量子秘密分散、量子もつれスワッピング、量子ゲートテレポーテーションの5つの量子プロトコルに加え、それらの変種である、量子リレースキーム、双方向量子テレポーテーション、二量子ビットテレポーテーション、量子ネットワークコーディングの4つの量子プロトコルの自動形式検証に成功した。本ツールは、動的量子論理に基づく実装としては世界初の実装であり、従来の手法と比較して高度な自動化が達成されている。つまり、補題やヒューリスティクスによって定理証明を人間が誘導（補助）する必要は一切なく、量子プログラムと仕様（満たすべき性質）を入力するだけで自動的にそのプログラムが仕様を満たすかどうかの判定が行われる。また、いずれのプロトコルも数秒以内に検証が完了しており、ツールの実行速度としては十分満足できるものになった。特に、今回検証した最大のプロトコルである量子ネットワークコーディングは14量子ビットのプロトコルであり、その検証は4秒程度で完了した。計算機に依存しない指標である書き換えステップ数については約1000万ステップとなった。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初の予定通り、前年度に構築した数理論理体系に基づいて、今年度は具体的な量子プログラムの検証を行うことができた。また、当初想定していたよりも多くの量子プログラムの検証を行えたため、進捗としては十分なものになったといえる。
|
| 今後の研究の推進方策 |
今後は本年度の成果をさらに発展させ、検証可能な量子プログラムの種類を増やしていくことを目指す。
|
| 次年度使用額が生じた理由 |
研究の進捗状況を鑑みて当初参加を予定していた学会への参加を見送ったため。代わりに、次年度で当該学会に参加する予定である。
|
