過去・現在・未来

【 広がるビジョン 】 2017年に亡くなったVoevodskyは、Milner予想、Bloch-Kato予想を解くなど、代数幾何でグロタンディックが進もうとした道で、大きな業績を残した天才数学者です。 彼の最後の仕事は、数学の基礎とコンピュータという二つの世界に関係していました。 前回取り上げた数学での「間違った証明」の問題ですが、彼も、苦い経験がありました。 2000年頃、彼は1993年に自分が発表した論文の重要な補題が間違っていたことに気づきます。でも、その頃には、その論文は広く出回っていて、多くの数学者がその証明を「信じて」いました。彼が、その間違った補題なしでも、論文の結論が正しいことを証明できたのは、2006年になってからでした。 別のこともありました。1998年に共著で彼が発表した論文の証明に対して「正しくない」という批判が出されるのです。結論的には、彼は、正しかったのですが、彼が、最終的に、自分が正しいことを確信できたのは、2013年になってからでした。 Voevodskyは、考えます。「数学が、累積的（accumulative）な性格を持つのなら、もしも、そこに誤りが紛れ込むと、それも、累積する可能性がある。」と。 こうした問題に対する、Veovodskyのとった対応はラジカルで驚くべきものでした。 彼は、数学をその基礎から改めて考えなおしたのです。そして、集合論に変わる新しい数学の基礎づけ Univalent Foundationを構築します。 さらに、彼は、数学の証明に、コンピュータを使うべきだと主張した最初の数学者となりました。そして、そのためのコンピュータによる証明支援システムのライブラリーUniMthを開発しました。 彼の考えたことを、少し長くなりますが、彼のインタビュー記事から引用します。 彼は、「数学は今、危機的状況、いや、2つの危機に瀕している」といいます。 「第一は、それは、「純粋数学」と「応用数学」の分離に関連しています。 遅かれ早かれ、実用性のないことに従事している人たちに、なぜ社会がお金を払わなければならないのかという疑問が生じるのは明らかでした。 第二は、あまり明らかではありませんが、純粋数学の複雑さに関連しています。 遅かれ早かれ、論文が複雑すぎて詳細な検証ができなくなり、発見されないエラーが蓄積される過程が始まるという

