微分可能プログラミング言語の意味論

これは ISer adventcalendar の 24 日目の記事です。昨日はOtaさんの人工知能は人間より強くなれるか。でした。

adventar.org

qiita.com

注意

本記事は微分可能プログラミングに関する記事ではありません。微分可能プログラミングのソフトウェアに関する解説をほとんど含まず、PyTorch や TensorFlow には触れません。これは自動微分が組み込まれた domain specific language の意味論に関する記事です。

ISer の 3A の科目『言語モデル論』で学習するプログラム意味論の知識があることが望ましいです。意味論になじみがなくても極力読めるようにがんばります。

挨拶

19er の人です。2020年もあとわずかですね。僕は4回生なので最近はずっと卒論を書いていないといけないのですが、大筋の部分を書いたところで読み返したところ、「この論文つまんねぇなぁ～」と思って書く気力を失いました。さっき LaTeX のコミットの履歴を見たら最終更新が10日前でした()

他の19erのみなさん、お元気でしょうか。卒論一緒に頑張りましょうね。20er は今年は本当に大変だったと思います。お疲れ様です。卒論も本当は 19er が苦しんでいるところを見て諸々の雰囲気とかをつかんでおいたほうが良いのでしょうが、このご時世だと難しいですね。演習3の様子を何も知らないのも割と致命的だと思うのですが大丈夫なんでしょうか...... 21er はまあ、いまのところ例年と変わらないとおもいますが、来年は地下に行ける状況になってるといいですね。先輩はアドベントカレンダー見てないでしょ、アハハ。ISer ではない方、初めまして (?) 

はい。

導入

この記事では微分可能プログラミング言語の簡単なモデルとなるような言語に対して、操作的意味論・表示的意味論 (\mathbb{R}に依存する意味論)・表示的意味論 (category theoretic) の研究のざっくりした紹介をします。

微分可能プログラミング言語とは

まず記事のタイトルの微分可能プログラミング言語についてですが、あんまりよく知りません。詳しくは下の記事を見てください。なお、以下の僕の記事を読むうえで必要ではありません。

qiita.com

bonotake.hatenablog.com

僕の甘い理解では

  • 機械学習などでは float -> float などの型をもつプログラム p を関数 f : \mathbb{R}\rightarrow\mathbb{R} とみなしたときにその微分 \frac{\mathrm{d}f}{\mathrm{d}x} が計算したくなることがある。
  • 我々が普段書くプログラムは exp や sin などの合成関数などが主であり、プリミティブの微分があれば合成関数の微分則を使って言語プリミティブとして関数の微分を計算する機構が作れる。

みたいな感じです。後者の微分の機構のことを自動微分と呼んで、自動微分が言語に含まれているようなプログラミング言語を微分可能プログラミング言語と呼んでいます。実用的には PyTorch や TensorFlow などがあるようです。

↓これが非常にいいサーベイ論文でした。

Baydin, Atılım Günes, et al. "Automatic differentiation in machine learning: a survey." The Journal of Machine Learning Research 18.1 (2017): 5595-5637.

 

forward mode differentiation と reverse mode differentiation について

自動微分 - Wikipedia や先ほど紹介したサーベイ論文を見てもらうとわかりますが、自動微分には二種類のアルゴリズムがあって、それぞれフォーワードモードとリバースモードの微分とよばれています。

そもそも自動微分はどうやって行うかというと、まず、微分したい関数を計算グラフ (構文木みたいなもの) とよばれるグラフに分解します。例えば、 z = xy + \sin x は次のようなグラフにします。

f:id:run_run_OJI:20201223005902p:plain

すなわち、頂点が v1-5 の5 つあって、それぞれの頂点に対応する中間変数 w1-5 を導入して、一番上の w5 を x と y だけで表現すると元の関数になるようにしておきます。目標はこの一番上にある v5 を x と y の関数だと思った時の x による偏微分を求めることとします。

