第9回：2026 年 10 月 19 日 | 諏訪 敬之 | Compile-time tensor shape checking via staged shape-dependent types
- 日時：2026 年 10 月 19 日（月）17:00 開始（16:30 開場）
- 場所：国立情報学研究所(NII) 1902,1903 会議室
- 講演者：諏訪 敬之
- 所属：京都大学
- 講演タイトル：Compile-time tensor shape checking via staged shape-dependent types
概要： DNN などをはじめとするテンソル（＝多次元配列）を扱うプログラムでは，テンソルを操作する演算に関して形状が整合していることを実行よりも前に保証できることが望ましい（ここでいうところの形状の整合性とは，「プログラム中で行列積をとる 2 つの行列 A と B に対し，A の列数と B の行数は等しい」といった制約を逸脱する振舞いをプログラムが起こさないことを指す）．こうした保証がなければ，重い計算を終えた後に形状不整合の実行時エラーが生じ，多大な時間が無駄になってしまうおそれが払拭できない．
テンソル形状に関する静的検証は古典的なトピックだが，理論的に成熟した種々の提案にもかかわらず，DNN プログラムを書く人がよく使うという程度にテンソル形状検査が定着している様子は今のところ見受けがたい．これについて，講演者は既存の多くの手法では手動ないし自動の証明を要することが実践適用への主要な障壁になってきたのではないかと考えている．これの解消を企図し，2段階の staged computation に基づくコンパイル時計算でアサーションを行なうことにより形状の不整合が起きないことを手動・自動にかかわらず定理証明なしで保証できる手法を提案する．（前述の障壁は今後 LLM に基づくコーディングエージェントの存在により大きく緩和できる可能性があるが，所要時間やエネルギー消費などの観点から依然として軽量な検査手法が実現できることが望ましい．）
この手法は「多くの場合，プログラム中の各テンソルの寸法の記述は型検査時に抽出でき，コンパイル時に具体的な値で instantiate することで整合性を確かめられる」という仮定に基づいるため，扱えるプログラムに一定の制約を課すが，DNN を実装したプログラムについてはそれほど厳しい制約にはならないことを実装により確かめている．具体的には，ocaml-torch のリポジトリで提供される数十〜数百行程度のプログラム例のうち 10 個を提案言語に移植し，検査できることを確認している．（残る十数個のプログラム例の移植は未完了だが，少なくとも明らかにカバーできない箇所は見つかっていない．）
このほか，コア言語のみでは註釈的な記述を多く要するため，暗黙引数 (implicit parameter/argument) の導入や，ステージに関する記述を省略しても適切に再構築できる仕組みを表層言語として提案する．これにより，ユーザが書くソース言語は，構文的に Idris のような依存型つき言語とそれほど大差のないものにすることができる．
なお，提案する体系は操作的にはそれほど込み入ったものではないが，left-linear でない簡約規則を必要とすること，refinement type を含む体系であることなどにより，正当性の証明には精緻な議論を要する．講演では，時間が許せばこれらについても簡単に紹介する.