【 数学者も証明を間違えることがあるということ 】 数学的知には、人間の認識によって獲得されたものとしては、独特の性質があります。 それは、いったん数学的に「真」であることが証明された定理は、時代が変わっても場所が変わっても、ずっと「真」のままであり続けることです。 そうして獲得された知は、個人というよりは人類の知として蓄積されていきます。それを数学的知の「累積性」といいます。 「フェルマーの定理」を証明したワイルズは、自分を「巨人の肩の上の小人」に喩えたのですが、それは彼の謙遜であると同時に、数学的知の体系が「累積的」であることを彼がはっきりと自覚していることを示しています。 それでは、 「数学的知の累積性」は、どのように保証されるのでしょうか？ ピタゴラスの「教団」は、いくつかの発見を「秘教」にしていたらしいのですが、ピタゴラスの定理を使うのに、我々はその「証明」を自分で繰り返し「再発見」する必要はありません。 もちろん、ピタゴラスの定理を使うたびに、ピタゴラスの遺産継承者に使用料を支払う必要もありません。 数学では、「数学的知の共有」は、数学という学問自体の前提と言っていいものです。 そういう意味では、コンピュータの世界でオープンソースのムーブメントが大きな影響力を獲得するはるか以前から、数学の世界はオープンソースの世界だったのです。 ただ、「情報の共有」が、「数学的知の累積性」を保証するとは限りません。「数学的知の累積性」にとって、一番重要なことは、その「数学的知」が数学的に正しいことです。 しかし、数学的正しさを証明する「数学的証明」は、現状では、いくつかの問題を抱えています。 一つには、数学者が正しいと思って提出した「証明」が、正しいものではない場合があるということです。 「フェルマーの定理」は、最終的には、1995年のAndrew Wilesの論文によって証明されたのですが、フェルマー自身は、この定理を証明出来たと信じていました。その「証明」は残っていませんが、それが誤った「証明」であったのは確かです。 Wiles自身も、95年の論文以前に一度、「フェルマーの定理を証明した」という発表を行うが、誤りが見つかり、それを撤回しています。 世紀の難問である「リーマン予想」は、何度か「証明」が発表されています。今までのところ、それらは誤った「証明」でした。 証

  【 マルレク「ことばと意味の構成性について」講演ビデオ公開しました 】 昨年の12月24日に開催した、マルレク「ことばと意味の構成性について」の講演資料と講演ビデオを公開しました。あわせてこのセミナーのまとめページ  https://www.marulabo.net/docs/discocat/  も更新しました。ご利用ください。 このセミナーは、現在ビデオ公開中の「AIは意味をどのように扱っているのか？-- ChatGPTの不思議」 https://www.marulabo.net/docs/meaning/   の内容を理論的に補うものです。 現在の「大規模言語モデル」の中核技術は、「ことばと意味」をコンピュータ上で扱う技術にあるのですが、その背景にどのような理論的問題があるかに興味ある方は、ぜひ、ご覧ください。 同時に、このセミナーは、サブタイトルの「カテゴリー論と意味の形式的理論」が示すように、先日の投稿「カテゴリー論の時代始まる」で紹介した数理科学へのカテゴリー論の応用の紹介になっています。　 第一部では、カテゴリー論の創世記の重要な達成であるローヴェールのFunctorial Semanticsを紹介しています。 第三部は、言語学と意味の理論へのカテゴリー論的アプローチである、Discocat理論の紹介です。 4月のマルレクでは、この分野の最新の研究動向を紹介する「意味の分散表現技術の現在」というセミナーを開催しようと思っています。ご期待ください。 今回公開したセミナーのテーマの一つである、「構成性 compositionality」という概念は、カテゴリー論の基本的な特徴と考えられているのですが、あまり見慣れないものかもしれません。 ただ、この「構成的 compositional」という概念は、大規模言語モデルを考える上で、重要な意味を持っています。 昨年の10月に、Google と OpenAIは、ともに、「大規模言語モデル」ではモデルの規模拡大だけでは AIの能力は伸び悩むという論文を発表します。 OpenAIは、"Scaling Laws for Reward Model Overoptimization" という論文を発表します。それは彼らが同年の4月に発表していた "Training language mo

【 カテゴリー論の時代始まる 】 20世紀を通じて、数学・物理を中心とする数理科学は、大きな発展を遂げました。それは、内部に多くの新しい研究領域を発生させながら、それぞれの領域は相互に越境し、さらにその領域を拡大し続けました。 前回見た、「計算」＝「証明」＝「プログラム」という認識も、新しい領域を巻き込み、長い時間をかけて獲得された、そうした認識の一例です。 21世紀になって、こうして拡大した数理科学の全体像を統一的に把握しようという探究がうまれてきます。 数理科学の専門化した諸領域の到達点を概観するのは、必ずしも容易ではないのですが、やがて、それらの間に驚くべき類似性が存在するという認識が生まれます。 今回のセッションで紹介する John Baezらの “A Rosetta Stone”論文は、数理科学の統一的把握の試みとして、もっとも成功した、もっとも影響力のあったものの一つです。 彼の認識の飛躍は、数学的には、数理科学の基礎にカテゴリー論をおくことで可能になりました。 1970年代、ペンローズは、ファインマン・ダイアグラムの一般化が、時空間の理解を改めることにつながるかもしれないことに気づきます。1980年代には、量子物理学とトポロジーとの間に、強力な類似性があることが明らかになっていきます。 弦理論では、この類似性を利用して、通常の場の量子論のファインマン・ダイアグラムを2次元のコボルディズムに置き換えて、時間の経過とともに弦が辿る世界のシートを表現します。 演算子とコボルディズムの類似性は、ループ量子重力や、より純粋に数学的な分野である「トポロジカル場の量子論」においても重要な役割をはたします。 バエズは、彼は、このアナロジーをさらに推し進めます。物理学とトポロジーだけでなく、論理学と計算理論もリストに加えて、数理科学の「パラレル・コーパス」を作成するのです！ 導きの糸となったのは、カテゴリー論の基本的な構成要素である、「オブジェクト」と「モルフィズム」の対応物を、これらの理論に中に見つけることでした。　 　・物理学でオブジェクトに対応するのは「システム」で、モルフィズムに対応するのは、「プロセス」。 　・トポロジーでオブジェクトに対応するのは「多様体」、モルフィズムに対応するのは「cobordism」。 　・論理学でオブジェクトに対応するのは「命題」、モ