\frac{\partial}{\partial x}(xy + \sin x)を求めるときにおそらく普段ヒトがする直感的な計算方法が、forward mode derivative に近い方法です。つまり、各中間変数の x による微分を再帰的な計算で求めていきます。これはよく考えると、先ほどの計算グラフの各頂点 vi に \frac{\partial wi}{\partial x} の値を書き込んでいく操作にあたります。実際、連鎖率を使うと簡単に \frac{\partial wi}{\partial x} はこのグラフの下の値を使って上の値を計算できるので、これでうまくいきます。

f:id:run_run_OJI:20201223005907p:plain

これに対して、reverse mode derivative は、各頂点 vi に \frac{\partial z}{\partial wi} を書き込んでいくことで計算をします。ここでは、一番上の階層では z は w5 の関数だと思い、中間の階層では w3, w4 の関数だと思い、一番下では w1, w2 の関数だと思っています。そうすると、たとえば v1 に書き込む値を考えたいときは z は中間の階層で w3, w4 の関数だと思った時の偏微分を計算してあるので、連鎖律多変数関数ver をつかって \frac{\partial z}{\partial w1} = \frac{\partial z}{\partial w3}\frac{\partial w3}{\partial w1} + \frac{\partial z}{\partial w4}\frac{\partial w4}{\partial w1}=\frac{\partial z}{\partial w3}w1 + \frac{\partial z}{\partial w4}\cos w1 と計算できるので、今度は上から下に向かって順に値を求めることができます。

f:id:run_run_OJI:20201223005917p:plain

この reverse mode はちょっとかんがえると、 x での偏微分を計算したかったのに、y での偏微分も同時に求められていることが分かります。それゆえ、入力の数が増えても計算量が変わらない点で強力です。

以下で紹介する意味論はこの reverse mode に即した意味論になっています。(本当は reverse mode にしたことによる影響などについても書きたかったのですが、既に内容が難しくなってしまったので諸々を諦め、その結果普通に微分の話をしていると思ってもそんなに差し支えない内容になっていると思います。)

プログラム意味論について

そもそもプログラム意味論ってなんやねんという話を知らない人向けに書いておこうと思います。

我々はプログラムを書くとき、for n in range(3): などと書くと、"3回次の命令を繰り返す" と思っているわけですが、for n in range(3): というのは実際のところ単なる文字列でしかありません。その単なる文字列から、あなたの目の前にあるコンピュータは処理系を介して何らかの "意味" を読み取り、CPU という質量をもった物理的な機械が計算をして結果をディスプレイに表示してくれるのです。すごいですね。

この "意味" というものがなんなのかを明らかにするのがプログラム意味論です。3A のコンパイラ実験では実際にコンパイラをつくるわけですが、意図した挙動をするアセンブリを生成するというのは、プログラムの意味を壊さないように翻訳するということにほかなりません。

3A で習うプログラム意味論は簡単な言語に関する操作的意味論や表示的意味論、公理的意味論ですが、もっと複雑な言語にもありますし、意味論の種類もこの限りではありません。意味論の学習については文献がいくつかあって、高橋計算論、横内プログラム意味論などが有名ですが、今年の夏に小林先生がプログラム意味論の基礎という本をお出しになったりしています。恥ずかしながらどれも読んだことがないのですが、気になった人は読むとよいと思います。プログラム意味論の研究がどうして大事かということについては蓮尾先生の記事などがよくまとまっています。要するにプログラムの挙動をちゃんと研究して書き下す手段を得ることで、処理系の構成、言語そのものの構成、プログラムが正しいことの検証、アルゴリズムの抽象化や正当化などができるようになるということです。

1. 微分可能プログラミング言語の体系と操作的意味論

操作的意味論というのは基本的に処理系に期待する動作を記述する意味論です。これからまず簡単なプログラミング言語を作って、先ほど紹介したような reverse mode の計算アルゴリズムに関する操作的意味論を作るのですが、if 文やループなどを言語にとりいれるのでそこに非自明パートがあります。この節と次の節は次の論文を元に構成しています。というかこの論文の要点を抜き出したものになっています。

Abadi, Martín, and Gordon D. Plotkin. "A simple differentiable programming language.” Proceedings of the ACM on Programming Languages 4.POPL (2019): 1-28.

