過去・現在・未来

【「量子情報と通信技術 -- 「量子インターネット」という未来」へのお誘い 】 4月30日のセミナーは、「量子情報と通信技術 -- 「量子インターネット」という未来」と言うテーマで開催します。 この間、量子論・量子情報理論には、「量子コンピュータ」と「量子情報通信」という二つの大きな応用分野があるという話をしてきました。今回は、後者の「量子情報通信」にフォーカスして、特に、その技術的到達点の現状を紹介しようと思います。 量子情報通信では、研究者が実装にしのぎを削っている研究・開発分野は二つあります。一つは、量子暗号とその量子キー配布の実装で、もう一つは、量子テレポーテーションの実装です。いずれの分野でも、近年大きな進展があります。そうした動向を紹介するのが、今回のセミナーの目的です。 セミナーは、次のようなトピックを取り上げます。基本的には、代表的な論文の紹介というスタイルで構成しようと思っています。 【量子暗号と量子キー配布】 日本も頑張っているこの分野では、2021年の1月に、中国の研究チームが、Nature誌に投稿した論文の概要を紹介します。彼らは、光ファイバーだけでなく衛星も使って、宇宙と地上を統合する 4,600kmに及ぶ、量子キー配布のネットワークを実装しました。 【量子テレポーテーション】 この分野では、2020年の7月に、アメリカの研究チームが arXiv に投稿した論文を紹介します。彼らは、22km離れた地点を光ファイバーで結んで、90%以上の信頼性で安定的に量子テレポーテーションを行うことに成功しました。 【量子リピーター】 量子通信の技術的なネックの一つは、現在の光通信で利用されている中継増幅器は、量子の状態を壊してしまうので、そのままでは使えないことです。量子の状態を壊さない中継器を「量子リピーター」と言います。この分野の取り組みの現状と課題を紹介します。 【量子インターネット】 興味深いのは、量子通信技術の着実な発展の中で、「量子インターネット」の構想が立ち上がりつつあることです。最初は、小さな動きでしたが、近年は大きな流れになりつつあるように思います。セミナーでは、「量子インターネット」と言う言葉を、多分、最初に使ったと思われる、2008年のarXivへの投稿論文を紹介します。 インターネットの未来については、現在、さまざまな議論がありま...

【 Open-AI Theorem Proverの限界 】 セミナーは今日なのに、大事なことを書くのを忘れていました。 というか、途中で、セミナーの構成を変えたのですが、その時、先に作っていたショートムービーの公開を飛ばしてしまっていることに昨日になって気づきました。公開資料もその部分を埋めたものに更新しましたので、改めてアクセスください。 どたばたしてすみません。 抜けていたのは、Open-AI Theorem Proverのチームの論文の結論部分の紹介です。 彼らは、率直に、Open-AI Theorem Proverの証明能力には限界があることを認めています。その評価は、妥当なものだと思います。 「現在のその主要な限界は、二つあるいは三つ以上の自明ではない数学的推論をつなげていくことの無能力さにあると考えている。このことが、（例外的にではなく）整合的に数学オリンピックの問題に挑戦することを妨げている。」 「複雑な推論ステップを必要とする証明の多くは、現在のコンピュータの能力の地平を超えたところにある。我々が、たとえ挑戦的な数学オリンピックの問題のいくつかを解いたとしても、我々のモデルは、いまだこれらの競技の最も優秀な学生たちと競争するにははるかに遠い場所にいるのである。」 【「Open-AI Theorem Prover -- 論文の結論にみるその「限界」の認識」を公開しました 】 https://youtu.be/ICkF3ocX5JI?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのpdfは、次からアクセスできます。 https://drive.google.com/file/d/12HljpZNPJl6b0G2XUDbhnka1wlndjavn/view?usp=sharing セミナーの申し込みは、本日のセミナー開始（19:00）まで受け付けています。 https://math-proof.peatix.com/ このトピックのまとめページは、こちらです。 https://www.marulabo.net/docs/math-proof/

【 3//26 マルレクの講演資料公開しました 】 3/26 マルレク「コンピュータ、数学の問題を解き始める」の講演資料を、MaruLaboのページ  https://www.marulabo.net/docs/math-proof/   で公開しました。ご利用ください。 講演資料は、次のURLからも直接アクセスできます。 https://drive.google.com/file/d/12726t4yD0ouUngmFXSy2UIzvQptSdP6g/view?usp=sharing 【 3/26 マルレクの申し込み受付中です！ 】 3/26マルレクのお申し込みは、次のページから受付中です。 https://math-proof.peatix.com/

