会場: 京都大学数理解析研究所 111号室
開催形式: 対面形式のみ
組織委員: 石渡哲哉(代表), 園田翔, 田中吉太郎, 中井拳吾(代表), 本田あおい
本共同研究の目的: 本共同研究(公開型)では、機械学習の数理的研究を牽引する研究者をはじめ、数値解析、微分方程式論、統計学、確率解析など関連分野からの多様な専門家を招集し、分野横断的な議論を行う。また、若手研究者や大学院生にも積極的に参加を呼びかけ最新の知見を共有するとともに、分野を超えた研究ネットワークの形成の第一歩とする。これにより、数理的研究に基づく機械学習のさらなる発展と、理論と応用の両面における新たな知見の創出を目指す。
プログラム (PDF版プログラムはこちら)
講演時間60分のあと10分程度の質疑応答・議論の時間を想定しています。
ただし、ショートコミュニケーションは講演時間20分のあと5分程度の質疑応答・議論の時間を想定しています。
5月27日(水) 12:30 開場 (予定)
12:55 オープニング・諸連絡
13:00-14:10 園田 翔(理化学研究所/サイバーエージェント)
「定理証明AIの統計的な証明可能性」
14:30-15:20 ショートコミュニケーション
大石 悟(大阪大学)
「吸引的低次元空間へのアトラクタ再構成を通じたカオス再現の安定化」
Yuanhe Zhang(University of Warwick/RIKEN AIP)
「Harness design for long-running autoformalization of research-level mathematics in Lean 4 」
15:40-16:50 田中 剛平(名古屋工業大学)
「リザバーコンピューティングと適応的学習」
5月28日(木) 9:30 開場 (予定)
10:00-11:10 川島 貴大(ZOZO研究所)
「集合間Bregmanダイバージェンスと置換不変NNによるその学習」
11:30-12:20 ショートコミュニケーション
中村 優真(金沢大学)
「広範な物理系を計算資源として活用するアンサンブルリザバー計算 」
折池雄太(株式会社サイバーエージェント)
「数学問題に対する AI 支援推論の実践 」
14:00-15:10 米田 剛(一橋大学)
「ベイズ最適化と随伴法で探る:滑らかなオイラー流における渦輪の非線形・局所スケール変形」
15:30-16:40 若山 智哉(理化学研究所)
「ベイズ推定に基づく文脈内学習のメタ学習的挙動の解析」
5月29日(金) 9:10 開場 (予定)
9:30-10:40 古屋 貴士(同志社大学)
「測度論的トランスフォーマーの理論解析」
11:00-12:10 原 誠人(京都大学)
「力学系のリザバー計算」
12:20 クロージング
各講演の概要(順次更新予定)
園田 翔(理化学研究所/サイバーエージェント) 「定理証明AIの統計的な証明可能性」
AI定理証明によって証明ができる仕組みを,証明完了状態に到達する確率「統計的証明可能性」に着目して解析する.形式的証明探索をMDPとしてモデル化し,学習済み証明器と最適証明器の差を理論的に評価することで,数学AIが機能する条件を調べる.
https://arxiv.org/abs/2602.10538
https://arxiv.org/abs/2602.10512
―――――
大石 悟(大阪大学) 「吸引的低次元空間へのアトラクタ再構成を通じたカオス再現の安定化」
データ駆動力学系学習器は、その内部にTargetカオス力学系のアトラクタを再構成することで、時系列予測や力学系再現を実現できる。
本公演では、学習器内の表現空間のどこにアトラクタが再構成されるべきか、という観点に焦点をあてる。
吸引的な低次元部分空間にアトラクタを再構成する手法[1]を中心に紹介し、カオス力学系再現をロバストに達成できることを示す。
[1] https://doi.org/10.48550/arXiv.2602.11069
―――――
Yuanhe Zhang(University of Warwick/RIKEN AIP) 「Harness design for long-running autoformalization of research-level mathematics in Lean 4」
We present a harness design for research-paper-length agentic autoformalization. We target Erdős problems to study how harness engineering can make long-running mathematical agents legible, recoverable, and capable of sustained Lean formalization.
―――――
田中 剛平(名古屋工業大学) 「リザバーコンピューティングと適応的学習」
時系列データの増大や環境の複雑化に伴い,変化する状況に柔軟に対応可能な情報処理技術が求められている.本講演では,動的システムの非線形応答を活用する計算パラダイムであるリザバーコンピューティングと変化に応じてモデルを更新する適応的学習に焦点をあてる.両者を統合した手法を中心として,いくつかの関連する研究事例を紹介し,今後の展望について議論する.
―――――
川島 貴大(ZOZO研究所) 「集合間Bregmanダイバージェンスと置換不変NNによるその学習」
Bregmanダイバージェンスは凸関数から導かれる連続空間上の擬距離で,統計学や機械学習において根幹的な役割を果たしている.同様に離散空間上で凸関数のアナロジーを利用してBregmanダイバージェンスを定義することにより離散構造をもつインスタンス間の乖離を柔軟に測ることが可能になると期待されるが,その構成法や妥当性は非自明である.
本発表では有限集合間のダイバージェンスとして母関数を集合関数としたDifference-of-Submodular Bregmanダイバージェンスを紹介し,加えて置換不変ニューラルネットワークを通した学習の枠組みについても議論する.
―――――
中村 優真(金沢大学) 「広範な物理系を計算資源として活用するアンサンブルリザバー計算」
リザバー計算は物理系を計算機として利用するための有望な方法として注目を浴びている.しかし周期系,カオス系はこれまでリザバー計算としては利用困難であると考えられていた.一方で,こうした系の中にはSpin-torque osicillatorのように計算機として有望な候補も含まれている.本研究ではこうした系を利用するための新しいフレームワークを開発し,その有効性について検証を行った.結果的に,従来は利用困難と考えられてきた系も,情報処理装置として利用可能であることを示した.
―――――
折池雄太(株式会社サイバーエージェント) 「数学問題に対する AI 支援推論の実践 」
本講演では、Erdős Problems に掲載された数学の問題を題材に、大規模言語モデルを用いた証明探索およびLean形式化支援の実践について報告する。一部の問題については、TeXで記述された問題文から自然言語による証明を生成し、その妥当性をレビューしたうえで形式化を試みた。形式化の過程では、Lean proof sketchの生成、サブゴール分解、未完成部分の補完、ローカル環境におけるコンパイルエラー修正といった反復的な作業を行った。これらの実践を通じて、数学研究における大規模言語モデルの有効性と限界を議論する。
―――――
米田 剛(一橋大学) 「ベイズ最適化と随伴法で探る:滑らかなオイラー流における渦輪の非線形・局所スケール変形」
渦輪における楕円不安定性は線形理論として古くから知られているが、実際に観測される渦構造の非線形かつスケール局所的な変形を統一的に説明する理論はこれまで存在しなかった。本研究では、非圧縮三次元オイラー方程式のもとで、ケルビン波を伴いながら半径方向に拡大する渦輪のラグランジュダイナミクスを解析する。
そのために、圧力の特異積分表現に依存しない幾何学的ラグランジュ枠組みを構築し、渦運動を支配する新たな波動方程式を導出する。本枠組みにより、従来の線形不安定性解析では捉えられなかった、渦構造のスケール局所的変形を駆動する内在的な非線形メカニズムを初めて明らかにする。
さらに、そのメカニズムの寄与を定量的に評価するために、ベイズ的な大域探索と随伴法による局所最適化を組み合わせた機械学習ベースのハイブリッド最適化手法を構築する。対象とする最適化問題は強い非凸性を有し、随伴法単独では局所解に陥るが、本手法により、より優れた解の探索が可能となることを示す。
―――――
若山 智哉(理化学研究所) 「ベイズ推定に基づく文脈内学習のメタ学習的挙動の解析」
本講演では、Transformerの文脈内学習(ICL)をメタ学習として捉え、有限サンプルでの誤差を解析する。ICLの誤差を、有限データで事前学習したモデルが理想的なベイズ予測器を再現する際の「近似誤差+推定誤差」と、理想的な予測器でも減らすことのできない「タスク自体に残る不可避な不確実性」に分解して解析する。モデルのデプロイ時において、混合タスク環境でも少数の例から真のタスクを素早く識別し、その後の誤差は真のタスクの難しさに支配されることを示す。
―――――
古屋 貴士(同志社大学) 「測度論的トランスフォーマーの理論解析」
本講演では、無限個のトークンを扱うための自然な枠組みとして、トランスフォーマーを測度の集合上の写像として定式化し、その近似理論および訓練に関する理論解析の成果について報告する。
―――――
原 誠人(京都大学) 「力学系のリザバー計算」
リザバー計算は,中間層(リザバー)を与えられた入力駆動型力学系とし,出力層のみを線型回帰など簡単な最適化手法で学習するような機械学習法の総称である.本講演では,リザバーとして回帰型ニューラルネットワークを用いた場合(エコーステートネットワーク:ESN)に関して,力学系から生成される時系列を適切に学習したリザバーが,学習後にはもとの力学系とある弱い意味で「同じ」になり得ることを示した数学的結果の概略を紹介する.これにより,リザバー計算による決定論的時系列予測がなぜ機能するのかという原理が少なくとも部分的に理解される.その他に,現在までのところ十分な数学的説明が与えられていないものの,講演者が特に興味をもっている数値的現象のいくつかについても議論したい.
―――――
◆昨年度のRIMS共同研究(公開型)「」のページ
https://sites.google.com/view/rims-ml-2025/