今後の開催予定
- 第5回
- 日時: 2025年9月19日（金）16:00 開始（15:30 開場）
- 場所: 国立情報学研究所 20階 2005講義室1-2004講義室2
- 講演者：脇坂 遼氏（京都大学）
- 講演タイトル：Online Job Scheduler for Fault-Tolerant Quantum Multiprogramming
- 概要：本講演では、我々が最近取り組み始めた誤り耐性量子計算(FTQC)時代のマルチプログラミングのための
ジョブスケジューラに関する研究について紹介する。マルチプログラミングは複数のジョブを並行に実行
することによってプロセッサ利用率を高める技術であり、ランニングコストの大きい量子計算機では特に
重要な技術の1つとされている。本研究では FTQC の中でも特に格子手術 (lattice surgery)と呼ばれる手法を
対象としたジョブスケジューリング問題を定式化し、それを解くための 3D bin packing 問題 (3D-BPP) に
基づくスケジューリング手法を提案する。さらに、量子プロセッサにおいても断片化と呼ばれる問題が
起こり得ることを発見し、それを解消する軽量なデフラグメンテーションアルゴリズムを新たに導入する。
本研究には多くの展望・課題が残されており、本講演ではそれらについても重きを置いて紹介する予定である。
過去の開催履歴
クリックすると詳細が表示されます．
第4回：2025年5月19日 | 渡邊 和樹 | 形式検証の構造とアルゴリズム
- 日時：2025年5月19日（月）16:30 開始
- 場所：国立情報学研究所 12階 1208室
- 講演者：渡邊 和樹
- 所属：国立情報学研究所
- 講演タイトル：形式検証の構造とアルゴリズム
- 概要：本講演では、講演者らが取り組んできた形式検証の研究を複数紹介する。具体的には、 1) 形式検証における”構造”を適切に抽象化することにより、その本質を明らかにすること、 2) 確率的なシステムに対する効率的な形式検証アルゴリズムの開発、 の二点のいずれか、もしくは双方に関連した最近の研究を紹介する。 本講演で紹介する研究はそれぞれ、 1) Anton Varonka & Kazuki Watanabe, Preprint, 2) Mayuko Kori, Kazuki Watanabe, Jurriaan Rot, To Appear in LICS25, 3) Mayuko Kori & Kazuki Watanabe, Preprint, 4) Kazuki Watanabe & Noboru Isobe, Preprint 及び進行中の研究に基づいている。
第3回：2025年2月27日 | 佐藤 哲也 | 差分プライバシーの検証と形式化
- 日時：2025年2月27日 (木) 16:30 開始
- 場所：東京科学大学 大岡山キャンパス 西8号館 W1008号室
- 講演者：佐藤 哲也
- 所属：東京科学大学 (南出研 助教)
- 講演タイトル：差分プライバシーの検証と形式化
- 講演資料
- 概要：本講演では、差分プライバシーの概要と、圏論的特徴づけの研究、最近行っているIsabelle/HOLによる形式化について紹介する。差分プライバシーとは、データベースの統計的なプライバシー基準とそれを実現する為のノイズ付加手法を指す。多くの応用が存在し、iOS の入力候補の推定や、Google Maps の混雑状況の算出、アメリカの国勢調査などにおける匿名化などに用いられている。こうした差分プライバシーを検証するためのシステムの数学的基礎として、講演者は関係持ち上げによる圏論的特徴づけの研究を行い、差分プライバシーの元となる統計的距離の圏論的性質を調べた。Isabelle/HOLによる形式化・検証については、基本的な部分が組みあがったところで、Future Workがいくつかあるのでそれも紹介したい。
第2回：2024年12月19日 | 松下 祐介 | 量子、並列、所有権
- 日時：2024年12月19日 (木) 16:00 開始 (開場予定 15:30)
- 場所：国立情報学研究所(NII) 1208・1210会議室
- 講演者：松下 祐介
- 所属：京都大学 (五十嵐・末永研 特別研究員(PD))
- 講演タイトル：量子、並列、所有権
- 講演資料
- 概要：この講演では、私・平田賢吾氏・脇坂遼氏の現在進行中の共同研究である、細粒度の並列化のための並行量子分離論理について発表します。 私たちの論理では、細粒度の並列化で性能を上げた量子プログラムをモジュラーに検証できます。特に、同じ量子ビットを操作するが意味論的にはデータ競合がない並列プロセスについて推論できます。また、ある種の完全性も満たします。そのための鍵となる仕組みは、柔軟な共有を可能にする、量子メモリに対する新しい形の所有権です。
第1回：2024年11月6日 | 酒寄 健 | Semantics of circuit description language with dependent type-and-effect systems
- 日時：2024年11月6日 (水) 17:00 開始
- 場所：東京大学理学部７号館 214教室
- 講演者：酒寄 健
- 所属：東京大学 (小林研 助教)
- 講演タイトル：Semantics of circuit description language with dependent type-and-effect systems
- 概要：Circuit description languages, such as Proto-Quipper, are high-level languages used to describe and generate circuits, a quintessential example being the quantum circuit. To statically estimate the resources used in a circuit generated by Proto-Quipper, a dependent type-and-effect system was recently developed.
In this talk, I will discuss the denotational side of this story in a step-by-step manner.
First, the categorical semantics for a variant of the simply typed Proto-Quipper will be given using an indexed (aka parameterized) monad that handles the effect of circuit generations. Then, ideas to extend this semantics for dependent types and effect systems will be presented independently. Finally, I’ll explain my attempts to unify these extensions (which I still haven’t succeeded in). If time allows, I would also like to discuss with the audience whether this concrete semantic model for circuits can be generalized and applied in other contexts. This is a joint ongoing work with Andrea Colledan and Ugo Dal Lago.
運営委員
2025年度
2024年度
発起人