人工知能は数学者の夢を見るか？ | 摂理研究所/キリスト教福音宣教会

おはようございます、satoです。

昨日に引き続き「人工知能」について語ります。
昨日は一般的に人工知能が出来ること、出来ないことを書きましたが、今日は「数学という分野で人工知能ができそうなこと」について考えてみました。

目次非表示

人工知能が得意そうなこと～四色定理の証明～
コンピュータが数学を証明する～Coq～
人工知能が全ての数学の問題を解決できるか？そして、「発見」できるか？

人工知能が得意そうなこと～四色定理の証明～

まず、コンピュータは高速で大量の計算をすることができます。というか、むしろこれがコンピュータのアイデンティティですよね。
しかも、人間は疲れてミスが多くなりますが、コンピュータは基本ミスをすることはありません。
コンピュータがミスをするとしたら、プログラムに間違いがあるからで、それはどちらかと言えば人間の問題です。
そういうわけで、「大量の計算が必要な問題」は人工知能が得意でしょう。

数学においても、大量の計算が必要な時はあります。
例えば、有名な話だと「四色定理」の証明にはコンピュータが用いられています。
四色定理とは「平面上の任意の地図は4色あれば塗り分けられる」というものです。実際に日本地図とか東京23区とか北海道の213市町村で確かめてみるといいです。
この証明にはコンピュータが本質的に用いられているのですが、私が知っている範囲で簡単に説明すると…。

「適当な地図を取った時に、必ずどれかが地図の一部に含まれる」という地図の形を用意します。
この地図の集まり(専門用語で不可避集合と言います)で「いい条件」のものを持ってくると4色定理が示せるわけです。

そして、この「いい条件」を満たす不可避集合が存在することをコンピュータを使って示したのです。
不可避集合に含まれる形の数は現在の改良された方法で633個になります。随分と多いですね…^^;

この不可避集合を探す際に結構な数の計算が必要で、それをコンピュータにさせたのです。初めて証明した当時は高スペックのパソコンで1200時間も計算させたのですから、人間には出来ない技ですね。

面白いことに、現在も四色定理をコンピュータ無しで証明した人は誰もいません。
むしろ「全ての証明(プログラムにバグがないことも含めて)をコンピュータにさせた」なんてこともあります。

このように複雑で大量の計算が必要になる時は人工知能の能力を発揮することが出来そうです。

コンピュータが数学を証明する～Coq～

さらに、最近のコンピュータは計算だけでなく式変形や因数分解、さらには証明まで出来ます。
先程四色定理を「コンピュータのみで」証明させたという話もありましたが、それはCoqという証明ソフトウェアを用いてさせたのです。
数学という世界は「記号」によって成り立っています。そして、数学の証明は「論理」によって成り立っていますが、これも結構パターンがあります。
よって、「証明や理論それ自体を数学として扱う」なんてことも出来ます。これが「数理論理学」ですが、その応用として「コンピュータが証明する」事もできるわけです。