過去・現在・未来

1月29日、丸山の連続セミナー「楽しい数学」で「「同じ」を考える 」というテーマでセミナーを開催します。 https://mathnight4.peatix.com/ 日常のあたり前に見えることにも、すこし考えると当たり前ではないことが潜んでいます。今回は、「同じ」の数理を考えます。皆さんの参加をお待ちしています。 ---------------- セミナー概要 ---------------- 数学では、「同じ」「等しい」というのは、もっとも基本的な概念の一つです。 　「2 x 3 は、3 x 2 と同じである」 　「2辺とその狭角が等しい三角形は、同じ三角形である」 　「自然数と有理数は、同じ数だけ存在する」 　「ドーナツとコーヒーカップは、実は、同じ形である」 ただ、これらの例での「同じ」は、全く「同じ」ではありません。 日常でも、「同じ」という言葉は、よく使われます。 　「彼と僕の身長は同じです」 　「同じ時間、同じ場所で、共に過ごした仲間」 　「みな、同じ気持ちです」 　「この英語と日本語の文章は同じ意味です」 ここでも、「同じ」という言葉は、全く「同じ」ではありません。 これらの表現を、「同じ」という言葉を使わない表現で言い換えてみようとすると、とても難しいことに気づきます。それは、「同じ」という概念が、他の言い換えができないほど基本的な概念であることを意味しています。 セミナーでは、自明なように見えるが、多様さも併せ持つ、「同じ」の数理を探ります。セミナーでは、また、一昨年急逝した数学者のVoevodskyの「同一性」をキーコンセプトにした数学の基礎づけの試みを紹介します。

1/8マルレク「意味の形式的理論」と懇親会の様子です。資料のURL改めておしらせします。不都合がありましたら教えてください。 https://goo.gl/CPXndH

明日のマルレクの講演資料です。 https://goo.gl/CPXndH 　ご利用ください。資料長いのですが、背景がピンクのスライドをザッピングすれば、大まかな流れは伝わると思います。 ---------------- 「はじめに」 ---------------- 人工知能技術にとって、自然言語の意味の理解は、重要な課題である。小論は、自然言語の意味を形式的に把握しようという試みを概観したものである。 第一部では、まず、現在の主要な三つの自然言語処理技術の現状を紹介し、あわせて、言語の意味理解にフォーカスして、様々な取り組みを取り上げた。 こうした技術を評価する上で、筆者の取っている基本的な視点は、次のようなものである。 　　文と意味の「構成性（compositionality）」 　　意味の「同一性」 / 意味の共通表現の存在 残念ながら、文が語から文法に基づいて構成されることは、現在主流の自然言語処理技術では、ほとんど考慮されていない。文法性の認識がないのでは、文の意味の構成性の認識を持つことは難しい。 ただ、文の意味の構成性の認識なしにでも、意味については考えることができる。一つには文を構成する「語の意味」、もう一つには「意味の同一性」に基づく「意味の共通表現」の模索である。第一部の後半では、これらの取り組みを取り上げた。 「語の意味」の表現では、その客観性・共通性を「実在」の関係に基礎をもつOntology、語の利用の頻度の統計的分析に帰着させるWord2Vec的「分散表現」、辞書項目に諸特徴を枚挙するスタイル、 conceptual spacesを構成するアプローチ等多様な試みが行われている。 「文の意味」の表現については、論理式（あるいは、ラムダ式）による表現と多次元ベクトルによる分散表現の二つがある。後者は、実装者にはそういうものとしては、あまり自覚されていないようにみえるのだが。 機械翻訳技術の成功は、二つの言語の意味の「共通表現」を多次元ベクトルによる分散表現として抽出しているところにあると筆者は考えている。もっとも、語の意味も、文の文法性も、このアプローチでは、直接には考慮されていない。 筆者は、論理式による表現が「好み」なのだが、文から論理式への還元は、文法に応じて様々の流儀がある。この点

「アリー　スター誕生」みてきました。稚内で映画見たの初めてです。 稚内に映画館がなかった時には、映画が見たくて見たくて、東京に行くと一日三館はしごしたりしていたのですが、東京にいるといつでも見れると思うせいか、むしろ映画見る回数減りました。軟弱な映画ファンです。 主題歌の Shallow とてもDeepなこと歌っていることに気づきました。 　Tell me somethin', girl 　Are you happy in this modern world? 　Or do you need more? 　Is there somethin' else you're searchin' for? 　I'm falling 　In all the good times I find myself 　Longin' for change 　And in the bad times I fear myself ブラッドリー・クーパー演ずるアリーの夫の姿が、エイミー・ワインハウスのことを思い出させて悲しくなりました。（ホイットニー・ヒューストンでもいいのでしょうが、僕はエイミーが好きなんです）

