企画セッション1 [11月12日 (水) 10:30 – 12:30]
Organized Session 1 [Wednesday, November 12, 10:30 – 12:30]
データ化のフロンティア
The Frontier of Datafication
オーガナイザー：手嶋毅志 (株式会社リクルート)
Organizer: Takeshi Teshima (Recruit)
神窪 利絵 (University of Maryland)
Rie Kamikubo (University of Maryland)
TBD
中村 優吾 (九州大学 大学院 システム情報科学研究院)
Yugo Nakamura (Graduate School and Faculty of Information Science and Electrical Engineering, Kyushu University)
AIoT行動変容支援におけるデータ化の現在地と展望
本発表では、AIoT技術を起点とした習慣的行動変容支援における「データ化」の現状を、自身の研究事例（食生活やモバイルゲーム等）を通じて紹介する。また、LLMなど基盤モデルの登場による変化の潮流を踏まえ、今後の課題と展望について述べる。
西田 佳史 (東京科学大学)
Yoshifumi Nishida (Institute of Science Tokyo)
生活セントリックデザインのためのデータ利活用の課題
活科学の難しさは、生活者や生活状況の多様性、生活データの分散性、ステイクホルダーや生活介入における複雑性の問題に起因することが多い。講演者は、約20年に亘り子どもや高齢者の生活安全に関する学際的研究や社会実装活動を行ってきた。この中で生活関連データの収集や利活用に関して感じている課題とそれに向けた活動として、EBPM型の生活支援の課題、個人情報を取り巻く課題、行政機関が生活問題解決を行う際の課題、データ化のデザインおける課題、生活イノベーションに支援における問題などを紹介する。
企画セッション2 [11月13日 (木) 9:30 – 11:30]
Organized Session 2 [Thursday, November 13, 9:30 – 11:30]
AI×形式手法と数学
AI x Formal Methods and Mathematics
オーガナイザー：園田 翔 (理化学研究所・サイバーエージェント)，熊谷 亘 (OMRON SINIC X)
Organizer: Sho Sonoda (RIKEN / CyberAgent), Wataru Kumagai (OMRON SINIC X)
水野勇磨 (University College Cork)
Yuma Mizuno (University College Cork)
定理証明系による数学の形式化
定理証明系は、数学の定理や証明をコンピュータ上で厳密に記述・検証するツールである。このようなツールは、AIによる数学研究の実現においても重要な役割を果たすと期待されている。本講演では、定理証明系で数学を形式化するとはどういうことか、そして数学の形式化に関する最近の発展について、数学者であり定理証明系Leanのユーザーでもある講演者の立場から紹介を行う。
谷中瞳 (東京大学・理化学研究所)
Hitomi Yanaka (The University of Tokyo / RIKEN)
範疇文法と論理：理論と応用
範疇文法(categorial grammar)は自然言語の統語構造と意味解釈との対応が明示的かつ簡潔な文法体系であり、その経験的妥当性と形式的厳密性によって大規模言語モデル時代の現在においても計算論的言語学研究の重要な理論の一つである。本講演では範疇文法の理論を概説し、講演者の研究事例とともに、範疇文法と論理に基づく自然言語の実証的研究の現在と今後の可能性を議論する。
戸次大介 (お茶の水女子大学)
Daisuke Bekki (Ochanomizu University)
証明論による自然言語の意味の理論
論理の証明論は、数学の推論に基礎を与える目的で発展したが、近年著者らの研究により、依存型理論の証明論に基づいた意味の理論が、理論言語学で論じられてきた意味論の諸問題を統一的に解決する見通しが得られつつある。本講演では、そのような取り組みの一つである依存型意味論(dependent type semantics, DTS)の概略を説明するとともに、証明論が自然言語の意味について何を明らかにするのかを、数学の推論とも関連させつつ解説する。
Kaiyu Yang (Meta Fundamental AI Research)
Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification
AI for Mathematics (AI4Math) is intellectually intriguing and crucial for AI-driven system design and verification. Much of the recent progress in this field has paralleled advances in natural language processing, especially by training large language models on curated mathematical text datasets. As a complementary yet less explored avenue, formal mathematical reasoning is grounded in formal systems such as Lean, which can verify the correctness of reasoning and provide automatic feedback. This talk introduces the basics of AI for formal mathematical reasoning, focusing on two central tasks: theorem proving (generating formal proofs given theorem statements) and autoformalization (translating from informal to formal). I will highlight the unique challenges of these tasks through two recent projects: one on proving inequality problems from mathematics olympiads, and another on autoformalizing Euclidean geometry problems.
企画セッション3 [11月14日 (金) 9:45 – 11:45]
Organized Session 3 [Friday, November 14, 9:45 – 11:45]
アルゴリズム・データ構造と機械学習
Algorithms, Data Structures, and Machine Learning
オーガナイザー：坂上 晋作 (サイバーエージェント・NII・理研AIP)
Organizer: Shinsaku Sakaue (CyberAgent / NII / RIKEN AIP)
大城 泰平 (北海道大学・理化学研究所)
Taihei Oki (Hokkaido University / RIKEN)
離散凸解析に基づく予測付き離散最適化手法
予測付きアルゴリズムは，機械学習による予測を活用してアルゴリズムを改良する新しい研究分野である．本講演では，離散最適化アルゴリズムを高速化するための予測付きアルゴリズムについて，離散凸解析の視点から考える．離散凸解析は，通常の凸解析の離散最適化版にあたる理論であり，最大重み完全二部マッチングのためのハンガリアン法や，最小費用流のための逐次最短路法など，さまざまな離散最適化手法が離散凸関数に対する離散的な勾配降下法として理解される．この視点により，これらのアルゴリズムの反復回数は，初期解と最適解集合との距離として特徴づけられ，アルゴリズムのウォームスタート（予測解からの開始）の理論保証を自然に与える．本講演では，予測付き離散最適化手法を理解するための離散凸解析の基礎を，凸解析との対応を軸として紹介する．本講演は、坂上晋作氏 (CyberAgent・国立情報学研究所・理化学研究所) との共同研究に基づく．
小野 峻佑 (東京科学大学 情報理工学院)
Shunsuke Ono (School of Computing, Institute of Science Tokyo)
モデルベース × データドリブン ― Plug-and-Playアルゴリズムの展開
本講演では、「アルゴリズム設計」と「機械学習モデル」の融合を体現する信号復元手法として、Plug-and-Play（PnP）アルゴリズムを紹介する。PnPアルゴリズムは、最適化アルゴリズムの反復過程に学習済みノイズ除去器を組み込むことにより、計測モデルに基づく数理構造とデータドリブンな知識表現を同時に活用するアプローチである。
まず、PnPアルゴリズムを支える要素として、近接分離アルゴリズムとノイズ除去器の近接写像解釈を紹介する。次に、汎用的に適用できるPrimal-Dual SplittingベースのPnPアルゴリズム（PnP-PDS）を取り上げ、画像復元への応用例を示す。さらに、ノイズ除去器の「堅非拡大性」という数理的性質が、PnPアルゴリズムの収束保証の鍵となることを解説する。最後に今後の展望について触れる。
松井 勇佑 (東京大学 大学院情報理工学系研究科)
Yusuke Matsui (Graduate School of Information Science and Technology, The University of Tokyo)
学習型データ構造：機械学習を内包する新しいデータ構造の設計と解析
学習型データ構造とは、B-treeやブルームフィルタといった古典的なデータ構造に対し小さな機械学習モジュールを組み合わせることで性能を向上させる、新しいデータ構造である。例えばブルームフィルタは集合を表現する確率的データ構造であり、要素が集合に含まれるか近似的に判定するが、学習型ブルームフィルタはまず小さな機械学習モジュールで要素が集合に属するかざっくり判定し、その後に小さなブルームフィルタを適用する。このような構成は、最終的なメモリ・精度トレードオフに優れると報告されている。本講演では、近年発展を遂げている学習型データ構造の外観を示し、それが大規模言語モデルやコンピュータビジョンといった応用先にどのように用いられる可能性があるかを議論する。
企画セッション4 [11月14日 (金) 15:45 – 17:45]
Organized Session 4 [Friday, November 14, 15:45 – 17:45]
時系列データ解析と基盤モデル
Time Series Analysis and Foundation Models
オーガナイザー：勝木 孝行 (IBM東京基礎研究所)
Organizer: Takayuki Katsuki (IBM Research – Tokyo)
松原靖子 (大阪大学)
Yasuko Matsubara (The University of Osaka)
時系列ビッグデータのためのリアルタイム解析：基礎研究と社会実装
近年のIoTデバイスの急速な普及に伴い、産業、医療、環境等の様々な分野で、多数のデバイスから収集された時系列ビッグデータを高速に解析し、高度なサービスに活用しようとする動きが盛んである。本講演では、これまでに取り組んできた時系列ビッグデータ解析技術、特に、特徴自動抽出、非線形動的モデリング、複合時系列テンソル解析、リアルタイム要因分析・将来予測、小型エッジ学習等について概説するとともに、最新の研究成果（KDD2025 / 4件、AAAI2025 / oral 2件、ICLR2025 / oral 1件等）について紹介する。また、時系列ビッグデータ解析の応用例として、現在実施している社会実装に向けた具体的な産学・異分野連携の事例（製造業DX、医療AI等）をいくつか紹介する。
坂井 智哉 (IBM東京基礎研究所)
Tomoya Sakai (IBM Research – Tokyo)
時系列基盤モデル
TBD
尾亦 範泰 (宇宙航空研究開発機構, JAXA)
Noriyasu Omata (Japan Aerospace Exploration Agency, JAXA)
宇宙開発における時系列データ解析
TBD