投稿

3月マルレク「コンピュータ、数学の問題を解き始める」について

【 3月マルレク「コンピュータ、数学の問題を解き始める」について 】 3月のマルレクは、「コンピュータ、数学の問題を解き始める」というテーマで開催しようと思っています。 この2月に、Deepmind / Open-AIはとても興味深い発表を行いました。 「数学オリンピックの形式的問題(のいくつか)を解く」 "Solving (Some) Formal Math Olympiad Problems"  https://openai.com/blog/formal-math/   国際数学オリンピックのいくつかの問題をコンピュータを使って解いて見せたのです。 たとえば、こんな感じです。 問題(2000年の数学オリンピックの問題だそうです) Prove that if |x - 2| = p, where x < 2, then x - p = 2 − 2p. ( |x - 2| = p とする。 x <  2 の時、x - p = 2 - 2p  となることを証明せよ。) 証明 Since x < 2, |x - 2| = - (x - 2). Using p = |x - 2| , we have x = 2 −  p and finally x - p = 2− 2p. ( x < 2 なので、|x - 2| = - (x - 2)である。p = |x - 2| を使えば、x = 2 −  p である。結局、x - p = 2− 2p となる。) 先の論文には、この例をふくめて6つの例が紹介されています。実際には、コンピュータは、形式的証明を返すのですが、ここで紹介したのは、「非形式的 Informal」な証明です。マシンは、Informal ボタンを押すと、こうした「非形式的」証明を返してくれます。形式的証明を非形式的証明へ要約・翻訳できるのも面白いです。 Deepmindは、数学へのAIの利用について、昨年12月、Natureにこんな論文を発表していました。それは、数学者に向けてAIも使いみちがあると述べたものでしたが、今回の発表は、そうした関心と方法の延長線上にあるものだと思います。ただ、今回の方が訴求力は大きいように思います。 "Advancing mathematics by guiding human

マルゼミ「認識の認識」講演ビデオ公開しました

【 マルゼミ「認識の認識」講演ビデオ公開しました】 MaruLaboでは、以前に行った講演ビデオを公開しています。  今回は、昨年11月26日に開催した マルゼミ「認識について考える 2 — 認識の認識」の講演ビデオの公開です。ご利用ください。 https://youtu.be/mGtP4zXollg?list=PLQIrJ0f9gMcNMN9xrRQiZ7bAsTFSeTiZO 以下の四つのビデオの再生リストです。 YouTubeの「チャプター」機能で、ビデオの途中からの視聴が可能になっています。お試しください。(PC/Mac をご利用の方は、ビデオの説明のなかの「もっとみる」をクリックください。)  ● Part 1 Grzegorczykの「科学の探究」モデル https://youtu.be/mGtP4zXollg?list=PLQIrJ0f9gMcNMN9xrRQiZ7bAsTFSeTiZO 00:00  はじめに 03:01 Grzegorczykの「科学の探究」モデル 07:57 情報の順序関係 16:25 Forcing Method  ● Part 2 Kripkeの「可能的世界」 https://youtu.be/OQbw8ztYACU?list=PLQIrJ0f9gMcNMN9xrRQiZ7bAsTFSeTiZO 00:00 Kripke の「可能的世界 」 06:54 「可能的世界と情報 12:34 「可能的世界」へのジャンプ 16:42 認識の特徴を表現するモデル 23:08 前節までのまとめと補足  ● Part 3 Bayesian推論と相対エントロピー https://youtu.be/n9Q4KFcAfq8?list=PLQIrJ0f9gMcNMN9xrRQiZ7bAsTFSeTiZO 00:00 Bayesian推論と相対エントロピー 01:01 相対エントロピーとは何か? 06:03 PriorとPosteriorで「認識の発展」を記述する 11:38 Deep Learning と相対エントロピー  ● Part 4 Jaynesの「最大エントロピー原理」 https://youtu.be/ejhCjxchtGU?list=PLQIrJ0f9gMcNMN9xrRQiZ7bAsTFSeTiZO 00:00 Jaynesの「最大エ

Transpose とcup, cap

