開催日：2026/11/17～2026/11/20

記号計算の高速化と産業課題解決への応用4｜2026a010

開催概要

プログラム

11⽉17⽇（火）非公開

11⽉18⽇（⽔）

9:30‒9:35　

研究代表者挨拶

9:35‒10:15

講演者：⽯原侑樹（⽇本⼤学）
講演タイトル：記号計算って、何？〜産業での活⽤例を通じて〜
アブストラクト：記号計算とは、数式をコンピュータ上で記号のまま扱い、式の
変形や⽅程式の求解などを⾏う計算⽅法である。本講演では「記号計算」を初め
て知る⽅を対象に、数値計算との違いや基本的な考え⽅を分かりやすく紹介する。
また、これまでの九州⼤学IMI共同利⽤研究「記号計算の⾼速化と産業課題解決
への応⽤」で取り上げられた事例を振り返り、暗号、制御、最適化、機械学習な
どの産業課題に記号計算がどのように役⽴つのかを紹介する。

10:30‒11:30

講演者：横⼭和弘（⽴教⼤学）【オンライン講演】
講演タイトル：グレブナー基底の種々のアルゴリズム
アブストラクト：記号計算において重要な概念である「グレブナー基底」につい
て、専⾨家である横⼭和弘先⽣にご解説いただきます。

11:30‒13:00

昼休憩

13:00‒14:00

講演者：坂⽥康亮（東京⼤学）
講演タイトル：MQ 問題を⾼速に解くグレブナ基底計算の理論と実装
アブストラクト：MQ 問題は，次世代暗号候補の⼀つである多変数多項式暗号の
安全性の根拠であり，その計算困難性を明らかにすることは重要な課題である．
この講演では，2023年に坂⽥・⾼⽊により提案され，MQ Challenge にて新記録
を出した，MQ 問題を⾼速に解くアルゴリズムについて紹介する．この⽅法は，
ランダムに⽣成されたMQ問題が⼀般性を持つことを利⽤した効率化を⾏ってお
り，その理論を説明する．また，グレブナ基底における記号計算の実装上の⾼速
化についても説明する．

14:15‒15:15

講演者：⼤塚敏之（京都⼤学）
講演タイトル：システム制御における関数表現：最適制御の陰関数表現と⾮線形
モデルの厳密な構造簡略化
アブストラクト：動的システムの解析と制御では、⾮線形なモデルや制御則をど
のように表現するかが計算のしやすさを左右する。本講演では、最適制御問題に
おける陰関数表現の活⽤として、逐次消去法と代数的勾配解を紹介する。また、
変数の拡張により⾮線形システムや⾮線形関数を単純な構造の動的システムで厳
密に表現する⽅法も紹介する。変数の消去と拡張という⼆つの観点から、記号計
算の役割と今後の課題を論じる。

15:30‒16:30

講演者：加藤祥太（京都⼤学）
講演タイトル：数式情報とデータに基づく物理モデル構築の⾃動化
アブストラクト：物理モデル構築では、⽂献に記述された数式や知識と、実験・
シミュレーションデータの双⽅が重要な情報源となる。本講演では、⽂献から数
式やモデル構造を抽出して物理モデルを構築するAutoPMoBと、数値データから
⽀配⽅程式を探索するシンボリック回帰を紹介する。異なる情報源から数式モデ
ルを構築する⼆つのアプローチを通じて、その⾃動化における課題を議論する。

17:00

懇親会

11 ⽉19 ⽇（⽊）

9:30‒9:35

2 ⽇⽬挨拶

9:35‒10:35

講演者：神⼾祐太（三菱電機株式会社）
講演タイトル：AI時代の記号計算の展開と展望
アブストラクト：近年のAI 技術の数学への応⽤技術の発展は⽬覚ましく、特に、
⼤規模⾔語モデルをベースとしたAIエージェントの組み合わせによる、未解決問
題の検証やその解決については、ミレニアム問題の⼀つであるナビエ・ストーク
ス⽅程式の解の安定性に関する問題が解決されるなど、数学の歴史の転換点を迎
えているといえる。⼀⽅、記号計算においては、AI技術によるブレイクスルーは
未だ限定的であるが、注⽬すべき潮流はいくつか発⽣している。本発表では、そ
のような潮流について、発表者の知る限りの範囲で情報共有を⾏う。

10:50‒11:30