考えるプログラミング言語

まず型として、

  • real
  • unit
  • T \times U (T と U も型) 

を採用します。項 (=プログラム) としては、次のようなものを考えます。(M,N,L はメタ変数です。)

  • 変数 x
  • 実数 r (たとえば 3.141599)
  • プリミティブ関数
  • let x = M in N
  • () (unit 型をもつ唯一のプログラム)
  • (M,N) (タプル)
  • fst, snd (タプルから第一、第二要素を取り出すプリミティブ関数)
  • if B then M else N
  • letrec f x = M in N
  • f (M) (f は letrec で定義される関数)
  • M.rd(L)(\x -> N) (NとM、Lとx は同じ型を持っていないといけない。)

最後の項が意味不明ですが、これは N が x を変数として持つ関数だと思った時に、その点 L におけるヤコビ行列を転置した行列に右から M をかけるたもの、という意味だと思ってください。意味不明ですか？私もです。ですが、まあこれが実際に reverse mode の微分を計算するときにする計算を表しているようです。より詳しくは論文を読んでください......

操作的意味論

基本的には普通のMLの評価順序と同じ順序で評価されるように定義します。微分だけ困ります。特に if 文や再帰関数の微分は困ってしまうので、これを頑張って回避します。

内容はかなりテクニカルなので難しいのですが、要点をまとめると以下のようになると思います。

  1. 基本的にMLの評価順序で評価を進めて、微分の評価の前に上でいう M と L (行列にかけるベクトルとヤコビ行列を計算する点に対応するプログラム) の評価は済ませておきます。
  2. 微分を計算する番になると、微分する関数を整えるフェーズに入ります。すなわち if 文のbool値や関数定義の letrec を先に (特殊な方法で) 評価してしまって消します。
  3. 整えて簡単な式になった関数は微分できる形なので、これを普通に微分します。

なんで 2 の変なフェーズがあるのかというといろいろ雑にやると困る点があるからです。例えば if x > 0 then 0 else x みたいなものを微分しようとすると、x > 0 を先に評価しなきゃいけないのですが、x に 値を単純に代入してしまえば例えば if 3 > 0 then 0 else 3 みたいな定数のプログラムになってしまいます。しかし欲しいのは if 3 > 0 then 0 else x なので、どこに値を代入するかについてセンシティブにならないといけないという事情があるのです。詳しくは論文を読んでください (2回目)。

2. (\mathbb{R}を使った) 表示的意味論

表示的意味論というのはプログラムを入力に対して出力を返す (数学的な) 関数だと解釈する意味論です。

この微分を考えている今の場合は普通にプログラムを入力に対して出力を返す関数 \mathbb{R}^n \rightarrow \mathbb{R}^m をプログラムの意味だと考えたくなります。しかしこれはうまくいきません、というのもさっき意味論で変なことをしたのです。

そもそも、我々は if x < 0 then 0 else 1 という明らかに原点で微分可能どころか連続ですらない関数を定義できて、これを微分できるような体系を作っていることにお気づきだったでしょうか。さらには変数 x に対して if x = 0 then 0 else x というプログラムは x そのまま返す恒等写像を表しているはずですが、これの微分を (さっき操作的意味論をかなり適当にやったのでそんなん知らんわと言われるかもしれませんが)、if x = 0 then 0 else 1 という関数で定めてしまいました。これは明らかに恒等写像の微分とは異なります。

(なんでそんな酷いことをするの？うるうると思いますがこれはおそらく実用されている微分可能プログラミング言語と仕様を合わせたためです。)

またさらに、再帰関数が作れるので評価が止まらず undefined になりうることも考えると単純にはいかないことがわかります。これに関しては再帰関数を含む表示的意味論には領域理論という理論があって、特殊な順序集合dcpo in nLabを使うとうまくできることが知られています。この論文もこの領域理論に基づいて意味論を構成しています。(再帰関数とは最小不動点だ！みたいなのをどこかで聞いたことがあるかもしれませんが、そういうことです(????)) 

