suzumiyaの日記

何となく作った

情報科学若手の会参加のすゝめ

この記事は eeic (東京大学工学部電気電子・電子情報工学科) Advent Calendar 2018 その2の1日目の記事として書かれたものです。

(空いてたのでねじ込みました)

この記事は何ですか?

2018年10月6日から10月8日にかけて軽井沢で情報科学若手の会という集まりに参加してイケイケな3日間を過ごせたので、報告を致します。

一応慣例として、参加者は合宿から帰ってきたらブログを書くまでが若手の会やぞ!という事になっているので、私以外にも色々な人が今年の感想を合宿直後に書いてます。私は今まで書かずに何をしていたのかというと、合宿直後に帰省だの卒業研究だので少し書くべきタイミングを逃してしまい、ダラダラ引きずっていました。

その断罪?として、今回は所属学科であるeeicの人向けに、eeicとして若手の会は一度行って見ると楽しいぞ!的な宣伝をして、いい感じに来年以降後輩とかに来てもらえるようにするという方向性で書いてみたいと思います。(つまり横着してeeic advent calendarと報告ブログの両方を兼ねる記事を書いてややこしくなっているという事)

前回の記事で自己紹介をし忘れたので自己紹介します.

  • eeic2017(電子情報工学科)で卒論生です
  • 画像認識っぽい事を研究してます
  • それ以外の情報科学っぽい背景は特にないです

TL;DR

  • 情報系学科の人間として行ってみて損はないぞ
  • 特に卒論やってるB4の時期に参加すると捗るかもしれないぞ
  • こういうエンジニアの集会っぽいのとか参加した事ない…みたいな人の最初の一歩として良いかもしれないぞ

情報科学若手の会とは?

学科の人向けに書くので一応詳し目に書いておくと

  • 情報処理学会の下部組織?が運営している、年1回開かれる合宿で、情報系学生・社会人・研究者の交流の場です
  • 由緒正しいので今年で51回目とからしいよ
  • とにかく色んな分野の人が、自分の分野の面白い話を発表します。交流イベントも少しあります
  • 参加者は発表に参加した方が楽しいですが、聞き専も出来ます。今年は5分くらいの発表なら飛び入り参加枠もあったりしました
  • 多分学科の人が参加及び発表するとしたら次の3種類の形態のいずれか

    • 一般発表: 発表30分+質疑10分 (参加申し込み時に登録)

    • ショート発表: 発表15分+質疑10分(参加申し込み時に登録)

    • ライトニングトーク: 5分で出来るだけ情報を詰め込んで終わらせろ!的なやつ。私は最初は聞き専でしたが、1日目夜に飛び入り参加を決めて、2日目夜に発表しました

  • 8月末〜9月初旬に参加締め切りと振り込みがあって参加費はB4なら今年は14,000円。開催は毎年9月末~10月初旬。学生は交通費補助を受けられる可能性が高いらしいです

何を発表したの?

  • 卒論研究テーマの概観みたいな話をしました。やってる研究の具体的で未発表な部分は当然話せないので、中間発表で言うところの背景みたいなお話をしたらちょうど5分くらいになりました。

感想色々

  • 初参加だったし、集合場所に着くと、割と常連っぽい参加者とか、既にTwitter上で交流し合ってそうな人々がいたので少し怖かった。でも1日目で数人と知り合えたので良かった。1つの部屋につき4人くらいで泊まるのでそこで色々話せる。後夕食の場でも知り合える。夕食の時にライトニングトークの勧誘をされ、結構気軽な雰囲気で発表出来そうだったので飛び入った。
  • アプリ開発・非同期処理の話・ネットワークの話…本当に多様な話を聞けて面白かった。個人的に興味がある、セキュリティ関連・深層学習関連の発表が多かったのは嬉しかった。コンテナデータセンター(物理)の講演は伝説と化していた。
  • 発表の実況・感想がSlackのチャンネルで流れる。各分野のナウい情報を持ってる人のレスポンスは非常に為になる。
  • 私の発表後に、様々な人が卒業研究テーマに興味を持って声をかけてくれたのでモチベが上がった。様々な視点で研究にコメントを頂けるのはありがたいなあ。
  • 発表される分野が幅広い為、新鮮な話がいくつかあったし、逆に自分が何を話しても一定数の人にとっては新鮮なのでwin-winな構造。
  • 夜の交流イベントは、グループに分かれて、箱の中身を当てるアレとか、指示を出してレゴを組み立てる競技とかで競い合った。勘が外れて難易度の高いタスクを選ぶなどの戦犯行為を犯した記憶がある…。

