ML勉強会#2 と ProofSummit2017 に参加した

ProofSummit2017ML勉強会#2に参加してきました。
とりあえず二日連続はつらいものがあった。

個々の感想

  • SML#の話は良かった。言語や処理系の機能が列挙されていると個人的に楽しい。そういう意味ではATSも楽しいんだけど、機能(のアップデート)が少なかったし、楽しさの半分は岡部さん自身が面白いことに由来している気もする。
  • OCamlのjupyterの話。blasのラッパーしか無さそうならSMLで実装もアリかなと思っていたけど、意外と環境が整っていそうなのでOCaml+Jupyterを試してみようという気になった。
  • autorewriteの話のストーリーが良かった。既存の部品を使って問題がうまく解決されている(と思う)。
  • tanakaさんのCoqの話は楽しいような気がした。でもtrusted baseが小さいという主張はなんかだまされた感がある。(C側の実装をVeriFastで検証しませう?)
  • パワーの溢れる若者が機械学習で自動証明の話をしていた。まだちょっと無理がある印象。証明戦略の選択をする話とかはまずSMTソルバとかでやってみてうまくいくことを確認してからでもいいんじゃないかという気がした。まぁ研究は野心的なことをやるべきなのかも知れないけど。そういえば発表中に出て来たものはほとんど対象がHOLだったし、自動化し易いのかな。

全体の感想

  • 発表にはストーリーがある(かつ明確な)方が良い。どこが主張で、今どの辺について喋ってるのか分からないとつらい。どの辺が重要なのか判定不能なので一瞬でも聞き逃すとリカバリ不能になる(というかする気がなくなる_(:3」∠)_。例えばコード生成について話してるけど、それ以降で高階型推論についての考察が始まるのか、シンタックスについてのコダワリが語られるのか、生成系の証明が始まるのかで注視するとこが違ってくる。聞きながらググるべき事の選定にも効いてくる(かも知れない)。
  • 特にそれが有名で無い場合は、紹介or提案or実装している言語or処理系or論理体系の大雑把な能力の説明があった方が良い。命題論理か述語論理か、一階か高階か、コンパイラインタプリタか、型推論は完全性を持つのかなどなど。
  • あと発表と無関係だけどJavaScriptへの殺意が高まった