連絡先
- 教員名：高木翼（准教授）
- 所属：北陸先端科学技術大学院大学 (JAIST)、情報科学系、コンピューティング科学研究領域
- メールアドレス：
- 部屋：I-54b（情報科学系研究棟5階）
- 当研究室にご関心のある方は、メールで直接問い合わせるか大学院進学相談会をご利用ください（オンライン面談可）
研究テーマ
当研究室では、形式検証による高信頼量子システムの実現に取り組んでいます。量子力学的な性質を利用したコンピュータやネットワーク（量子コンピュータ・量子通信ネットワーク）は、従来のコンピュータやネットワークよりも高速あるいは安全な計算を実行できると考えられています。しかし、量子計算は従来の計算とは根本的に異なる複雑な仕組みをもつため、設計した量子計算が正しいか（仕様を充たすか）の検証は簡単ではありません。そこで、数理論理学という背景理論によって支えられた形式検証という技術によって、量子計算が正しいことを厳密に保証することで、非常に高い信頼性（安全性）を備えた量子システムの実現を目指しています。
研究紹介
学生指導方針
- 確かな研究実績（学会発表や論文出版）を積んで就活に臨みたい、あるいは博士課程に進学したい方を歓迎し、そのためのサポートを惜しみません
- 学生の積極的な査読あり国際会議での研究発表を推奨
- 当研究室の学生の実績：M2学生が国際会議SFPVV 2025に論文採択、M1学生が国際会議QCNC 2026に論文採択、M1学生が国際会議TASE 2026に論文採択、M2学生が国際会議ISSSR 2026に論文採択（学年は当時で全員別の学生）
- このように、本人の努力次第ではありますが、M1もしくはM2という入学後直ぐの時期から業績を積める環境が整っています
- 国際会議/国内学会に参加するための参加費・旅費・宿泊費は研究室が全額負担
- 当研究室の学生が国立研究開発法人科学技術振興機構（JST）の2026年度次世代研究者挑戦的研究プログラム（SPRING）に採択されました
- 当研究室の学生が独立行政法人情報処理推進機構（IPA）の2026年度未踏ターゲット事業（量子コンピューティング技術を活用したソフトウェア開発分野）に採択されました
よくある質問
- Q. 配属前に最低限修得しておくべきことは？（博士前期課程）
- A. 一階述語論理式の読み書き、素朴集合論（集合、関係、関数、同値類、集合族）に関する（標準的な難易度の）証明問題が解けること。これら二つを難しく感じるなら、当研究室でやっていくのは厳しいかもしれません。要は、最低限の数学的な抽象的思考力が必須です。
- Q. 配属前に最低限修得しておくべきことは？（博士後期課程）
- A. 上述の能力に加え、国際会議で学術的な会話ができる程度の英語力を求めます。
- Q. 配属後に何を学ぶ？
- A. 量子計算、代数的仕様、モデル検査（時相論理や分散プロトコル）の基本事項などを学びます。
- Q. 研究テーマは自分で決めれる？
- A. 責任ある指導をするために、博士前期課程の間は、こちらが提示する複数の候補から相談の上決定します。博士後期課程からは自由です。
- Q. 研究室のイベントは？
- A. 週に一度のミーティング（参加必須）、年に一度の研究室合宿（参加自由）、新歓、送別会
- Q. コアタイムはある？
- A. ありませんが、土日祝日や帰省中など以外は研究室に毎日一度は顔を出すことを推奨。来ることで研究のモチベーションを維持できます。
- Q. 金銭的支援はある？
- A. 希望に応じて博士前期課程の学生に業務を割り振ることがあります（当然謝金を払います）。博士後期課程の学生は希望者全員をUA (University Assistant)として採用し謝金を払います。
構成員
- 高木 翼（准教授）
- 宋 阳（研究員）
- 名越 龍一（D1）：測定型量子計算の形式検証（PPL 2025 ⁄ PRO 2025 ⁄ SFPVV 2025 ⁄ ISQR 2025 ⁄ PPL 2026 ⁄ KSE 2026 ⁄ SFPVV 2026）
- 佐藤 直人（M2, 東京社会人コース）：量子算術演算回路の形式検証（PPL 2026 ⁄ ISSSR 2026）
- 小林 脩亮（M2）：
- 山口 快（M2）：
- 魯 珍赫（M2）：数学的帰納法による量子ルーティングの形式検証
- Yunhao Ni（M2）：整礎帰納法と項詳細化による形式検証
- 石橋 和愛（M1）：
- 山下 朋晃（M1）：
- Muhammad Shafiq Irfan Bin Mohd Naim（インターンシップ）
当研究室では、ポスドク研究員を公募しています．
修了生
【博士前期課程】
- 内田 隆貴（2026年度修了）：量子通信プロトコルの形式検証
- 中村 太陽（2025年度修了）：量子通信プロトコルの調査研究
- 名越 龍一（2025年度修了）：Improving Reliability of Measurement-based Quantum Computation by Formal Verification
【博士後期課程】