【 当事者のIT技術者に見えにくい「リンク」】 先に、”Proof as Program プログラムとしての証明” という認識が、Curry-Howard対応の発見や従属型理論の登場の中で、生まれてきたことを述べてきました。 それは、論理的＝数学的証明は機械のプログラムで実行できるということ、ひるがえって言えば、機械は論理的＝数学的推論能力を持つという認識に他なりません。 この認識は、人工知能論にとって本質的に重要な認識であると、僕は考えています。 このセッションでは、改めて、「計算」＝「証明」＝「プログラム」という認識がどのように形成されてきたのかを、 振り返りたいと思います。 「計算」「証明」「プログラム」という三つの言葉は、もともと別の意味を持っています。それは今でも同じです。そして それぞれがそれぞれの歴史を持っています。 この三つの言葉の中で、「計算」の起源が一番古いものです。4000年以上前の古代バビロニアでは、2の平方根の値も知っていたし、ピタゴラスの定理で直角三角形の斜辺の長さを計算する「計算表」も持っていたといいます。人間は、具体的な「計算」を通じて数学の世界の扉を開きました。 「証明」の概念の起源は、2300年前のユークリッドに帰してもいいと思います。古代ギリシャ人は、具体的な数の「計算」とは異なる数学の世界があることに気づきました。プラトンは彼のアカデミアの門に、「幾何学を知らざるものこの門入るべからず」と掲げたと言われています。彼らにとって、「数学的証明」は「真理」に到達する、重要な方法だと認識されていたと思います。残念なことに、ギリシャ数学の伝統は中世ヨーロッパでは途絶します。 この中で、「プログラム」という概念が一番新しいものです。その起源は、コンピュータが登場した1950年代を遡ることはないのは明らかですので。 このセッションは、機械の能力を人間がどう認識してきたかを、「計算」「証明」「プログラム」という三つの概念の関係の認識の歴史をメイン・ストーリーにして述べたものです。 さきに、概略を述べておきましょう。（以前のセッションと内容的には重なっています。） まず、「計算」と「証明」が、本質的には同じものであるという認識が生まれます。1930年代のことです。 それから40年ほど経って、「プログラム」は「証明」とみなせるという認識が生まれま

【 「証明支援システム」-- 人間と機械の「協働」の始まり 】 Dependent Type Theory 「従属型理論」の基本が出来上がるのは、1980年代です。その中心人物は、マーティン・レフです。 彼の理論が与えた影響を、二つほど見ておきたいと思います。 第一に、この理論は、21世紀になって急速に実装が進んだ Coq, Agda, Lean 等の「証明支援システム」に理論的基礎を提供しました。 「証明支援システム」というのは、“Proof as Program” という、証明をコンピュータのプログラムとして実行するというアイデアを、現実に実行可能にしたシステムのことです。 「証明支援システム」は、コンピュータが自動的に数学の問題の証明を与える「自動証明システム」ではないことに注意してください。それは、あくまでも人間が行う数学の証明を、コンピュータが支援するというシステムです。 ただ、「証明支援システム」で、証明を行なっていると、奇妙な感覚にとらわれることがあります。 　「僕は、コンピュータで証明を行なっている。 　　証明をしているのは僕だ。 　　コンピュータが、それを助けてくれている。」 　「でも、待てよ ... 」 　「本当は、証明をしているのはコンピュータで、 　　それを支援しているのが、僕なんじゃないか？」 以前は、「証明支援システム」を利用して「証明」を行う人は少数だったもので、こうした「主客逆転」の「感覚」を伝えることは、少し難しかったのですが、今年に入って状況は大きく変わったと思います。 その変化とは、いうまでもなく、GitHub Copilot が登場して、それを圧倒的に多くのプログラマが使い始めて、機械とのペア・プログラミングの経験が急速に拡大していることです。 まだ、「ChatGPTが、プログラムを全部書いてくれるので、人間のプログラマはいらなくなる」という議論も時々見かけるのですが、実際に使ってみた人は、プログラマの仕事は楽になるけど、形は変わってもやっぱり人間が必要なんだということに、いつか気づくと思います。GitHub Copilot は、基本的に、人間主導の「機械と人間の協働」なのです。 それは「大規模言語モデル」ベースの「プログラム開発支援システム」の限界だと思います。人間の役割が必要だということは、人間にとって悪いことではありま

