計算機科学の理論的基盤を構築する

髙木(翼)研究室　TAKAGI Laboratory
准教授：髙木 翼（TAKAGI Tsubasa）

E-mail：
［研究分野］
理論計算機科学、数理論理学、形式検証、量子計算
［キーワード］
多ソート等式論理、様相論理、動的論理（ホーア論理）、時相論理（モデル検査）、量子論理

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

単に計算機を道具として使用するだけでなく、計算機の仕組みを理解したい（考案したい）という動機があるとよいでしょう。そのような動機さえあれば配属前に必要な知識はなく、配属後に学修を開始しても遅くはありません。

この研究で身につく能力

本研究室では、確かな論理的/ 数学的思考力に基づいて社会の問題を解決する能力を身につけます。このような能力は修了後にどのような職種に就いても必要になる汎用的かつ応用性の高い能力です。

【就職先企業・職種】 情報通信・情報処理産業、大学や企業の研究職など

研究内容

　計算機科学の一つの重要な理論的基礎は数理論理学に求めることができます。数理論理学はコンピュータが誕生する以前の時代に生まれ、コンピュータの誕生と発展に深く関わってきました。本研究室では、数理論理学を用いて、特に量子計算（量子プロトコル・量子プログラム）の正しさを厳密に証明する研究に取り組んでいます。
　量子計算は古典計算とは根本的に異なる原理に基づく計算であり、テストによるデバッグが困難です。その理由として、（1）途中状態の確認行為がその状態を変化させる（観測による状態崩壊）、（2）同じ測定でも異なる測定値が確率的に得られる（観測の非決定性）、（3）同じ状態を複製できない（no-cloning 定理）といった量子力学に由来する現象が影響しています。このような理由で従来の直観が働きにくい量子計算の信頼性を高めるためには、量子計算の設計が正しいことの数学的証明（形式検証）が重要になります。
　一方で、古典計算に目を向けると、古典計算の形式検証には長い歴史があります。その結果、多ソート等式論理や様相論理（動的論理や時相論理）などの数理論理がその目的のために有効であるということが分かってきました。そこで、本研究室ではこれらの数理論理を改良もしくは拡張することで量子計算の形式検証を実践しています。

【多ソート等式論理に基づく量子計算の形式検証】

　形式検証を行うためには、まずはシステムやプログラムの仕様を数学的に厳密に記述する必要があります。特に、等式で表現される厳密な仕様（代数的仕様）の理論的基礎を与えるのが多ソート等式論理であり、その仕様に基づく等式推論によって形式検証が実行されます。この手法は古典計算の形式検証において大きな成功を収めました。
　そこで、この手法に倣い、多ソート等式論理に基づいて量子計算の代数的仕様を与えることは自然な発想です。本研究では、さらに進んで量子計算の代数的仕様をプログラミングによって古典計算機に読み込ませることで自動的な形式検証を行うことに成功しました。

【動的量子論理に基づく量子計算の形式検証】

　古典形式検証を出発点とするのではなく、量子計算の論理とは何かという疑問を出発点とするのも興味深い方向性です。コンピュータの父とよばれるジョン・フォン・ノイマンらは1936年に量子力学の論理として量子論理を創始しました。量子計算の誕生はその半世紀後なので、当然この時点では量子論理と量子計算は無関係です。では、量子計算の観点を取り入れることで量子論理を現代的な論理に生まれ変わらせるにはどうすればよいのでしょうか。
　それに対する一つの回答が、ホーア論理を拡張した動的論理と量子論理を組み合わせた動的量子論理です。本研究では動的量子論理の代数を考えることで、それに基づいて様々な量子プログラムの形式検証をホーア論理と同様の方法で行うことに成功しました。動的量子論理は単に数学的構造としてみても興味深く、その性質の探究は量子計算の理解にも役立ちます。

主な研究業績

1. Tsubasa Takagi, Semantic Analysis of a Linear Temporal Extension of Quantum Logic and Its Dynamic Aspect. ACM Transactions on Computational Logic, 24(3): 1-21, ACM, 2023.
2. Tsubasa Takagi, Canh Minh Do, Kazuhiro Ogata, Automated Quantum Program Verification in Dynamic Quantum Logic. In Proceedings of DaLí: Dynamic Logic – New Trends and Applications, Lecture Notes in Computer Science (LNCS), 14401: 68- 84, 2024.
3. Tsubasa Takagi, An Algebra of Quantum Programs with the Kleene Star Operator. In Proceedings of International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols, CEUR Workshop Proceedings, 3280: 2-15, 2022.