こういう問題点を踏まえたうえでどういう意味論を作るかというと、当然微分を考えるのですからベースとしてはユークリッド空間の (無限回) 微分可能な関数を使いたいのですが、これをうまく拡張して if文や undefined を解釈できるようにした上で、dccpo という構造 (これは再帰関数の解釈をしたいときにこの構造があればうまくいくことが知られているような領域理論に基づいた構造) があるようなものを作ればよいということになります。

実はこれは、 f : \mathbb{R}^m\rightharpoonup\mathbb{R}^n なる部分関数であって \mathbb{R}^m の開集合で定義されていて定義されている範囲で無限回微分可能な関数たちをとってくるとみたせます。なのでこれを使って意味論を作ることができます。(このあたりちゃんと読めていないのでこれで if 文の解釈ができることに僕は直感が追い付いていないのですが、できるそうです。)

意味論の具体的な構成などは割愛します。残りの部分は割とつまらない+僕が疲れたので。 

3. (圏論的な) 表示的意味論

 これも 2 に引き続き表示的意味論ですが、今度はプログラムを数学的な関数だと解釈するのではなく、圏論における射と解釈するような意味論になります。圏論的意味論で有名なのは型付きラムダ計算をデカルト閉圏で解釈する意味論ですが、様々な体系に対して様々な圏論的意味論が既に研究されています。RIMSの長谷川先生のこのpdfの図1がたまに引用されていたりします (ほんまか？) いまのところ圏論的意味論に日本語の良い文献はおそらくないので勉強しようとすると洋書になりますが、R.L. Crole, Categories for Types. Cambridge University Press, 1993. や B. Jacobs, Categorical Logic and Type Theory. がよいです。前者は圏論知らなくても頑張れば読めて、後者は無理です。圏論の入門書は Awodey, Steve. Category theory. Oxford university press, 2010. と壱大整域を勧めます。数学徒以外にはベーシック圏論と圏論入門は非推奨です。圏論勉強会 @ ワークスアプリケーションズは後世に残すべき名スライドです。

 圏論の紹介はさておき、まず圏論における微分を考えないといけません。ユークリッド空間における微分というのは、ヤコビ行列のことだったのでヤコビ行列を線形写像だと思うと、f:\mathbb{R}^m\rightarrow\mathbb{R}^n の微分は \mathrm{d}f : \mathbb{R}^m\times\mathbb{R}^m\rightarrow\mathbb{R}^n なる関数であって、\mathrm{d}f(x,y) = (Jf_{x}) y (点xにおけるヤコビ行列にベクトルyをかけるもの) と考えられます。これの一般化として、Cartesian differential category (CDC)というものがあります。CDCでは、射f: A\rightarrow B に対して Df: A\times A \rightarrow B なる射を定めることで微分を考えます。具体的にはCDCは左加法圏であって f に対し Df が定まっており、いい感じの線形性や連鎖律、二階偏微分の順序の交換などの公理を課したものです。気になる人は検索してください。

CDC は圏論的な微分の一般化と言われているのですが、reverse mode の微分はヤコビアンの転置を考えるため、f の微分は \mathrm{d}^rf : \mathbb{R}^m\times\mathbb{R}^n\rightarrow\mathbb{R}^m になってしまい、これはCDC の枠組みではとらえられません。これに対して去年、Cartesian reverse differential category (CRDC) というものが考えられました。ここにおける微分は D^rf: A \times B \rightarrow A という形になっており、ちょうど reverse mode の微分になるような枠組みとなっています。そして今年、待望の圏論的一般化が Cruttwell, Geoffrey, Jonathan Gallagher, and Dorette Pronk. "Categorical semantics of a simple differential programming language."で発表されました。

圏論的意味論ができると何を期待するかというと、広く抽象化することでより良いアルゴリズムが見えやすくなる、ということです(ほんまか？)。実際この論文の最後にすこし操作的意味論の改善できることが分かった、という内容があります。

おそらく今後はよりリッチな型 (配列とかリストとか) をもつような言語へ拡張することを考えたりするのではないでしょうか、しらんけど。

おわり