【 「証明」＝「計算」＝「プログラム」】 数学と計算科学の接点を振り返っています。 ゲーデル、チャーチ、チューリングの「証明可能性」は「計算可能性」に等しいという発見から40年たった1970年代、数学と計算科学の接点で注目すべき二つの動きがありました。 一つは、計算機科学の側から生まれた、具体的なプログラムの分析を通じて、計算機科学の数学的基礎づけを目指す動きです。残念ながら、この「形式手法」と呼ばれる意欲的なムーブメントは。ITの世界では広く受け入れられることなく挫折します。 もう一つは、論理学＝数学の側から生まれた動きです。その代表的な成果は、「Curry-Howard対応」の発見と、それに基づくマーティン・レフの「従属型理論」の成立です。 今回のセッションでは、「Curry-Howard対応」の発見を取り上げます。 Curry-HowardのCurryは、関数型言語Haskellにその名を残しているCurry Haskell その人です。既に1934年に、Haskell Curryは、型付きラムダ計算の関数の型を示す矢印 → と、論理式“A → B” の中に出てくる含意を意味する矢印 → との間に、対応関係があることに気づいていました。 具体的には、「A → B が成り立ち、かつ、Aが成り立つなら、Bが成り立つ」という有名な「三段論法」の推論ルールと、「f が A → B という型を持ち、a がAという型を持つなら、f(a) は型 B を持つ」という型付きラムダ計算での型の計算ルールが、よく似ていることに気がついていました。 Howardは、このCurryの発見を、マーティン・レフらと共に、さらに深く考えました。 論理式 A → B が、 A → B という関数と同じ型を持つと考えられるのなら、他の論理式も、型を持つと考えることができるのでは？　例えば、論理式 A ∨ B は、型 A ∨ B を、論理式 A ∧ B は、型 A ∧ B を持つと考えることはできないか？ そして、この論理式（命題：Proposition）を型とみなすアイデアは、うまく機能するのです。こうした考えを、"Proposition as Type"と呼びます。 もう一つの飛躍は、命題が型Pを持つとしたとき、型Pの項pにあたるものが、命題Pの証明と考えることができ