【 数学のスタイルが変わる? 】 Voevodskyが危惧したことは、数学は、累積的（accumulative）な性格を持つので、そこに誤りが紛れ込むと、誤りも累積する危険があるということでした。彼は、それを数学の危機だと考えます。 彼は、数学への誤りの混入を避ける唯一の道は、数学の証明を、コンピュータで検証できるプログラムの形にすることであると考えるに至りました。ただ、その当時（もう21世紀に入っていたのですが）、そうした彼の考えを支持する数学者は、ほとんどいなかったと言います。 2010年頃から状況は変わり始めます。Voevodskyが提唱するHomotopy Type Theory に基づく数学の新しい基礎づけ Univalent Foundationが数学者の注目を集め始めます。2012年から2013年にかけて、プリンストン高等研究所は、"Special Year"を設定し、Univalent Foundationについての大規模な連続セミナーを開催し大きな成功をおさめます。数学者の関心は大きく広がりました。 Univalent Foundationは、数学理論として新しい内容を持つのですが、それらの理論の形式化をコンピュータ上の証明支援システムで行うことに適しているという特徴があります。特筆すべきは、Voevodsky は、Univalent Foundationに基づく数学の基礎づけ・再構成を、彼の主張に忠実に、GitHubで公開されたコンピュータ・プログラムの形で実行して見せたことです。こうして、それまで、数学でのコンピュータ利用に懐疑的だった多くの数学者の見方は変わり始めます。 コンピュータ上の証明システムは、個々の数学的証明の正しさの検証に使えるだけではありません。大規模な数学の形式化を整備することで、数学者のコミュニティが、形式化された定義や定理や証明を共有し、検索可能なライブラリーを構築することを可能になることを、数学者は気づき始めています。 21世紀の数学のスタイルは、今とは違ったものになっていくでしょう。 【 「Univalent Foundation」を公開しました 】 https://youtu.be/1zm8E2Y7vyY?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのp...

目の前から、人間が作ったもの、人間に関わるものを、すべて消してみましょう。それでも、自然はあるがままの姿で、広がっているように思えます。野に咲く花も、空を飛ぶ鳥も、木々をゆらす風も、夜空の星も。 ただ、そうした空想を行うことが、だんだん、難しくなっています。人間のいない世界のイメージといえば、「廃墟」のイメージを持つ人がむしろ多いかもしれません。それでも自然は残ると僕は思うのですが。それは、私たちの日常的な視界から、自然が見えにくくなっているからだと思います。 一方で、現代は科学の時代だと多くの人が考えています。ただ、科学の主要な対象である自然から、私たちは、どんどん遠ざかっています。そのことは、自然に対する関心だけでなく、いずれ、科学に対する関心をも失わせる力として働くことになると感じています。 科学を私たちにとって疎遠なものにする、もう一つの大きな力があります。 それは、そもそも、科学が歴史的には、冒頭に述べたような素朴な自然観から、自分を意識的に分離することで生まれたことによるものです。 私たちの遠い遠い祖先は、自然と深く結びついていました。というより、圧倒的な自然の力の前に人間は無力でした。ただ、自然に対する畏怖・感嘆の念を持ち得たことは、人間を他の動物とを区別するものです。それは、その後、宗教・芸術・科学等に枝わかれしていく、すべての人間の営みの原始の共通の起源になりました。 時間を何万年か進めます。話は少し飛躍します。 現代では、科学は、主要に「科学者」という専門家集団によって担われています。彼らは、特殊な訓練を受け、特殊な言葉で話します。その言葉は、一般には、わかりにくいものです。 「科学者」が人口に占める割合は、大きなものではありません。おそらく宗教が支配的であった時代、どの村々にも必ず存在していた神職者が人口の中で占めていた比率を上回ることはないと思います。 （科学の世界では、博士号を取得した科学者の卵たちの「過剰」に悩まされています。それは、社会的には「構造的な問題」なのですが、僕は、むしろ、歴史的には必然的な傾向のように考えることができると思っています。） それでは、なぜ、多くの人は、実際にはかなり疎遠なものでしかない科学に対して、現代は「科学の時代」だと考えるのでしょう？ その理由は、明確だと思います。「科学」の応用としての「技術」が、現代の...