はい、この記事では微分可能プログラミング言語の意味論の最近の研究の論文をざっくり紹介しました。明日はアドベントカレンダー最後だそうです。完走間近ですね、すごい！それでは皆様よい意味論ライフを。

グラフ理論の一問に数十時間溶かした話

理学部情報科学科の3Sの演習授業に離散数学演習というものがあります.

離散数学演習は, 二週間に問題が13問程度出され, 学期を通して一人一回以上の発表と, 解いた問題(何問でも可)の解答の提出が課せられる授業です.

最後の方はグラフアルゴリズムの問題(特にマトロイドの問題)が増えますが, おおよそほとんどグラフ理論の問題と思って構いません. (但し, 離散数学の授業はグラフ理論よりグラフアルゴリズムよりなので, 離散数学演習ができても離散数学のテストは解けません.)

問題には難易度A,B,Cがあり, A は全員提出必須の比較的難しくない問題, B はそこそこ難しい問題からかなり厄介な問題まで揃っており, C は学期を通して一問だけ出される超難問(?)になっています.

偶然(?)僕は3S前の春休みに Graph Theory (Diestel) を8章まで読んでいたのもあって, 離散数学演習の問題は全解きチャレンジをしていたのですが, C 問題がどうしても解けなくて, 10日くらい他の課題を全てすっぽかして何十時間か溶かしましたが, 遂には解けませんでした.

その問題をここで公開すると20erに見られてしまってアレなので, 公開はしないのですが, その代わりに関連する定理を一つここで紹介して, 証明を記し, グラフ理論のノリを知っていただければいいなと思います. この記事の最後にグラフ理論の紹介をちょっとします. ("グラフ理論" はかなり分野として広くて, かなり多種多様な話題があります.)

 

定理の紹介

 

定理

ただ 1 通りに 3 枝彩色可能*1な 3 正則*2グラフ*3はハミルトニアン*4である.

(ただ一通りとは, 色の入れ替えを除いて, の意.)

 

証明

ただ一通りに3 枝彩色3 正則なグラフ G = (V, E) *5が {1, 2, 3} の 3 色で枝彩色されているものとする.

                            c(e) = 1      ~~~      (e\in E)

と書くことで, e が 1 で塗られていることを表すことにする. (枝彩色を関数 c として表現しただけ)

いま,

                             C = c^{-1}(2) \cup c^{-1} (3)

とすると, C が G のハミルトン閉路を定めることを示す.

まず, C がいくつかの交わらない閉路からなる*6ことを示す. そのためには, 各頂点に対し, C に含まれる辺がちょうど 2 つ接続されていることを言えば十分である*7. これは各頂点にちょうど 3 辺が接続されていて(3正則の条件), 各頂点の周りに最大で 3 色しか塗られていないから(3枝彩色), 各頂点の周りには 1, 2, 3 が塗られた辺がただ一つずつ存在することになり, C にはそのうちちょうど 2 つ, 色2 と 色3 が塗られた辺が含まれるから従う.

次に, C が連結*8であることを背理法で示す. もしも連結でないなら, ある 2 頂点 [\tex: u, v \in G] があって, u から v へは道がない. このとき, C の辺で, u から歩き始めて到達できる範囲にあるものの集合を S とする. 次の関数 c' を定義する.

c'(e) = \left\{\begin{matrix}c(e)~~~~~~~~~~~~~~~~~(e\notin S)\\2~~(e\in S, c(e)=3)\\3~~(e\in S, c(e)=2)\\\end{matrix}\right.

この関数が 3 枝彩色を定めることを示せば, G の仮定(Gは"一意に" 3 枝彩色可能)に反するので, C が連結であることが従う.  これも下にある図を見てもらえればほとんど明らかなので, 厳密に証明はしないことにする.

下が下のグラフG.

f:id:run_run_OJI:20191210171722p:plain

この G の緑, 赤の辺を取り出したものを C (左下の図)として, 色を入れ替えたものが右下の図である.

f:id:run_run_OJI:20191210171711p:plain=>f:id:run_run_OJI:20191210171704p:plain

 

 これで, C はただ一つの閉路からなり, G の各頂点は C の 2 つの辺に接続されていることがわかったが, このような C はハミルトン閉路に他ならない.

 