講演者：計良宥志（千葉⼤学/国⽴情報学研究所）
講演タイトル：CALT ライブラリを⽤いた算術・記号計算の深層学習チュートリ
アル
アブストラクト：近年、Transformer をはじめとする深層学習を⽤いて、算術や
記号計算そのものを学習する研究が広がっている。⼀⽅で、実際にこうした実験
を始めるには、データ⽣成、表現⽅法、モデル学習、評価など、機械学習に関す
るさまざまな準備が必要となる。本チュートリアルでは、算術・記号計算の学習
実験のためのライブラリCALT（Computer Algebra with Transformers）を⽤い、
実際にPC上で問題データを⽣成し、Transformer を学習させ、その性能を評価
するところまでを⼀通り体験する。これを通して、機械学習の専⾨家でなくても、
個⼈で算術・記号計算の学習実験を始められるための⼊り⼝を提供する。

11:30‒13:00

記念撮影・昼休憩

13:00‒14:00

講演者：園⽥翔（理化学研究所）
講演タイトル：定理証明AIの統計的な証明可能性
アブストラクト：定理証明⽀援系 Lean と⽣成AIを組み合わせて数学定理を⾃
動証明する技術が急速に発達している．伝統的な計算複雑性理論によれば，定理
証明は難しい問題であるにも関わらず，今⽇のAIは未解決問題すら形式証明でき
る．伝統理論と現実のギャップを理解するため，講演者らは，証明探索をMDP
としてモデル化し，AI定理証明器の証明成功確率（統計的証明可能性）を理論的
に評価した．本講演では，AI定理証明の近況と統計的証明可能性の理論について
説明する．

14:15‒15:15

講演者：瀬川秀⼀（三菱電機株式会社）
講演タイトル：数学の蓄積を⼯学設計の保証につなぐ ― Lean によるシステム検
証と産業応⽤への展望 ―
アブストラクト：数学や記号計算が培ってきた理論やアルゴリズムを、より多様
な利⽤者や設計課題へ届けるには何が必要だろうか。本講演では、定理証明⽀援
系Lean の概要と、LLMによる数学研究⽀援の動向を紹介する。続いて、スイッ
チドシステムの⼀例である降圧コンバータを取り上げ、LLMが提案する電流上界
の成⽴をLean で検証する取り組みを解説する。AI数学の進展を、既存の理論や
⼿法の活⽤機会を広げる契機として捉え、産業応⽤の可能性と課題を議論する。

15:30‒16:30

講演者：鎌⽥⽃南（北陸先端科学技術⼤学院⼤学）
講演タイトル：デュードニーパズルの最適性証明とその応⽤
アブストラクト：1907年、H. E. Dudeney は「正三⾓形をできるだけ少ないピー
スに切り分け、それらを組み合わせて正⽅形を作れ」というパズルを提⽰した。4
週間後、デューデニーは美しい4ピースの解法を⽰し、これは今⽇に⾄るまで最
も有名な裁合せパズルのひとつである。本発表では、このパズルの最終な解決、
すなわち、正三⾓形と正⽅形は、3ピース以下の裁合せを持たないことの証明に
ついて、紹介する。またこれらの技法を応⽤したその他の研究成果について紹介
する。本講演の内容の⼀部は 17th Innovations in Theoretical Computer Science
Conference (ITCS 2026)で発表された Erik D. Demaine ⽒、上原隆平⽒と発表者
の共同研究に基づいたものである。

16:30‒16:35

閉会挨拶

11 ⽉20 ⽇（金）非公開

申込方法

事前申込制（組織委員，講演者のかたも登録が必要です）
参加無料
定員になり次第，参加登録を締め切らせていただく場合がございます.

＼下記URLより参加登録をお願いいたします／

Zoom（オンライン）からご参加の方

Zoomを使ったオンライン開催，ハイブリッド開催の場合

参加登録後に件名［九大IMIより］Zoom用URLのお知らせというメールがimikyoten@gmail.comから自動配信されます．
届いていない方は，お手数をおかけしますがもう一度ご登録いただくか下記にメールにてご連絡をお願い申し上げます．
（迷惑メールフォルダもご確認お願いいたします）

＜九州大学マス・フォア・インダストリ研究所 共同利用・共同研究拠点事務室＞
imikyoten(at)jimu.kyushu-u.ac.jp
(at)を@に変更してください

Zoomについて

開催日までにZoomアプリをインストールしてください．
Zoomアプリは無料版で問題なくご視聴いただけます．

ミーティング用Zoomクライアントのダウンロードは下記からお願いします．
すでにインストールされている方は最新版にアップデートをお願いいたします．
https://zoom.us/download#client_4meeting

パソコンやスマホへのインストール方法は下記をご参照ください．
https://zoom.nissho-ele.co.jp/blog/manual/zoom-install.html