おはようございます、satoです。
昨日に引き続き「人工知能」について語ります。
昨日は一般的に人工知能が出来ること、出来ないことを書きましたが、今日は「数学という分野で人工知能ができそうなこと」について考えてみました。
人工知能が得意そうなこと～四色定理の証明～
まず、コンピュータは高速で大量の計算をすることができます。というか、むしろこれがコンピュータのアイデンティティですよね。
しかも、人間は疲れてミスが多くなりますが、コンピュータは基本ミスをすることはありません。
コンピュータがミスをするとしたら、プログラムに間違いがあるからで、それはどちらかと言えば人間の問題です。
そういうわけで、「大量の計算が必要な問題」は人工知能が得意でしょう。
数学においても、大量の計算が必要な時はあります。
例えば、有名な話だと「四色定理」の証明にはコンピュータが用いられています。
四色定理とは「平面上の任意の地図は4色あれば塗り分けられる」というものです。実際に日本地図とか東京23区とか北海道の213市町村で確かめてみるといいです。
この証明にはコンピュータが本質的に用いられているのですが、私が知っている範囲で簡単に説明すると…。
「適当な地図を取った時に、必ずどれかが地図の一部に含まれる」という地図の形を用意します。
この地図の集まり(専門用語で不可避集合と言います)で「いい条件」のものを持ってくると4色定理が示せるわけです。
そして、この「いい条件」を満たす不可避集合が存在することをコンピュータを使って示したのです。
不可避集合に含まれる形の数は現在の改良された方法で633個になります。随分と多いですね…^^;
この不可避集合を探す際に結構な数の計算が必要で、それをコンピュータにさせたのです。初めて証明した当時は高スペックのパソコンで1200時間も計算させたのですから、人間には出来ない技ですね。
面白いことに、現在も四色定理をコンピュータ無しで証明した人は誰もいません。
むしろ「全ての証明(プログラムにバグがないことも含めて)をコンピュータにさせた」なんてこともあります。
このように複雑で大量の計算が必要になる時は人工知能の能力を発揮することが出来そうです。
コンピュータが数学を証明する～Coq～
さらに、最近のコンピュータは計算だけでなく式変形や因数分解、さらには証明まで出来ます。
先程四色定理を「コンピュータのみで」証明させたという話もありましたが、それはCoqという証明ソフトウェアを用いてさせたのです。
数学という世界は「記号」によって成り立っています。そして、数学の証明は「論理」によって成り立っていますが、これも結構パターンがあります。
よって、「証明や理論それ自体を数学として扱う」なんてことも出来ます。これが「数理論理学」ですが、その応用として「コンピュータが証明する」事もできるわけです。
人工知能が全ての数学の問題を解決できるか？そして、「発見」できるか？
このように数学の証明を行うまでになったコンピュータの発達ですが、
果たして人工知能が数学の問題を解決できるのか？そして「発見」できるのか？
というのは一つの疑問に思います。…長くなったので、次回これを書きます。
この記事を書いたブロガー
-
「素直に、深く、面白く」がモットーの摂理男子。霊肉ともに生粋の道産子。30代になりました。目指せ数学者。数学というフィールドを中心に教育界隈で色々しています。
軽度の発達障害(ADHD・PD)&HSP傾向あり。
最近の投稿