【 3/31 マルレク「人工知能と数学」へのお誘い 】　 3月31日 19:00からオンラインで「人工知能と数学」というタイトルでセミナーを開催します。 今日の「人工知能」は、その「言語能力」で、画期的な進歩を遂げています。 ある言語の文を他の言語に「翻訳」すること、言語を問わず膨大な文字データから「関連する」データをを見つけ出すこと、長い文章を短い文章に「要約」すること、ある話題に対して関連する話題を提供して「対話」を続けること。 こうした能力は、「大規模言語モデル」と呼ばれる人工知能技術の登場とその成長によって初めて可能になりました。その成長の秘密の鍵は、この技術が「ことばの意味」を、コンピュータ上で表現する方法を見つけたことにあります。 イメージの認識なら、イメージをピクセルの集まりとしてコンピュータ上で表現することは容易です。ただ、「ことばの意味」を、コンピュータの上で表現せよといわれたら、みなさんはどんな方法をイメージしますか？　 Googleの検索は、膨大なネット上の文字データから、基本的には特定の「文字列」を探すものです。「意味」を「検索」しているわけではありません。「犬」の検索と「dog」の検索は、文字列が異なりますので、異なる検索です。 「大規模言語モデル」では、「意味」がコンピュータ上に表現されています。この「意味の表現」では、「意味が同じ」ことだけでなく「意味が近い」ことが表現できます。「意味の近さ」が表現できるということは、実践的にはとても大事です。 「翻訳」でしたら「意味が同じ」ことが重要です。話題の「関連性」を見つけるとか「要約」のケースでは「意味が近い」ことがポイントになります。こうした判断をコンピュータが自由に行えるようになったことが、コンピュータの「言語能力」の飛躍をもたらしました。それらは、「大規模言語モデル」が獲得した「意味の表現」のの力によるものです。 「意味の表現」については、現在公開中の次のページを参照ください。 　「AIは意味をどのように扱っているのか？ -- ChatGPT の不思議」 https://www.marulabo.net/docs/meaning/ こうした発展は素晴らしいものです。ただ、問題は、その先にあるのです。 「大規模言語モデル」的アプローチには、大きな弱点があります。それは、こうしたアプロー

【「AIは意味をどのように扱っているのか？」講演ビデオ公開しました 】 1月28日に開催したマルレク 「AIは意味をどのように扱っているのか？ -- ChatGPTの不思議」の講演ビデオと講演資料を公開しました。 ここでの「AI」は、基本的には、Googleニューラル機械翻訳に始まり、BERT、GPT-3、ChatGPTへと続く、現在の「大規模言語モデル」のことを指しています。 今回のセミナーは、「大規模言語モデル」がどのように「意味」を扱っているのという問題にフォーカスしたものです。なぜなら、 「人工知能」技術の現在の飛躍の最大の秘密は、「意味」の扱いにあるからです。 なぜ、大規模言語モデルがどのように「意味」を扱っているのかという問題が、重要なのでしょうか？ それに答えるのは比較的容易です。 人間は、自然言語を扱う理論をいろいろ作ってきたのですが、それに基づいて実際のコンピュータ上で、意味を含んだ自然言語を扱うシステムを実装することには、なかなか成功しませんでした。 大規模言語モデルが重要なのは、それがコンピュータ上で自然言語の意味を扱うことに成功した、事実上最初の、そして現状では唯一の実装されたモデルだからです。 大規模言語モデルの出発点となったのは、「語の意味の多次元ベクトルによる表現」でした。それを「意味の分散表現」といいます。 今回のセミナーの、Part 3「意味の分散表現の登場」、Part 4「大規模言語モデルの成立 -- 意味の分散表現論の発展 」という構成は、今回のセミナーの目的の一つが、大規模言語モデルの成功を意味の表現から跡づけようとしていることを示しています。 Part 2「意味理解への様々なアプローチ」では、大規模言語モデル以外の、意味理解のアプローチを紹介しようと思います。 ただ、「意味の表現」をめぐる探究は、現在の大規模言語モデルで完成したわけではありません。「意味表現」論のさらなる発展に興味がある方は、「 文と意味の構成性Compositionalityから問題を整理する」という節に注目ください。こちらのショート・ムービーからもアクセスできます。 https://youtu.be/Jh0hGq4kuH0?list=PLQIrJ0f9gMcMl-rOnfK6S5EPXazITzFeK ---------------------

 【 人間の力が、機械の力にみえること -- 「ChatGPTの不思議」ビデオ公開 】　 「人間のフィードバック」に全面的に依存するChatGPTのアプローチは、「機械の思考は可能か？」というTuringの問いかけ以来の、機械の自律的な「知能」を追求する人工知能研究からは、「逸脱」したものです。 ただ、「逸脱」が悪いこととは限りません。なぜなら、そうした動きをドライブしているのは、基本的には人間の能力の再評価だと、考えることができるからです。 問題は、こうした人間の力が、機械の力として現れて見えることです。 機械の知能に対する、人間の知能の最初のささやかな「反乱」は、こうして、皮肉なことに、機械の知能の台頭として意識されることになります。 いつか、「人工知能と人間」というセミナーをやりたいと思っています。 ----------------------------- マルレク＋MaruLaboでは、開催したセミナーの様子を、ビデオで公開しています。 今回は、1月14日に開催した、マルレク「なぜ？で考える  ChatGPT の不思議」のセミナー・ビデオの公開です。ご利用ください。 ----------------------------- ChatGPT 試してみましたか？なかなか驚きです。今までのAI技術と一味違います。 いろいろ不思議なことに気がつきます。 第一。なぜ、こんなになめらかに賢く、人間と対話できるのでしょうか？ 第二。なぜ、こんなにも賢く見えるのに、平気で間違ったことを言うのでしょう？ 今回のセミナーは、主要にこの二つの「なぜ？」に答えようとしたものです。 「第 1 章 　ChatGPTの対話サンプル」では、ChatGPTの素晴らしい対話能力を示す例と、その反対に、全くの嘘を繰り返すひどい例の二つのタイプの対話サンプルを紹介します。 「第 2 章 　ChatGPTの方法」では、「対話のために最適化された言語モデル」であるChatGPTの最大の特徴である、「人間のフィードバックからの強化学習」という方法の概要を紹介します。 「第 3 章 　ChatGPTの教育環境」は、この「人間のフィードバックからの強化学習」という方法がどのようなものであるかを、彼 ChatGPTが受けた教育を具体的に振り返ることを通じて深掘りします。 「第 4 章 　ChatGPT

