マルレク「コンピュータ、数学の問題を解き始める」へのお誘い

【 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 mathematics by guiding human intuition with AI "　https://www.nature.com/articles/s41586-021-04086-x

今回のOpen-AIの発表は、そうした関心と方法の延長線上にあるものだと思います。

【セミナーで伝えたいこと】

セミナーでは、まず、Open-AI / Deepmind によるこうした動きを紹介しようと思います。それは、現在のAI技術の到達点を知る上で、重要なことだと思います。

ただ、今回のセミナーで伝えたいことは、もう一つあります。それは、こうした「成果」を、「ニューラル・ネットワーク」や「ディープ・ラーニング」、一般に AI 技術と言われるものの「成果」と単純に見做すべきではないということです。

丸山は、コンピュータ・プログラムが、もともと「論理=数学的推論」を行う能力を持っていると考えています。それは、いわゆるAI技術に基づいて「論理＝数学的推論」を実現しようというのとは異なる視点です。詳しくはセミナーで。