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

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

注意

本記事は微分可能プログラミングに関する記事ではありません。微分可能プログラミングのソフトウェアに関する解説をほとんど含まず、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

すなわち、頂点が $v$ 1-5 の5 つあって、それぞれの頂点に対応する中間変数 $w$ 1-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 文や再帰関数の微分は困ってしまうので、これを頑張って回避します。

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

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

なんで 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."で発表されました。

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

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

おわり

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

注意

挨拶

導入