【 巨人の肩の上の小人 】 「フェルマーの定理」を証明したワイルズは、自分を「巨人の肩の上の小人」に喩えました。それは自分の仕事は先人たちの偉大な業績の上に成り立っているという謙遜なのですが、同時に、そのことは彼が数学という知の特徴をはっきりと自覚していることを表しています。 数学的知には、人間の認識によって獲得されたものとしては、独特の性質があります。それは、いったん数学的に「真」であることが証明された定理は、時代が変わっても場所が変わっても、ずっと「真」のままであり続けることです。それを数学的真の「普遍性」とか「不変性」ということがあります。 そうして獲得された知は、個人というよりは人類の知として蓄積されていきます。それを数学的知の「累積性」といいます。 先に、数学者がコンピュータによる形式的証明を受容する動きが広がっている理由をいくつか見てきたのですが、最後にあげた 　「数学者は、しばしば「間違った証明」する」 というのが、結局は一番大きな理由になるだろうと僕は考えています。 偽である命題からはどんな命題も導くことができます。「間違った証明」も、誰もそうと気づかなければ、それを利用して導かれる真である保証のない「証明」も共に「蓄積」していきます。 それは、がっしりして盤石であると思われた「巨人」の足腰が、徐々に蝕まれて行くことを意味します。病んだ巨人の肩の上では、小人たち（僕らのことです）は、自由に遊ぶことはできません。 ただ、数学者も一般の人も、あまりそのことを深刻に考えていないようにも見えます。 　「専門性の高い数学者が証明を誤ることは、ほとんどない。」 　「数学者だって人間だもの、誤ることだってある。」 数学者の誤りの問題を、数学の基礎である累積性への脅威として捉えたのは、Voevodsky が始めてだったと思います。彼は、数学の形式的証明の必要性を強く訴えます。 【 「 数学的知の「累積性」」を公開しました 】 https://youtu.be/9NIcuPvrDj0?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのpdfは、次からアクセスできます。 https://drive.google.com/file/d/1-79tELOCp2Cpmo-pTIAwg7U7ow4X8LTS/view?usp=sharin...

【 数学者も証明を間違える 】 では、なぜ、数学者はコンピュータを使い始めたのでしょうか？  それには、理由があるように思います。 第一の理由は、人間の手にはあまるが、コンピュータなら解ける巨大なサイズの問題が存在するからです。一般的な解法は見当たらなくても、場合の数が有限なら、すべての場合をしらみつぶしに総当たりでチェックができるなら、問題を解くことができます。 数学の証明問題へコンピュータが最初に使われたのが、こうした方法が使われた「四色問題」であったことは象徴的です。このことは、コンピュータを使って、そういうタイプの問題に、人間がチャレンジすることが可能になったのだとも言えます。前回見たヘイルズの「ケプラー予想」の証明も、こうしたタイプの証明でした。 ただ、場合の数が有限だとしても、シラミつぶし総当たりの方法が、実際にコンピュータで実行可能とは限りません。このタイプの問題は、たくさん存在するのですが、実際にコンピュータで解けるのは、場合の数が小さい時だけです。 さらに、難しい数学の問題がすべてこのタイプである訳ではありません。むしろ、数学者の多くが取り組んでいる問題は、こうしたタイプの問題ではないのです。ですから、数学者が証明にコンピュータを使い始めたのには、別の理由があります。 第二の理由は、証明が複雑になると、証明が正しいことが検証しにくくなるからです。先に、証明が長すぎて、「その証明を、全部読んでいる数学者は誰もいない。」というブラック・ジョークを紹介しました。先に紹介した「Feit–Thompson定理」の証明は、このケースです。 　「そうだ。コンピュータを使った巨大な証明なんか信用できない。誰がその正しさを保証するんだ。」　 確かにその通りです。ただご安心を。現代の巨大証明は、検証ずみの証明支援システムを利用して、それ自身の正しさを検証しながら、証明を実行します。その意味では、1970年代にアッペルとハーケンが行った「四色問題」の証明と、21世紀になってからのゴンティエによる「四色問題」の形式的証明とは、本当は異なるものです。 証明の長さだけが、問題ではありません。例えば、全く新しいアイデアに基づく証明は、その正しさを（彼が数学の専門家であったとしても）第三者に確信させるのは難しいのです。 ペレルマンは、2002年から2003年にかけて ar...