グラフ理論のノリ

グラフ理論は通常の(?)代数学*9 とは かなり様相が異なります.

冒頭で僕が呼んだと紹介した本 *10は学内 springer から落とせる(+駒場図書館, 経済学部図書館で借りられる) ので, 興味があれば開いてみて欲しいのですが, 本当に慣れるまでは読みにくくて仕方がありません. (慣れるとすごくいい本に思えてきます(?))

まず, 基本的に有限集合しか扱いません. そして演算がありません. しかし, かなり難しいです.

なんとなく雰囲気で説明すると, グラフ理論においては, よく次のような言い回し(証明の流れ)がされます.

"ある性質 P を満たす頂点 x が存在するならばその x を hoge すると証明ができる. もしそのような x が存在しないならば, 全ての頂点は P を満たさない. このとき , 性質 Q を満たす頂点 x が存在するので矛盾する. もし Q を満たす x が存在しないならば ... (以下繰り返し)"

この流れは気持ち悪いと言えば気持ち悪いのですが, この証明の順番はプログラミングの末尾呼び出し的になっていて, この順番にしないと"呼び出し"のネストが深くなりすぎて混乱してしまうので仕方がないのです.

グラフ理論の証明は 五色定理の証明を一度読んでみるとわかると思うのですが, 有限集合の元を一つずつ手で動かすような操作が非常に多く, さらに場合分けが大量に出てきます. (五色定理は場合分けがかなり少ない方.) 場合分けが多いと上のような変な証明法にしないと途中で混乱してしまうのです. そしてその場合分けがかなり尽くせているかどうかの判断が難しかったりします.

グラフ理論の分野

グラフの定義というものは非常にシンプル(脚注3)で, それゆえ(?), グラフ理論と言ってもかなり広い分野があります. また, グラフ理論はかなり新しい理論なので, 未だに未解決な問題がたくさんあります.

  • 組み合わせ(マッチング等々)
  • 平面グラフ
  • 彩色問題
  • フロー
  • 無限グラフ
  • ランダムグラフ
  • グラフマイナー
  • 代数的グラフ理論

説明しだすと大変なので割愛します. 数学に興味ある人はこの Springer の本がかなり頭おかしくて*11面白いのでペラペラめくってみるとテンション上がると思います.

link.springer.com

 

最後に

この記事は

adventar.org

の3日目のものとして書かれました. 遅くなって誠に申し訳ありません...

 

 

*1:各辺に対して三色のうち一色が与えられており, 各頂点に対して, その頂点に同じ色が塗られた辺が二つとして接続されていないような彩色を3彩色という. そのような彩色が存在することを3彩色可能という.

*2:各頂点に対し, その頂点に接続(その頂点を一端にもつこと)された辺がちょうど 3 つあるようなグラフ.

*3:頂点の集合Vと辺の集合 E があり, E の要素 e はVの 2 元集合になっているもの. e = {u, v} のとき, e は頂点 u, v の間にかかる辺と解釈する. 多重辺や, ループ辺は定義からない.

*4:ある頂点から出発して, 同じ頂点を二度と通ることなく, 全ての頂点を一回ずつ通って最初の頂点に帰ってくるような道が存在すること

*5:V は頂点集合, E は辺の集合

*6:閉路は同じ頂点を二度通ることなく最初の頂点に戻ってくるような道. ここでは, C はいくつかの閉路の辺集合の非交和(disjoint union)からなることをいう.

*7:このとき, 行き止まりがない一本道になっていることになるから, これは閉路に他ならない

*8:任意の2頂点間を辺の上を通って移動できること

*9:群, 環, 体, 圏

*10:ちなみにこの本は第5版なのですが, 第1版では未解決問題とされていた予想が定理に変わっていたりしてアツい. 日本語版もありますが, これは古い.

*11:多様体とグラフ理論結びつけようとする人が正常であるはずがない. かなり難しい本なので読めないのですが, ペラペラめくるとこの人何考えてんだ!? とはなる.