【「数学観」が技術を動かす -- 可哀想な数学 】 前回は、数学の基礎と計算機科学を直接結びつける重要な数学的発見が、1930~40年代にあったものの、肝心のコンピュータは、存在していなかったというという話をしました。今回はその後の時代の話です。 　【 20世紀後半での数学と計算機科学の接点 -- 「形式手法」と「従属型理論」】 20世紀の後半コンピュータが登場し、1960年代にはその利用が急速に拡大する中で、数学と計算機科学の接点を探ろうという研究は活発になります。 1970年代には、二つの研究の流れが独立に生まれます。　 一つは、計算機科学の側から生まれた、具体的なプログラムの分析を通じて、計算機科学の数学的基礎づけを目指す動きです。「形式手法」と呼ばれています。 もう一つは、論理学＝数学の側から生まれた、新しい「型の理論」である「従属的型理論」を構築して、プログラムとその実行の数学的特徴を捉えようとする動きです。 前者の「形式手法」の代表はホーアやダイクストラです。彼らは、代入文やif文、シーケンシャルな実行や繰り返しのWhile文といった具体的なプログラムの構成と論理との関係を研究しました。 後者の「従属的型理論」の代表は、ハワードやマーチン・レフです。彼らは、「型の理論」を作り上げ、抽象的ですが、プログラムの実行は、ある定理の証明に他ならないという認識にたどり着きました。 両者のアプローチは異なっていましたが、「プログラムと論理」という問題意識は共通のものでした。ただ、 20世紀の段階では、「プログラムと論理」という問題を扱うには、両者共に、いろいろな困難がありました。 論理学＝数学からのアプローチではある「従属型理論」は、現実のコンピュータ技術や具体的なプログラム言語との接点は明確ではありませんでした。そのスキマを埋めるのには、実際には、前回見たように 30年から40年の時間が必要でした。 計算機科学からのアプローチでは、論理の多様な性質への理解を欠いていました。実践的には、彼らの理論を実行する強力な「証明マシン」は存在しませんでした。ただ、それ以上の「障壁」があったように、僕は感じています。それが、今回のセッションの一つのテーマです。 今回のセッションでは、ホーア、ダイクストラ、ランポートらの「形式手法」の登場と挫折を取り上げます。 　　【 20世紀