【 セミナーの構成について -- Voevodskyの仕事を考える 】 これまでの第一部では、コンピュータに証明問題を解かせる試みとして、Open-AI Theorem Proverを紹介してきました。 これからの第二部では、数学者が証明問題を解くのに、コンピュータを利用し始めていることを紹介して、数学へのコンピュータ利用の背景とその意味を考えようと思います。 前者では、問題を解く主体はコンピュータですが、後者では、問題を解く主体は、人間＝数学者です。 数学の証明を記述するスタイルは、今、大きく変わろうとしています。これは、21世紀の数学を特徴づけるものになるだろうと僕は考えています。 第三部では、こうした流れを切り拓いた天才 Voevodskyの数学の基礎についてのUnivalent foundationsという考えを紹介します。 彼のプロジェクト UniMathは、コンピュータで検証可能なスタイルで数学を記述しようとする、初めての試みです。 https://github.com/UniMath/UniMath 　 Univalent foundationsの中核である Homotopy Type Theoryについては、別のシリーズを予定しています。 「カテゴリー論入門」セミナーについて https://www.marulabo.net/category-theory/ 　 今回のセミナーでは、Open-AI Theorem ProverのようないわゆるAIがコンピュータに「推論能力」を与えるのではなく、そもそもコンピュータ自身が、「推論能力」を持っているという立場で議論を進めたいと思っています。 【「セミナーの構成について -- Voevodskyの仕事を考える 」を公開しました 】 https://youtu.be/4SNHi4K-2eA?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのpdfは、こちらからアクセスできます。 https://drive.google.com/file/d/1vza1sCNErB7T1eybCEqU-AFwGBAqw_Dr/view?usp=sharing このトピックのまとめページは、こちらです。ほぼ毎日更新されると思います。 https://www.marulabo.net/d...

【 丸山、証明に失敗する 】 この間紹介した「連続体仮説」にしろ「Feit-Thompson定理」にしても、その意味を説明するのは簡単ではないのですが、今回紹介する「ケプラー予想」の意味は分かりやすいものです。 それは、箱におなじ大きさのボールを詰め込もうとした時、どのようにボールを並べたら、一番たくさんボールを詰め込めるかという問題です。ケプラーは、不規則にではなく規則的にボールを並べると一番高密度にボールを詰めこめると考えました。ある意味もっともだと思います。ただ、そのことを証明できませんでした。 紹介がおくれましたが、ケプラーというのは、あの天文学者のケプラーです。彼が、ボールの箱へのパッキング問題を考え予想を立てたのは 1611年のことでした。日本なら徳川幕府ができた頃です。 ただ、それから 300年たっても問題は解けませんでした。ヒルベルトは、1900年に20世紀の数学が解くべき23の未解決問題のリストを公開するのですが、「ケプラー予想」は、その18番目にランクインしています。それでも問題は解けませんでした。 ケプラーから数えれば400年たった 2014年、ヘイルズがこの問題を解決します。 彼は、不規則なボールの配置のパターンを数え上げ（5,000パターンぐらいあるそうです）、その全てのパターン総当たりで、詰め込みの密度の最小値を線形計画法を使って計算します。線形計画法の100,000個のプログラムが必要だったようです。 もちろん、その計算にはコンピュータが使われるのですが、同時に、彼はその計算が正しいことを検証するためのプログラムを開発します。そのプロジェクトを、flyspec Project といいます。それはGitHubで公開されています。 僕は、昨日、flyspec Project をビルドしようとしました。ところがなんとプロジェクトのビルドに失敗してしまいました。僕は、ケプラー予想の証明に失敗したことになります。いつも一発でビルドが通るとは限らないので、もう少し粘ってもよかったのですが、はやばやと諦めました。 というのも、このプロジェクトのビルドに成功したとしても、そのプログラムの実行（すなわち、ケプラー予想の証明）には、5,000個のCPUを使っても、一時間かかるということが分かったからです。とても、僕のくたびれたMac一台で太刀打ちできる計算...

【 数学者もブラックな冗談を言う 】 2012年、Georges Gonthierは、Coqを用いて、群論のFeit–Thompson 定理の形式的証明に成功しました。 この定理は、1962-1963年にWalter Feit と John Griggs Thompson によって証明された、群論の基本的な定理の一つです。この定理は、「奇数位数の有限単純群は可解である」ことを主張し（「奇数位数定理 = “Odd Order Theorem” とも呼ばれます ）、有限単純群の分類問題で重要な役割を果たしています。 「有限単純群の分類問題」は、Daniel Gorensteinをリーダーとする数学者の集団によって解決され、20世紀の数学の大きな成果の一つと呼ばれています。 ただ、その「証明」は、100人以上の数学者が、50年のあいだに数百の論文誌に発表した、膨大な量の「証明」の総和です。そのページ数は一万ページを超えると言われています。 証明が、あまりに膨大なので、 　「この証明を全部を読んでる数学者は、１人もいない。」 というブラック・ジョークがあるそうです。 でも、数学の証明を行うのに、過去の数学の論文を全部読む必要は、実はないのです。それについては、また別の機会に説明したいと思います。 【 「Feit–Thompson定理の形式的証明」を公開しました。 】 https://youtu.be/Uxtp0N0y3bg?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのpdfは、こちらからアクセスできます。 https://drive.google.com/file/d/1zN_-J2KbwuKs_DEeapY_0P5-rtidnH4B/view?usp=sharing このトピックのまとめページは、こちらです。ほぼ毎日更新されると思います。 https://www.marulabo.net/docs/math-proof/ セミナーへのお申し込みは、こちらからお願いします。 https://math-proof.peatix.com/