おすすめな所

  • B4で参加すると、時期的に中間発表の直後くらいでちょっとだけ余裕がある。かつ研究テーマに対して少しは語れる程度の基礎が出来上がっているので、5分くらいの発表、上手くいくと15分くらいの発表は自然に出来たりする。とてもちょうど良い。
  • 自分の場合、なんか学科の強い人達は更に強い情報系エンジニア達との交流で濃い時間を過ごしてるみたいだぞ…みたいな感覚はB3あたりからあったが、そう言う場でのアイデンティティとなる技術や経験がある訳ではなかった。B4でちょっと語れる事が出来たタイミングで、こういった場に出てみて刺激を受けるのは良い経験になった。

まとめ

  • eeic出身の参加者増えろ!(今年は私1人)(それでも十分楽しめるけどね)
  • 記憶を辿って後で追記するかも

初心者の目から見たCoq/SSReflect/MathComp

What is this 記事?

この記事はeeic (東京大学工学部電気電子・電子情報工学科) Advent Calendar 2018 その2 18日目に参加しています.

  • 真面目で面白い事が書きたくなったので, Coqの記事を書いてみた

  • ゴリゴリの情報科学っぽいことを初心者がやってみたよノートなので対象者は限られるかもしれないが, eeicにも興味を持ちそうな人はいるはず

  • 少し変わった世界に触れ, 敷居を低く感じてもらったら嬉しい

はじめに

この記事はほぼこの本[1]の内容を参考にしています.

Coqは証明支援システムの一つである[2]. と言われても何のことだか分からない. OCaml(eeicB4夏の神授業たるプログラミング言語で習う奴)で実装された, 記号論理学ツールだと思って頂ければ多分問題ない.

教養時代に記号論理学を取った人なら少しピンとくるであろう, 矛盾なら全て成り立つとか, 命題だの否定だのを導入したり除去したりする, アレだ. プログラミング言語の範疇には多分入る…と思うが, 議論せんそうが起こったらゴメンなさい.

そう, どうせ学科の人はverilogだのsqlだの, なんかプログラミング言語ではないらしい何かの概念の概要を知っている人が多いので, プログラミング言語である時点で, ゆるふわで, メジャーで, 受け入れ易くて然るべきだ.

SSReflectはCoqの拡張機能, MathCompはそのライブラリ, と言う立ち位置らしいが, 正直まだピンと来ていない. この記事では, 命題や導入・除去っぽいものを書いてるのがSSReflect+MathCompの文法で, それを正しいとIDE上で解釈している部分がCoqの仕事みたいなふわっとした理解で多分良い.

ちなみに, 真面目な呼び方をすると命題やその証明を書き綴ることは「形式化」, それが正しいと機械に判別させることは「検証」と呼ぶ.

どこがeeicっぽいんですか

が好きな人は雰囲気がもろ同じだし.

で少しだけ三段論法をフニャフニャするプログラムみたいなのを学ぶのでその関連知識みたいな所がある. また, 入り口は記号論理学めいているが突き詰めると確率や情報理論の定理も形式化出来る(通信路符号化定理もあるよ)ので,

  • 情報通信理論

は間違いなく関係あるし, ワンチャン統計的機械学習アルゴリズムも関連する. これは間違いなくeeic, 完全にeeic.

証明てw何がすごいんですか?

ソフトウェアのコードも要するに大量の計算で, 正しさが証明されるべきであり, 証明されたものは安全である(雑理解). 故にVerificationという, ソフトウェアの安全性に関わる分野に利用されるし, 元々, 私はセキュリティ系の興味でCoqの存在を知った. ブロックチェーン辺りの安全性の検査の為に流行ったりしてるらしい.

CoqでTLS/SSLを実装したら安全性のキモみたいな部分が分かってOpenSSLの脆弱性を発見できた[3]みたいな, 訳の分からない世界だって存在する.

もうちょっとパンピーのロマンに近付けて話題を持っていくと, 2018年現在もコンピュータの力でしか解けない事で有名な四色定理がある. あまりにも証明が複雑で長いので, Coqでチェックされる事で, まあこの証明は正しいんじゃないかということになっている [4].