【 数学の基礎と型の理論と計算機科学 】 今回のセミナーのテーマは、「人工知能と数学」ですが、このセッションでは、少し視点を変えて、もう少し広く「計算機科学と数学」の関係を考えてみようと思います。「計算機科学」と「数学の基礎」の関係が一つのテーマです。 数学の知識は、科学と技術のほとんどの分野で広く利用されています。ITの世界でも、数学の応用のスタイルは基本的には同じです。ただ、IT技術者が「数学の基礎」を意識すること -- 数学を利用・応用するだけでなく、なぜそれが可能なのかを考えることは、あまりないように思います。それは、IT技術者だけでなく、他の科学や技術の他の分野でも、数学との「距離感」は、基本的には同じかもしれません。 ただ、「人工知能」が日常的な話題になる今、数学の基礎をめぐる議論は、新しい形で甦りつつあります。 なぜなら、20世紀の「数学の基礎」をめぐる最初で最大の発見は、1930年代に行われた「論理的・数学的証明可能性は、計算可能性と等しい」という発見でした。それは、「チャーチ＝チューリングのテーゼ」という定式化を経て、「（機械によって）計算可能なもの は、証明可能である」という性質を明確に数学的に定式化することに成功します。 「（機械によって）」と括弧を付けたのには、理由があります。それは、この発見がなされた当時、「計算する機械」コンピュータは、まだ存在しなかったからです。 現代の「人工知能」をめぐる中心的な関心は、「計算機が計算可能な「知能」は、どのようなものか」という問いにあります。ただ、こうした問いに答えるのは、「応用数学」の知識ではなく、「数学の基礎」についての知識なのです。 今回のセッションでは、「数学の基礎」と「計算機科学」を結びつける「繋ぎ手」の領域として、「型の理論」に注意を喚起しています。この分野の重要性については、今回のセミナーでも説明していきたいと思います。 ただ、「数学の基礎」と「計算機科学」の距離は、想像以上に「遠い」ことも事実です。それには、いくつかの要因があります。 まず、「数学の基礎」の分野での基本的発見が、1930年代と、コンピュータのなかった遠い昔の出来事だったことが、一つの要因です。今から、90年前ですもの。ただ、科学的知識は、人間と違って経年劣化するものではありません。 もう一つには、この発見の口火を切ったの

