今回は、3月2日の「Nature」 Vol.615に出た以下の記事について、興味を感じた部分を中心に解説したいと思います。
“How Will AI Change mathematics” （和訳：AIが数学をどう変えるのか）
数学の世界では、AIによる自動化は単なる計算を遥かに超えている現状です。
これまでの数学AI
これまでに数学に使われたAIは大まかに２通りあります。
１）ルールベースのアプローチ（「古き良きAI」）
ここでは、ロジックや計算のルールをコードの中に組み込みます。コンピュータはそのルールに従い、インプットされた数値に対して操作します。
出力がぶれない、理解できるので、ルールの改善がしやすいです。
早くに成功したAIは「Lean」です。数学の問題を解く際に、数学者に、最も詳細な部分を含んで、各ステップを「強制的に」書き出させます。さらに、各ステップが矛盾していない、間違っていないことをチェックします。
２年前に、Leanを用いて、これまでに証明を悩んでいた重要な問題を証明することができた上で、Leanにその証明が正しいということを確認させてもらえたのです。数学者は互いの仕事を疑いますが、Leanが「正しい」というなら、受け入れられることを意味します。
このように、leanのようなAIは、”proof assistant”（照明の助手）として機能し、それによって、数学者たちの間の関係改善に寄与します。
２）ニューラルネットワークのアプローチ
大量なデータ（例：数学の教科書）を学習することで目的にあった予測などができます。
統計的な推測を行うので、予期せぬ、理解しづらい出力を行うこともあります（ブラックボックス問題）。
Googleが開発した「Minerva」（チャットボット型AI）は、ニューラルネットワークを用いて、文章補完AIのさらに高度なバージョンのように機能しながら、高度な数学の問題を解決することができます。arXivにある数学の論文を使って訓練されています。
Lean はプログラミングコードの形式で人間とやりとりしていたのに対して、Minervaは会話型のやりとりができます。問題を与えられると、その答えをわかりやすい英語で返すことができます。
Minervaにももちろん限界が見えています。例えば、素因数分解を行うことができる一方で、数字がどんどん大きくなると間違いを起こします。
Minervaは単なる統計的な推測にとどまらず、汎用的な法則を学習できることが示されています。その仕組みは現時点でGoogleによってまだ完全に解明されていません。
ブレインストームに使ったり、数学者ではない一般の人が専門書から情報を抽出したり、といった用途が期待できます。
数学AIの展望
今後は、数学AIが数学者のサポート役にとどまるのか、それとも独立した数学の研究をAIだけで行うことができるのでしょうか？
一部の数学者は「たとえ、AIが自ら数学の証明を生み出せても、その証明が理解不可能なものになるのでは」と意見します。その対策として、AIに客観性をもった数学的思考、異なる数学の分野の橋渡しを教え込むことだと思われます。
さらなる進歩を遂げるために、数学AIは、現場の課題の中から、興味深いもの、証明に値するものを自ら見出す力が必要です。また、「具体的な情報から抽象的な原理を導く」、つまり「理論を生み出す」力です。
そこまでできたら、数学者の仕事がどうなるのでしょうか。
執筆担当者 ヤン ジャクリン （データ分析官、講師）