【 感慨 -- 思えば遠くに来たもんだ 】 昨日、不思議な感動的な体験をしました。 月末のセミナーに向けて、数学者が証明問題を解くのに、コンピュータを利用し始めていることを紹介しようとしているのですが、どうしても取り上げたいトピックがありました。 一年ほど前、連続体仮説の独立性をコンピュータ上で証明できたという論文が出ていました。彼らは、その証明を GitHubで公開していました。「証明」はコンピュータで実行可能な「プログラム」の形をしているのです。 昨日、それを実行してみたのです。 僕のくたびれた非力なMacは、証明の準備にとりかかりました。メッセージをみると、証明に必要な情報をたくさん集めているのがわかります。一時間ほどかかって、ようやく準備ができましたようです。「証明して」とコマンドを打ち込んだら、15分ほどで、証明が終わりました！ 不思議な気持ちになりました。 確かに、僕が命令して僕のマシンが働いたのですが、僕は「連続体仮説の独立性」を証明したのでしょうか？ 「連続体仮説」というのは、数直線上の 0と1 の間に、何個の点があるのかという問題です。カントールはこの個数についてある仮説を立てたのですが、ついには狂気にいたるまでそれを証明することができませんでした。ヒルベルトは、この問題を 20世紀の数学が解くべき問題の筆頭に掲げました。 ゲーデルは、この仮説が集合論の他の公理とは矛盾しないことを示すことができました。この問題が最終的に解いたのは、コーエンです。彼は、連続体仮説がなりたつ集合論もあれば、それが成り立たない集合論もあることを示すことに成功します。それが「連続体仮説の独立性」証明です。 arXivもGitHubもない時代でした。僕がコーヘンの論文とその準備をしたゲーデルの無矛盾性証明のレクチャーノートを手に入れるのに、田舎にいたせいもあって、3ヶ月かかりました。PCもタブレットもないので、プリンストンの真っ赤な表紙のレクチャーノートをいつも持ち歩いて、ボロボロになりました。 カントール、ヒルベルト、ゲーデル、コーエンが苦闘した問題を、こたつの上の古いMacが、一時間ちょっとで解いたのです！　かつて「連続体仮説」フェチだった僕にとっては、Open-AI の「人工知能」が、数 I レベルの「数学オリンピック」の問題のいくつかをといたことなんかより、はるかに...

【 数学者、コンピュータを使い始める 】 Open-AI Theorem Prover が、どのようなデータを学習してきたかをみてきたのですが、今回紹介する mathlib-train は、特別な役割を果たしています。 量的にも、これまでみてきた訓練用データより、ひとまわり大きいのです。 　miniF2F-curriculum　 327 　synth-ineq               5,600 　mathlib-train          25,000 (25K) 質的にも、mathlib-train は一味違っています。それは、多くの数学の領域をカバーしている、Lean で書かれた数学の定理集（証明付き）です。もちろん、これを作ったのは、人間です。Lean  mathlibは、多くの数学者が参加しているオープンソースのプロジェクトです。 　"Lean mathlib" 　 https://github.com/leanprover-community/mathlib mathlib-train で訓練されたOpen-AI Theorem Proverは、見違えたように賢くなりました。イリヤたちの論文のAppendix E に、三つほどその例が出ています。 なんと、Open-AI Theorem Proverは、学習した mathlib-train とはちがった形で定理の証明を考え出したのです！　素晴らしい！ ただ、話はそれで終わらないのです。 今回のセミナーのタイトルは、「コンピュータ、数学の問題を解き始める」なのですが、それに先行したのは、Lean  mathlib のように、「数学者、コンピュータで数学の問題を解き始める」という動きでした。 一人の天才数学者が、こうした動きを決定づけました。 セミナーの後半では、こうした動きを紹介しようと思います。 【「彼は、何を学習したのか (3) mathlib-train 」を公開しました 】 https://youtu.be/NPlQ9fVc8bQ?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのpdfは、こちらからアクセス...