【 GitHubがChatGPTを救う (2) 】 　【 ChatGPTの実装の特徴 】 ChatGPTは、 「人間のフィードバックからの強化学習」”Reinforcement Learning from Human Feedback (RLHF)” と呼ばれる手法に基づいて、訓練されています。 それは、Turingの「機械の思考は可能か？」という問いに始まる、基本的には機械の自律的な思考を追求する、従来の「人工知能」へのアプローチとは、異なるものです。 この手法は、ChatGPTのプロトタイプであるInstructGPTで導入されたものです。 　【 ChatGPTは成長する「子供時代」の彼は、何を学んだのか？】 なぜ、「人間のフィードバックからの強化学習」と呼ばれるのかは、ChatGPTがどのようなデータでどのような訓練を受けてきたのかを見ればわかります。 まず、「子供時代」のChatGPTが何を学んだのかを見ていきましょう。（「子供時代」という言い方が変に思われるかもしれませんが、ChatGPTも「成長」します。） 機械翻訳では、同じ意味をもつ二つの言語のペアのサンプルの集まり「パラレル・コーパス」が学習すべきデータでしたが、「会話」のスキルを学ぶべき彼(ChatGPT:Optimizing Language Models for Dialogue )に与えられたのは、「質問」と「答え」のペアからなる会話のサンプルです。 　【 質問に、ことばで答えることを人間から学ぶ 】 OpenAIは、彼 ChatGPTの教育のために、「質問」と「答え」からなる沢山のペア・データPromptを、人を雇ってつくらせました。雇われた人間は、Labelerと言われています。 彼 ChatGPTにことばを教えた「母」は、このLabeler です。彼がことばを操るのは、「子供時代」に人間(Labeler)が書いたことばを学んだからです。機械は、真似するのは得意ですから。 もしも、質問と歌のペアで訓練されたら、きっと彼女 ChanteGPTは、質問に対して歌い出したはずです。 　【 会話の評価は、人間が与える】 「子供時代」のChatGPTの受けた教育で最も重要なものは、会話の「評価」です。 その「評価」は「母」であるLabeler が与えます。人間が、評価を与えています。その評

 【 GitHubがChatGPTを救う (1) 】 今回のセッションでは、GitHubがChatGPTを救うかもしれないという話をしようと思います。ChatGPT的アプローチの抱えている基本的弱点のいくつかを、GitHubの利用によって補完することができるかもしれないという話です。 少し長くなりそうなので、2回に話を分けたいと思います。 最初にお断りしたいのは、僕はこうしたアプローチGitHub + ChatGPT = GitHub Copilotと考えていいのですが、そうした動きを紹介するのは、それらに諸手を挙げて積極的に評価しているからではありません。 ただ、今、何が起きているのか、なぜそうしたことが可能なのか、その背景を正確に理解する必要があるのだと考えています。 その上で、各人が考えることが必要なのです。 　【 僕の基本的立場 】 今回のセミナーのテーマは、「人工知能と数学」です、現代の大規模言語モデルベースの「人工知能」技術には、数学的な能力が欠如しているというのが基本的な問題意識です。 それでは、「人工知能とプログラミング」という問題については、どうなのでしょうか？ 現在の「人工知能」にプログラムを書く能力があるのかという問題に関して言えば、そんな能力はまだないと僕は考えています。なぜなら、プログラムを書く能力は、本質的には数学的能力だと考えているからです。 　【 一つ目の誤解 】 ChatGPTの登場を見て、「人工知能」技術が新しい段階に順調に発展したきたと考えている人は多いと思います。でも、それは誤解だと思います。 確かに、「人工知能」技術の新しい段階への飛躍を目指して、OpenAIは「人工知能」による数学の問題の証明に、Googleは「人工知能」によるプログラムの生成に、果敢に取り組みます。ただ、この二つのプロジェクトは2022年には失敗します。 ChatGPTは、こうした挫折の中で、一時的な「路線転換」として生まれたものだと僕は考えています。 　【 OpenAIの数学への挑戦 】 OpenAIの “Theorem Prover” プロジェクトでの数学の問題への挑戦と挫折については、マルレク「コンピュータ、数学の問題を解き始める」をご覧ください。  https://www.marulabo.net/docs/math-proof/　 原論文は、

【 「RNNとLSTMの基礎」ページ、全面的に書き換えました 】 MaruLaboの「RNNとLSTMの基礎」ページ、ビデオを中心として、全面的に書き換えました。ご利用ください。 https://www.marulabo.net/docs/20170222-marulec05/ ChatGPTをはじめとして、現代の大規模言語モデルへの関心が高まっています。これらの実装の基礎にあるのは、RNN/LSTM技術です。ぜひ、現代の「人工知能」の基本技術であるRNN/LSTMを学んでほしいと思っています。 ビデオは、2017年の2月22日に Microsoft さんの会場で行われたマルレク「RNNとLSTMの基礎」をcrash academy さんが収録したもので、ctash academyさんからビデオの提供を受けました。いまから、ちょうど6年前のコンテンツですが、内容は古くなっていないと思います。（多分） -------------------------------------------- ● Part I  「RNNの驚くべき能力について」　 講演ビデオは、こちらからアクセスできます。 https://youtu.be/lrbo6NPmvb4?list=PLQIrJ0f9gMcPo88QwSeCvc-eULderGaF4 講演資料は、こちらからダウンロードできます。 https://drive.google.com/file/d/1HT4Xl4YJtKNXHs4Vn7Utv875YJziDcxm/view?usp=sharing   ● Part II   「RNNとは何か?」 講演ビデオは、こちらからアクセスできます。 https://youtu.be/t53y-03XhIU?list=PLQIrJ0f9gMcPo88QwSeCvc-eULderGaF4 講演資料は、こちらからダウンロードできます。 https://drive.google.com/file/d/1H_Cafp5VD-9c8o-n35K9NGR-bZUn775z/view?usp=sharing ● Part III    「LSTMの基礎」 講演ビデオは、こちらからアクセスできます。 https://youtu.be/V1iUMPxIY3E?list=PLQIrJ0f9gMcPo88QwSeCv