【 Transpose とcup, cap 】 cupは入力を出力に、capは出力を入力に反転させる操作です。この操作を適用すると、たとえばcapを使えば、入力をもたず二つの出力のみをもつ「二部状態」は、一つの入力と一つの出力を持つ「プロセス」に変換されます。こうして、「状態」と「プロセス」は、一対一に対応することが示せます。 今度は、入力Aと出力Bをもつプロセスf への、cup, cap の適応を考えます。入力Aにcupをつなげ出力Bにcapをつなげば、プロセス f は、入力Bと出力Aをもつ新しいプロセスに変換されます。こうしてできたプロセスを、f の「Transpose」と言います。 Tranposeは、線形代数ではおなじみの概念ですね。それは、行列の行と列を入れ替えて「転置」行列を作る操作です。転置行列を習ったときに、それがエンタングルメントと関係があると思った人は、誰もいなかったと思います。 ところが、そうじゃないんです。 cupはエンタングルメントを表します。yanking等式によれば、capはcupの逆変換です。プロセス fのTransposeがcupとcapで表せるということは、実は行列の転置も、エンタングルメントの言葉で表現できることを意味します。 エンタングルメントは、なにか現実とはかけ離れた奇妙な概念ではなく、我々のごく身近なところに存在しています。ただ、我々は、それが数学的にも物理的にも基本的なものであることに気が付かなかっただけなのです。 今回から、プロセスをあらわす箱の形が少し変わりました。長方形の角を切り落として台形になりました。このノテーションも秀逸です。図形的には、Transposeは、図形を 180度回転させることに対応するのですが、長方形だと回転前と回転後の区別つきませんからね。 なんと、Transposeは、プロセスが cupの谷あるいはcapの山をこえることを表現していることがわかります! 今回のセミナーでは、図形の「回転」としてTransposeを解釈したのですが、水平方向あるいは垂直方向に鏡をおいて、その鏡像反転として新しい図形を考えることができます。その解釈については、また別の機会に触れたいと思います。 ショートムービー「Transpose 」を公開しました。 https://youtu.be/mMywPckI2bw?l

yanking等式について

【 yanking等式について 】 先に、cupとcapは、String Diagramで、もっとも特徴的な図形だと述べました。実は、cupはその線の両端が、エンタングルメント状態にあることを表しています。String Diagramは、エンタングルメントを、一つの図形記号で表すのです! yanking等式は、二つの図形が等しいことを示す図形についての等式です。具体的には、String Diagram では、cupとcapを結んだ山と谷からできた曲線が、その凸凹をならした一本の直線と同じものとして扱うことができることを主張しています。 図形として考えると、二つの図形が同じものであるのは、直観的には明らかに思えます。 ただ、このyanking 等式が表現しているものを、数学的に説明しようとするとかなり手強いことになります。  「それは、monoidal categoryである compact closed categoryの基本的性質を表現している。 .... 」 ご安心を。 確かに、compact closed category の基本的性質は、いくつかの「数学的等式」によって表現されるのですが、yanking 等式の「図形的等式」は、その基本的数学的性質を完全に表現しています。 何も、面倒な数学的議論にさかのぼらなくても、図形的な直観にしたがって議論をすすめても、正しい議論を展開できるのです。それはある意味、驚異的なことです。不思議な経験です。  「String Diagramは、深いことを表現しているけど、わかりやすい。」 皆、String Diagramが大好きなのは、そのためです。yanking等式は、その典型です。 ちなみに、yank は「ヤンキー」のもとになった言葉です。南北戦争時代、北軍の兵士は 南部の人から  Yankee と呼ばれたようです。その後は、アメリカ人をさす言葉として世界中で広く使われました。 そのせいか(しらんけど)、String  Diagramの世界でも、アメリカの研究者は、"yanking  equation" という言葉をあまり使わないような気がします。 "snake equation" とかいいますね。 ショートムービー「yanking等式 」を公開しました。 https://youtu

cupとcap