(むしろロマンの破壊者では?)

そういえば, Advent Calendarのページには思いっきり「画像処理っぽい何か」と研究の何かを書く予定だったらしき記述があるが, 四色定理の証明は画像を処理しているので, ギリギリ予定通りと言ったところか.

インストール

Mac

恐らくMacに対する環境構築が一番引っかかりやすいし, 私もMacでやったので, そうでない人はこれ[5]で多分出来るので出来てくれ(不親切). CoqIDEという環境も加えてインストールする. やり方は複数あるがopamというOCamlのパッケージマネージャを使うのが恐らく丸い.

brew install opam

からの snap.textfile.org

にある奴をopam install coqide.8.7.0 ではなくopam install coqideで行う方法で入れた.

環境はmacOS10.14.1である.

使ってみる

f:id:seldonian:20181218025059p:plain
coq_test

左の窓がスクリプトエリア, 右上の窓がゴールエリア, 右下の窓がレスポンスエリアだ. 基本的にスクリプトエリアに証明を書き, デバッガのように一行ずつ読み込んで行けば, ゴールエリアに, 何が仮定なのか(横線の上部分), 何がまだ証明されていないのか(下部分)が映るという構造だ.

読み込み方は矢印のクリックで行う, ほぼ直感通りに動くし, やり直しも容易で夢のよう.

文法の解説が結構つらい事に薄々気付き, もう紹介出来ればいいやみたいな雑な気持ちになったので概要だけ説明する.

Hypothesisが仮定でTheoremが証明したいものみたいなのは雰囲気で理解してもらい, ProofからQedまでが証明の記述だという事も雰囲気で理解してもらう. X, Y:Propは, XとYという名前の命題がありますよ程度の意味.

move: というのはタクティクスと呼ばれる手続きで, ここでは「仮定Xと証明したいものYがあった時, Yを(XならばY)に遷移させる」手続きだ. Xが仮定なら, (XならばY)を証明するだけでYは証明されるので正当な手続きだ. よって今画面にはX->Yが証明したいものとして映っている.

次にby という行を読み込ませるが, by はターミネータと呼ばれる処理で, 「証明したいもの」「自明じゃん乙w」って言って削除してくれる. よく見たらX->Yは仮定にあるので, 自明, という解釈だ. これで「証明したいもの」は無くなるので証明は完了する.

やや難しい奴

Coqはデフォルトは直観主義論理らしいので, 排中律を仮定しないと古典論理として動かない. 記号論理学を取った人は, 直観主義論理に加える仮定として, 背理法, 排中律, 二重否定除去は同じ意味を持つ, みたいな綺麗なことをやったと思う.

f:id:seldonian:20181218032423j:plain
美しき三位一体の図, JavaScript

その「同じ意味」であることを確認する為に, その中のごく一部であるが「直観主義排中律が仮定されたら二重否定除去も出来る」を証明させる(正確には人間が証明手続きを書きゴールエリアの反応で確かめる)とこうなる.

f:id:seldonian:20181218031211p:plain
排中律→二重否定除去

プラスマイナス記号はただのインデントで意味はない.

move=>hoge は証明したいものがX->Yとかの場合にXにhogeという命題名を付けた上で仮定側に持っていく操作.

move\ hugaは, 仮定hugaがあり, 証明したいものがX->Yの時に, 証明したいものを(huga /\ X) -> Yに変える操作.

case:A\/B は, A\/Bが証明済みである時に, 証明したいものがXならばA->XとB->X両方証明すればいいじゃん的な変形をする操作である. これ以上の説明が苦しくなってきたので雰囲気だけ分かる落書きを貼る.

f:id:seldonian:20181218084831j:plain

こんな感じで証明の正しさが分かるらしい. 多分人間より頭のいいことをやっている.

最後に

不完全性定理の証明[6] コピペしてポチポチするだけで記述が変形して証明が進み, 何も分からないけど幸せになれる.

四色定理の証明[7] gitで証明が手に入る時代. ただし複数ファイルのコンパイルが必要で面倒(やり方を調べ中で私にもチョットワカラナイ).

テキトーな理解を晒しているのであまりスゴイ人に見つかりたくないので技術系なのにqiitaではなく自分のブログに書きました.

とはいえ, 仮にヤベーこと言ってたら是非ともボコボコにして出来れば色々御教授願えればありがたい.