あけまして、おめでとうございます。 今年もよろしくお願いします。 そのうち、僕は、あたまもおめでたい人になるのでしょうね。 その時は、よろしくお願いします。 浅知恵で、そうなる前にと考えて、昨年はやることを変えました。やりたいことをやれるうちに、できることをできるうちにやるのが、一番いいと思ったからです。残っている時間は自分ではわかりませんからね。それは若い人も一緒なのですが。 それまで何年かディープラーニング技術にフォーカスしていたのですが、関心を、量子情報理論・言語理論・数学の基礎の三つに切り替えました。三つの関心には脈絡がないように見えますが、僕の中では繋がっています。人工知能への関心は、結局、我々自身 -- 人間 -- の認識能力への関心に他ならないと考えています。 この30年間、IT技術の「ちょっと先の未来」について語ってきました。くじ運だけは強いので、クラウドでもモバイルでもAIでも、短期の予想は外れたことはありません。ただ、これからは、いろんな機会にいろんな形で、もう少し長いスパンで、人間と科学の未来について語ることができればと思っています。 なんの根拠もないのですが、21世紀の科学は、産業革命を準備した「科学革命」以来の大きな変革期に入るだろうという「予感」が僕にはあります。僕は自分の「予感」を信じています。 僕は、人間は、様々な危機を乗り越えて進むことができるという「希望」を持っています。「失望」には理由が必要ですが（例えば、「GoogleやFacebookには失望した」というような場合）、希望を持つのに理由は必要ではありません。絶望だって希望の十分な理由になります。 もちろん、未来を作るのは、僕ら古い世代の仕事ではなく若い世代の仕事です。僕らは、いずれこの世からいなくなります。 といっても、悲しいことに、若くてもなくなる人はいます。 僕が一番注目していた数学者Voevodskyは、一昨年、9月に51才で突然なくなりました。 昨年3月、僕の6つ下の弟がなくなりました。 昨年6月、20才で殺されたXXXTentacionの"Skins"を、この冬休み聴きました。前作のアルバム "？" を、僕は毎日聴いて泣いていました（嘘かも）。やはり、死んじゃいけないんですね。

先に、「同じ」型A に属する二つの項 aとb（a : A かつb : A）が「同じ」だという a = b : A で表現される「同じ」さと、二つの型AとB（A : Type かつB : Type）が同じだという A = B : Type で表現される「同じ」さは、同じ「同じ」でも、違う「同じ」であるという話をした。 前者は、例えば、Aを「三角形」という型だとして、三角形a と三角形b が「同じ」だと言っているのだが、後者は、例えば、Aを{異なる三つの点を結んでできる図形}、Bを{平行でない三つの直線で囲まれた図形}とした時、AとBは、同じ型の図形であることを主張している。 型を持つプログラミング言語の場合、あるインスタンスがどの型に属するかを意識することは大事なことだ。面倒と言えば面倒なのだが、そのことがプログラムの誤りを少なくするのに効果的なのだ。 型を持つプログラミング言語のうちのいくつかは（例えば、COQ, Agda, Haskell, 部分的にはScalaも）は、不思議な型 dependent type をサポートしている。dependent type は、パラメータによって（パラメータにdepend して）、型が変わる型だ。 パラメータxが型Bを持つなら、このdependent type E(x)を次のように表す。 　　　(x : B) E(x) また、あるsが、dependent type Eを持つことを、次のように表す。 　　　(x : B)  s(x) : E(x) あまり正確ではないが、B={ 整数、実数、複素数 }として x : B なるパラメータ x によって、dependent type E(x)は、整数型、実数型、複素数型 に型が変わるのだ。 昔のwakhok時代、同僚の浅見さんから、dependent type がすごいことはよく聞いていた。ただその頃、僕はそれをよく理解できなかったのだと思う。僕が、その重要性に気づいたのは、だいぶ後になってからだ。 5年前の2013年のマルレク「「型の理論」と証明支援システム — Coqの世界」で、ようやく後追いを始めることになる。 https://www.marulabo.net/docs/typetheory-coq/ 　

あるものAとあるものBが「同じ」だというのは、何を意味するのだろう。 もしも、AとBが数字なら、その意味ははっきりわかる。 例えば、A=1でB=1なら、AとBが「同じ」だということになる。それは、1=1のことだ。 もしも、AとBが集合なら、AとBが同じだということは、Aに含まれる要素がBに含まれる要素が全て等しいということだ。集合 A={ りんご、みかん、バナナ } は、集合 B = { バナナ,  みかん. りんご } と「同じ」である。 もしも、AとBが三角形なら、二つの三角形の二辺の長さが等しく、その二辺が作る角度が等しい場合、三角形Aと三角形Bは、「同じ」だと言える。 これらの例でわかることは、あるものとあるものが「同じ」だというためには、それぞれが、同じ種類のものでなければならないということ。数字と三角形は、「同じ」にはなれない。 ここでの「同じ種類」というものを、「同じ型を持つ」ということにすれば、あるものAとあるものBが「同じ」だというためには、AとBは、「同じ型」を持っていなければいけないということになる。 このあたりのことを、数学者のドリーニュが例を挙げて丁寧に説明しているビデオがある。"What do we mean by "equal" " https://goo.gl/nXhqmb 今年の9月にプリンストンの高等研究所で開催された "Vladimir Voevodsky Memorial Conference" https://www.math.ias.edu/vvmc2018 での、彼の講演である。 ドリーニュは、若くして、グロタンディックを出し抜いて「ヴェーユ予想」を解いた有名な数学者なのだが、不思議なことに、彼が説明していることは、コンピュータでプログラミングをしたことがある人は、よくわかっていることだということである。 整数 A=1 と浮動小数点実数 B=1.0 とは、コンピュータ内部での扱いは違うものである。もしも、あるプログラミング言語が、整数型・実数型の他に複素数型をサポートしているとすると、A=1, B=1.0, C=1.0+0.0i は、皆、違うものである。 数字の場合いずれの型にも、加減乗除の演算は定義される。複数の型に適用