【 cupとcap 】 cupとcapは、String Diagramの中の図形で、もっとも特徴的な図形の一つです。 cupは、A × A という同じ型を持つ二つのの出力だけを持つプロセスです。 capは、A × A という同じ型を持つ二つのの入力だけを持つプロセスです。 cap,  cupの名前の由来は、スライドの図を見ていただければ、たぶん、了解できると思います。 capとcapは、String Diagramの中で、どのような役割をもつのでしょう? いくつかの例を見てみましょう。 cupの一つの出力を、別のプロセス fの入力につなげることができます。その図式はすぐにかけますね。その「解釈」もすぐできると思います。そのまんまです。 今度は、cupの右の出力を、capの左の入力につなげてみましょう。プロセスの出力をプロセスの入力につなげるのは普通の操作です。その図式はすぐにかけると思います。でも、この図は、どのように解釈すればいいでしょう? 今度は、cupの左の出力を、capの右の入力につなげてみましょう。この図式もすぐにかけると思います。でも、この図は、さっきの図とはちょっと似ていますが、別のものです。これらは、どのように解釈すればいいでしょう? 今回は、これらふたつの図式の解釈を提供します。 ショートムービー「プロセスと状態の双対性 」を公開しました。 https://youtu.be/U9MYthX8UFY?list=PLQIrJ0f9gMcPSp_fL7-LZW0yOwYXyvXtb スライドのpdfは、次からアクセスできます。 https://drive.google.com/file/d/1jiIkIBaVk2SHVZlzJ0Rf9qkpy3lqUnhE/view?usp=sharing このシリーズのまとめページは、こちらです。ご利用ください。 https://www.marulabo.net/docs/category01/ セミナーのお申し込みは、次のページからお願いします。 https://string-diagram.peatix.com/

String Diagram の新世界

 【 String  Diagram の新世界  】 この節から、新しい内容が始まります。 いよいよString Diagramの新しい世界が始まります。  「これまでも String Diagramの話じゃなかったの?」  「そうなんですが、それは、ちょっと長い助走期間。お楽しみはこれからです。」  「何が始まるの?」  「量子過程を図解します。」  「最初から、そう言っていなかった?」  「そうなんですけど、これまでは主要に量子コンピュータの回路の話でした。」  「その話だけじゃだめなの?」  「多分、そうです。」  「あと何があるの?」  「量子過程の図解です。   図形で考えることができることを示しながら、   エンタングルメントを図解します」    ショートムービー「分離可能性」を公開しました。 https://youtu.be/qc3GKXyDZr4?list=PLQIrJ0f9gMcPSp_fL7-LZW0yOwYXyvXtb スライドのpdfは、次からアクセスできます。 https://drive.google.com/file/d/1jR5bTmfD5EQWq42e9JJ5mVh3TM--PvEm/view?usp=sharing このシリーズのまとめページは、こちらです。ご利用ください。 https://www.marulabo.net/docs/category01/ セミナーのお申し込みは、次のページからお願いします。 https://string-diagram.peatix.com/

天才 ディラック

 【 天才 ディラック 】 複雑なものを理解しようとする時、複雑なものをどのように表現するかという問題は、とても大事です。 「それは、単なる表現手段・表記法の問題で、対象の物理的・数学的本質とは関係ない」と考える人がいるかもしれません。ただ、僕は、そうではないだろうと考えています。優れた表記法は、対象全体の見通しをよくし、新しい洞察を可能にするからです。 量子の世界を記述するのにディラックが考案した「ket記法」は、とても優れたものです。ディラックの物理学上の業績をよく知らなくても、「ket記法」だけでも、彼の「天才」をうかがい知ることができると思います。 量子の世界を知る上で、ディラックの「ket記法」は、必須のツールだと思います。興味ある方は、次のページをご覧ください。  「ケット |k> で理解する量子の世界」 https://www.marulabo.net/docs/ket-talk/ String Diagram も、量子の世界を記述する新しい表現法の一つです。そこでは、「数式」ではなく「図式」が利用されています。 興味深いことに、ディラックの「ket記法」とString Diagram との間には、対応関係が存在します。今回は、その話をしようと思います。 ショートムービー「ket記法との対応」を公開しました。  https://youtu.be/Qw4sjm-mb6U?list=PLQIrJ0f9gMcPSp_fL7-LZW0yOwYXyvXtb スライドのpdfは、次からアクセスできます。 https://drive.google.com/file/d/1iR5QumVG_zs3FnqBZ2o84NAyL04nGU-6/view?usp=sharing このシリーズのまとめページは、こちらです。ご利用ください。 https://www.marulabo.net/docs/category01/ セミナーのお申し込みは、次のページからお願いします。 https://string-diagram.peatix.com/