【 すごい！ でも、すこし違うかも 】　 前回は、Open-AI Theorem Proverが何を学習したかということで、"miniF2F-curriculum" 、"synth-ineq"、"mathlib-train"という三つの「カリキュラム」があることを紹介しました。 今回は 、5,600の訓練用の定理からなる"synth-ineq" を、もう少し見てみようと思います。といっても、僕は、このデータを全て見た訳ではありません。イリヤ達の論文にそのデータの作り方が、Appendix  D. にサンプルが、紹介されています。 サンプルの二つ目に、次のような定理が挙げられています。 　　2a(a - 68) <= a^2 + (a - 68 )^2 (a - 68 ) の '68' という数字は、ランダムに選ばれたものです。それ自体に意味はないと思います。ただ、イリヤ達の論文で、synth-ineq の作り方を見ていると、いったん '68' が選ばれると、次のような命題も、生成されるべき定理の候補になるような気がします。 　　2a(a - 1/68) <= a^2 + (a - 1/68 )^2 　　2a(a - log 68) <= a^2 + (a - log 68 )^2          ・・・ ただ、これらは全て、次のより一般的な定理から、簡単に導かれるものです。 　　2xy <= x^2 + y^2 　（ なぜなら、(x - y)^2 >= 0 から、 x^2 - 2xy + y^2 >= 0 ですから。) この定理の学習だけでは、足りないのでしょうか？ イリヤ達が紹介しているように、不等式型の定理の生成では先行する論文があります。 "INT: AN INEQUALITY BENCHMARK FOR EVALUATING GENERALIZATION IN THEOREM PROVING" https://arxiv.org/pdf/2007.02924.pdf 　 https://github.com/albertqjiang/INT これは、なかなかすごい論文で力作です。GitHub...

【 お勉強は大変だ 】 数学的証明の場合には、ゲームの場合のように、セルフ・プレイで訓練用データをいくらでも提供できるわけではないことを先に見て来ました。 それでは、Open-AI Theorem Proverには、まず最初に、どのような訓練用データが提供されたのでしょうか？ ここでは、それをみていこうと思います。もちろん、このデータを選択し提供したのは、人間です。 Open-AI Theorem Prover に与えられたのは、次の三つの訓練用データです。 　1. miniF2F-curriculum 　2. synth-ineq 　3. mathlib-train 以下、それがどんなものか概略を紹介しましょう。 1. の"miniF2F-curriculum" の主要部分は、数学オリンピックにチャレンジしようとする中高生向けに、LehoczkyとRusczykがつくった問題集 “The Art of Problem Solving” https://www.amazon.co.jp/-/en/Sandor-Lehoczky/dp/0977304566 からの抜粋です。ベンチマークの miniF2Fの試験をいい成績で通るように、人間の手で、327の問題が選ばれています。もちろん、それはLeanの言葉に変換・翻訳されています。 https://github.com/openai/miniF2F/blob/statement_curriculum_learning/lean/src/statement_curriculum_learning/aopsbooks.lean に、全体が公開されていますので、ご覧ください。 2. の"synth-ineq" は、もっと強烈です。 Leanでは「等式」の証明には、便利なtactics があります。以前のショートムービー「Open-AI Theorem Proverが行う証明」 https://youtu.be/BAvCsZFGQKQ?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg で紹介した 問題1, 問題5で利用されていた "linarith" は、そうしたtactic の一つです。 ただ、不等式の証明は、基本的には、代入・変形...

