人工知能と数学

機械は推論する

僕は、人間の様々な認識能力の中で、数学的な認識能力に一番興味があります。

自然の認識の変化でも、科学と技術の発展でも、それらの変化の背後にある一番大きな推進力であり基礎にもなっているのは、数学的な認識だと考えています。

人間の認識について少し単純化した議論だし、いろいろ異論は多いと思いますが、僕は、人間の知能の中核は「数学する能力」だと考えています。

ただ、現在主流の「人工知能」技術は、GPT-3.5を使ったTheorem Proverの失敗の総括で、Ilyaが述べているように、たとえ高校生レベルの問題でも数学の問題を解くことには全く手が出ないのです。

それでは、機械に数学的能力を期待するのは、難しいのでしょうか? 大規模言語モデルの上に数学的能力を構築するのが難しいからといって、まったくそうではないのです。

機械には、そうした回り道をせずとも、直接に、自分の力だけで、論理的・数学的に正しい推論を行う能力を持っているのです。

現在の「人工知能」ブームの中で、多くの人はそのことを見落としているように感じています。

マルレク 「人工知能と数学」へのお誘い

( slide-pdf blog )

セミナーへのお申し込みページはこちら

セミナーに向けたblog

第一部 大規模言語モデルと数学

なぜ、大規模言語モデルは、数学が苦手なのか?

( slide-pdf blog )

大規模言語モデルとパラレル・コーパスと言語学習

( slide-pdf blog 「パラレル・コーパスを使った言語学習技術、日本が先取りしていたかもしれないこと」)

言語の習得と数学の学習

( slide-pdf blog )

ニューラル・ネットワークは モノマネの天才

( slide-pdf blog )

GitHubがChatGPTを救う (1)

( slide-pdf blog )

GitHubがChatGPTを救う (2)

( slide-pdf blog )

第二部 20世紀:数学の基礎と計算科学

数学の基礎と型の理論と計算機科学

( slide-pdf blog:「数学の基礎と型の理論と計算機科学」)

「数学観」が技術を動かす

( slide-pdf blog:「「数学観」が技術を動かす -- 可哀想な数学」)

Curry-Howard対応の発見

( slide-pdf blog:「「証明」=「計算」=「プログラム」」)

従属型理論の登場

( slide-pdf blog:「「証明支援システム」-- 人間と機械の「協働」の始まり」)

Proof as Program

( slide-pdf blog:「当事者のIT技術者に見えにくい「リンク」」)

第三部 21世紀:数学の基礎と計算科学の新しい動向

Rosetta Stone、再び

( slide-pdf blog:「カテゴリー論の時代始まる」)

21世紀 数学的証明での「形式的証明」の拡大

( slide-pdf blog:「数学者も証明を間違えることがあるということ」)

Univalent FoundationとUniMath

( slide-pdf blog:「広がるビジョン」)

参考資料

「ChatGPTと大規模言語モデル」関連ページ

「プログラム と論理」関連ページ