私はこの秋にMITのCSのPhDコースに入学しまして、先日期末試験を終えて冬休みに突入しました。MITは(おそらくアメリカの大学院ならMITに限らないと思いますが)本当に日本人が少なく、興味がある人がいても情報を手に入れづらいと思いますので、受けた授業の感想でも書いてみようかなと思います。ただし、私が受けたのは次に示すように数学っぽいものだけだったので興味の違う人には参考にならないかもしれませんが……。
私が今学期受けた授業は、
- 18.404/6.840 Introduction to Theory of Computation
- 6.820 Foundation of Program Analysis
の二つです。二つだけというと少ないように聞こえるかもしれませんが、それぞれ週に2回、90分の授業が行われるので4コマ分です。さらに、こちらでは大学院の授業でも宿題などが多く課されるのが普通ですので、一般的な日本の大学院より授業は大変なんじゃないかなと思います。(もちろん、私も日本の大学院全般を知っているわけではないので同程度に授業がハードな日本の大学院もあるのかもしれません。)
計算論(計算可能性・複雑性)の基本です。学部・院併設の授業です。担当は Michael Sipser という先生で、自身の書いた教科書 Introduction to Theory Of Computation を使って教えていました。この本は日本語訳もあります：
計算理論の基礎 1.オートマトンと言語
計算理論の基礎 2.計算可能性の理論
計算理論の基礎 3.複雑さの理論
内容は普通の計算論で、前半はオートマトンやチューリングマシン、後半の計算複雑性は P, NP, (N)PSPACE, log space, hierarchy theorem, BPP, IP などをやりました。チューリングマシンや複雑性についてちゃんと勉強したことがなかった自分にも分かりやすい授業でした。そして、何より宿題が面白かったです。宿題はほとんどが証明問題で、考えさせる問題が多かったです。たとえば、一番最初の宿題の一番目は、
「ベクトル (x y z) (x, y, z ∈ {0, 1}) から成るアルファベットを考える。文字列 (x1 y1 z1)...(xn yn zn) について、x1...xn, y1...yn, z1...zn をそれぞれ二進数で表された数と見るとき、
x1...xn + y1...yn = z1...zn
が成立する文字列全体が正規言語であるとを示せ」
という問題で、その次が
「同様の設定で、
x1...xn * y1...yn = z1...zn
が成立する文字列全体は正規言語でないことを示せ」
という問題でした。どちらも証明するのは難しくはないのですが、「足し算と掛け算はどう違うのか？」という問いを示唆しています。その観点で、有限オートマトンには何ができて何ができないのかについてのイメージを以前よりはっきりさせることができました。
また、計算複雑性に入ってからの宿題だと、「P = NP ならば素因数分解が決定性チューリングマシンで多項式時間でできることを示せ」という問題がありました。一見単順に見えますが、これには注意書きがあって、「『素因数分解は NP だから』は証明にならない」とあります。P や NP というのは「言語」の集合です。「素因数分解がこの時間でできる」ということを示すには、そのようなアルゴリズムを与える必要があり、P と NP という二つの言語の集合が等しいという仮定はアルゴリズムを与えることには直接は繋がらないのです。私はこの問題を見て初めてその事実に気付きましたし、計算論をフォーマルに学んでいない多くの人が誤解しやすいポイントのように感じます。
また、手応えがあってかつ数学的に面白かったのが、「(a) 与えられた論理式が最小(より短い同値な論理式を持たない)であるかどうかを判定する問題は PSPACE であることを示せ。(b) P = NP ならば 上の問題は P であることを示せ。」というものです。(a) は難しくはないですが、(b) の問題文を見たときは驚きました。最初はなんで PSPACE から P まで落ちるのかさっぱり分からなかったのですが、すごく巧いからくりで実際にそうなることが示せます。
中間試験や期末試験は、時間の割に問題数が多く、問題を見たらすぐ解法が思い浮かぶくらいでないと厳しいです。試験問題でもほとんどが証明です。基本的に習ったすべてのトピックについて一つずつ問題が出ていて、どれもしっかり理解していないと短時間では解けません。
日本語訳すると「プログラム解析の基礎」で、内容はとにかく色々詰まっていました。何をやったかを言うには課された宿題のリストを並べるのが早いと思うので、並べてみます：
- Haskellで型なしラムダ計算のインタプリタを実装、さまざまな関数をチャーチエンコーディング
- HaskellでHM型推論を実装 & ラムダ計算に例外処理が付いたような言語について、そのbig-step semanticsとsmall-step semanticsが一致することをCoqで証明
- コールスタックの振舞いを簡単にモデルしてCoqで検証
- Hoare論理。配列を持つシンプルな手続き型言語について、そのコードをverification conditionを計算しながら与えられた事前/事後条件をみたすかどうかを検査するプログラムをOCamlで書く。SMTソルバはZ3を使う。
- OCamlでAbstract Interpretationを実装して、C言語風プログラムに対してメモリエラーが起きないかどうかを検査する。Abstractionのための束(lattice)の与え方を工夫して解析が詳細にできるようにすればするほど貰える点数が増える。
- Spinで平行プログラムの検証をしてみる & OCamlでCTL論理式に対するモデル検査器を実装。
(対応する宿題はありませんでしたが、Hoare論理の後にSeparation Logicも習いました。)
宿題が公開されてから締切まではそれぞれ2週間ありますが、公開された後でそれに必要な知識を授業で教わるので実質取り組める時間は1週間程度です。
この宿題リストを見るとこの授業は前提として関数型プログラミングの知識が仮定されてるかのように見えますが、そんなことはありません。それまで関数型プログラミングの経験がまったくなかった受講生もたくさんおり、HaskellやCoqは授業で教わります。ただし、それぞれ1回や2回きりです。(そして、課題の半分でOCamlが求められているものの、OCamlは授業中に習うことはありませんでした。)私は元からHaskellやCoqやOCamlの経験があったからよかったものの、そうでなかったなら相当きつかった気がします。たとえば日本のCoqの授業ならおそらく最初にリストのappendの結合律を示しましょうなどが定番だと思うんですが、そういうのはまったくありません。いきなり操作的意味論についての証明を求められます。かといってCoqを学ぶのがメインの授業ではなく、それらはただの序盤です。
個人的にはAbstract Interpretationやモデル検査は自分にとって完全に新しい内容だったので学ぶことは多く面白かったですが、その分宿題もハードでした。授業でやる内容は授業を聞けばすぐ理解できたのですが、宿題は基本的に授業の内容よりどこか捻ってあってその分は各自で考える必要があります。あと、OCamlと同じでZ3やSpinの使い方は授業中に習わなくて、自分で調べてねという方針でした。ちなみにこちらにはrecitationと呼ばれる、TAが行う補講のような授業もあり、正規の授業だけではついて行けない人はそちらに出て各種ツールの使い方を教わったり宿題の内容に関して少し詳しく聞いたりできます。オフィスアワーも通常よりたくさん開かれました。そんなこんなで受講者にとっても先生にとってもTAにとっても相当time-consumingな授業だったように思います。
授業の内容についてもう少し書こうかと思いましたが、長くなりそうですし専門的になるのでここでは省略することにします。気になる人がいたら聞いてください。
そんな風に、どちらもなかなか骨のある授業でしたが、驚いたのが、宿題や試験の点数の分布を見るとみんなかなり点数が良かったことです。点数の分布を見るまではなんとなく自分はうまくやっている方かなと思っていたのですが、別にそんなことはなく、普通でした。それまで特に実情をよく知らずに標語的に「MIT生はすごい」みたいなことを言うことはしなかったのですが(低く見積っていたわけでもないですし、同じ分野の人については知識や技術力が高い人がたくさんいるのも知っていました)、そこで初めて「あっみんな優秀なんだな」と思ったのでした。計算論の授業ではA+が取れましたが、たぶん課題の中のオプショナル問題(少し難しめで、ABCDの評価には影響しない問題。AがA+になるかどうかにだけ加味される。自分の研究に集中したい大学院生などはスキップする人がたぶん多い)ですべて満点を取ったからかもしれません。Program Analysisの成績はまだ出ていません。ともかく、内容は面白かったと同時に、課題の多さにうんざりしかけたり、周りのガリ勉さを知ることができた1学期間でした。