【 セルフ・プレイに代わるもの 】 イリヤ達の論文は、数学的証明をDeep Learningで行う上で、二つの難しさがあるといいます。 一つは、ゲームの場合にはそれぞれの局面で選択できる手は有限個しかないのですが、数学的推論では可能な選択は有限とは限りません。もう一つの問題は、ゲームの場合には非常に有効だった、機械と機械を戦わせて膨大な対戦データを自動的に蓄積して、それを機械の訓練に利用する手法（それを、「セルフ・プレイ」といいます）が使えないことです。 この二つのことから、ゲームでは成功を収めた「強化学習の方法を形式的な数学に、素朴に適用することは成功しそうにない。」といいます。彼らは、この論文では二つ目の「セルフ・プレイ」の問題にフォーカスしています。 「二つ目の問題に取り組む上で基礎となるのは、セルフ・プレイのもっとも重要な役割は、それが教師なし学習のカリキュラムを提供していたという観察である。我々は、それらの代わりに、様々のレベルの難しさからなる補助的な問題群を（証明を要求することなく）提供することを提案する。」 彼らが提案していることは、セルフ・プレイが生成する訓練用データの代わりなるようなデータを提供するということです。 「証明なしでも構わない」と言ってることが気になる人もいると思いますが、それは問題ないと思います。なぜなら、そこで提供されるのは、「証明が存在しない」ような、すなわち「偽」である命題ではなく、正しいことが保障されている問題だけだからです。 数学の証明問題で、「ピタゴラスの定理」を使ったとして、その度に、「ピタゴラスの定理」の証明を繰り返す必要はありません。いったん証明された定理は、その後は、証明なしでも使うことができます。 「これらの補助的な問題の難易度が、十分に多様なものであれば、単純な学習の繰り返しの手順で、だんだんと難しくなる問題のカリキュラムを解くことができることを、我々は経験的に示した。」 大事なことは、「これらの補助的な問題の難易度が、十分に多様なもの」であることです。 それでは、こうした「補助的な問題群」は、どのようにして作られたのでしょうか？ 注目すべきことは、今回のOpen-AI Theorem Proverでは、人間が手動で編集したデータが使われているということだと思います。 「我々の結果は、形式的数学が絶えず継続的に...

【  Deep Learningの到達点と課題  】 イリヤ達の論文 “Formal Mathematics Statement Curriculum Learning” https://arxiv.org/pdf/2202.01344.pdf 　は、Open-AI Theorem Proverの解説としてだけでなく、Deep Learning技術の到達点と課題を率直に述べたものとして、興味深いものです。 彼は、Deep Learning が、数多くの成功にもかかわらず、いまだ成功を収めていない分野があることを指摘します。 「ディープラーニングは、言語・ビジョン・画像生成を含む多くの分野で目覚ましい成功を謳歌してきた。 ディープラーニングがまだそれらの分野と比肩しうる成功を収めていない一つの領域がある。それは、広い見通しとシンボルに基いた推論を必要とするタスクの中にある。」 多くの人は、ディープラーニングの「深く考える能力」の代表として、人間の碁のチャンピオンを破ったAlphaGoのようなものを考えると思います。確かに、それは印象的な出来事でした。ただ、確かに、碁や将棋のような対戦型のゲームには、無敵のAIが存在するのですが、そのことで、機械の推論能力が人間を超えたとは言えないと僕は思います。 「ゲームが対象とするスコープは比較的狭いため、結果として達成される推論能力は制限されている。」 「この点では、インタラクティブな証明アシスタント、すなわち、形式的な数学での定理証明は、取り組むべき興味深いゲームのような領域に見える。」 「形式的な数学の広い応用範囲を考えれば、 （たとえば、数学的な推論の証明を見つける）そこで得られた強力な推論結果は、ゲームでの同等の結果よりも大きな意味がある。それは、 （たとえば、ソフトウェア検証といった）重要な実際の問題にも適用できることを意味する。」 僕は、こうした議論に賛成しています。 【「数学的証明の重要性とその難しさ」を公開しました 】 https://youtu.be/BAvCsZFGQKQ?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのpdfは、こちらからアクセスできます。 https://youtu.be/VjBduTnlFtY?list=PLQIrJ0f9gMcP...

【 誰が証明を行っているのか？】 前回は、Open-AI Theorem Proverがどのような問題を解いているのかを紹介しました。ただ、ある数学の問題が与えられた時、Open-AI Theorem Proverがどのような答えを返すのかは紹介していませんでした。 前回紹介したのは、（自然言語で）普通に与えられた問題を、（数学の言葉で）普通に解いてみただけです。Open-AI Theorem Proverは、これとは違ったスタイルで、数学の問題を解きます。 まず、自然言語で与えられた数学の問題を形式的な数学的な言語に翻訳します。これは、Sequence  to Sequence の変換で、ニューラル・ネットワークにとっては楽勝です。数学の問題は、語彙は専門的ですが数は少なく、文法的にも単純です。シェイクスピアは読めなくても、数学の論文なら読める人は沢山います。 次に、Open-AI Theorem Proverは、こうして形式化された問題を、形式的に証明しようとします。そこで、証明支援の言語 Lean が登場します。Open-AI Theorem Proverは、Leanで形式化された問題としてLeanで問題を証明しようとします。そしてLeanでの証明が成功すれば、それを返します。 　「これが、問題のこたえです。」 Leanは、pCIC（Predicative Calculus of Inductive Constructions）に基づいています。その意味では、LeanはCoqの兄弟言語です。Leanについては、章をあらためて紹介しようと思います。 今回は、前回紹介した問題に対する、Open-AI Theorem Proverの答え、すなわち、Leanによるその証明を紹介します。今回は、そこまでです。 ただ、次のような問題を考えてみましょう。 　「証明問題を解いているのは、 　　ニューラル・ネットワーク gpt-Xなの？ 　　それとも Lean なの？」 これは、なかなか面白い問題です。残念ながら、長くなりそうなので、別の機会に。 【「Open-AI Theorem Proverが行う証明」を公開しました 】 https://youtu.be/BAvCsZFGQKQ?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライド...

【 AIについての二つの見方 】 今年の2月に、Open-AI は、数学オリンピックの問題をニューラル・ネットワークで解くという、とても面白い取り組みの成果を発表しました。 今回のショートムービーは、そのニューラル定理証明システムが、どのような問題を解いて見せたのかの紹介です。以前にも、これらの問題を部分的には紹介していたのですが、今回は、それを実際に自分でも解いてみました。みなさんも、時間があったら、ぜひ、挑戦ください。 コンピュータが、どのような問題を解いたかを知ることは大事なことだと考えています。それは、「どのようにして解いたのか？」とは別のことなのですが（それについては、おいおい説明していきたいと思います）、最新のAI技術が、どのような問題にチャレンジしているかを、わかりやすく知ることができるからです。 人によっては「簡単な問題じゃないか」と思う人も（数学オリンピックの問題が、みな難しいわけではありません）、「さっぱりわからん」という人も（数学苦手の人は、多いです）いると思います。 実際に問題を解いてみれば、その問題が易しいのか難しいのかの判断は、人によって分かれるはずです。それでいいと思います。 ただ、コンピュータが解いた問題を自分が簡単に解いたからといって、「AIは、やはり、大したことができないのだ」と判断するのは早計です。同様に、自分が解けない問題をコンピュータが解いたからといって、「AIは、素晴らしい。なんでもできる。」と考えるのも、どうかと思います。 本当は、両者の極論の、中間ぐらいに真実はありそうです。今回のセミナーでは、そのあたりのことをお話しできればと思っています。 【「Open-AI Theorem Proverが証明したこと」を公開しました 】 https://youtu.be/isV540CPULM?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのpdfは、こちらからアクセスできます。 https://drive.google.com/file/d/1rBccwWov_aODp5u5yOtVS0eRFnN2ZOsx/view?usp=sharing このトピックのまとめページは、こちらです。ほぼ毎日更新されると思います。 https://www.marulabo.net/docs/math-pr...

【 3/26  マルレク「コンピュータ、数学の問題を解き始める」へのお誘い 】　 3月のマルレクは、「コンピュータ、数学の問題を解き始める」をテーマとして、3月26日オンラインで開催します。 AI関係のセミナーは、マルレクでは久しぶりのことです。面白い話が出来ればと思います。 申し込みページはこちらです。https://math-proof.peatix.com/ この2月に、 Open-AI はとても興味深い発表を行いました。彼らは、国際数学オリンピックのいくつかの問題をコンピュータを使って解いて見せたのです。例えば、2000年の数学オリンピックの問題は、こんな感じです。 問題 　 |x - 2| = p とする。 x < 2 の時、x - p = 2 - 2p となることを証明せよ。 証明 　 x < 2 なので、|x - 2| = - (x - 2)である。p = |x - 2| を使えば、x = 2 − p である。結局、x - p = 2− 2p となる。 この例は、高校生の数 I レベルのやさしい問題ですが、こうした問題をコンピュータが解くのは、画期的だと思います。論文には、この例をふくめて6つの例が紹介されています。 （このセミナーのまとめページ https://www.marulabo.net/docs/math-proof/ に、6つの例を紹介しています。） 実際には、コンピュータは、形式的証明を返すのですが、ここで紹介したのは、「非形式的 Informal」な証明です。コンピュータは、Informal ボタンを押すと、こうした「非形式的」証明を返してくれます。形式的証明を非形式的証明へ要約・翻訳できるのも面白いです。 「数学オリンピックの形式的問題（のいくつか）を解く」 "Solving (Some) Formal Math Olympiad Problems" https://openai.com/blog/formal-math/ 　 Deepmindは、数学へのAIの利用について、昨年12月、Natureにこんな論文を発表していました。それは、AIを利用することで人間の数学的直観を導くことができることを示して、数学者に向けてAIも使いみちがあると述べたものでした。 "Advancing mathem...