コンピュータは数学的な推論を自動的に構築するのにどれくらい近いですか？

Artificial Intelligence Toolkitは、次世代の自動定理証明者の形を定義し、それを使用して、数学と機械の関係を定義します。

1970年に、数学論理の研究でフィールズメダルを受賞した唯一の数学者ポールコーエンは、1970年に根拠のない予測を行い、それは数学者を喜ばせたり苛立たせたりし続けていると言われています。コンピューター」。セット理論を扱う大胆な方法で知られるコーエンは、証明を書くことを含め、すべての数学を自動化できると予測しました。



証明は、仮説または数学的仮定の真実を確認する段階的な論理的推論です。証拠が現れた後、仮説は定理になります。それは、ステートメントの正しさを確認し、それが真実である理由を説明します。しかし、その証拠は奇妙です。それは抽象的なものであり、物質的な経験とは関係ありません。 「それらは、架空の非物理的な世界と生物学的進化から出現した生き物との間の異常な接触の結果です」と、証拠構造の分析を通じて数学的確実性を研究しているカーネギーメロン大学の認知科学者サイモンデデオは言いました。 「進化は私たちにこれに対する準備をさせませんでした。」



コンピューターはバルクコンピューティングに適していますが、証明には別の何かが必要です。仮説は、誘導的推論（興味深い問題に関連する特別な直感）から生じ、証明は通常、推論的で段階的な論理に従います。多くの場合、複雑な創造的思考と隙間を埋めるというハードワークが必要であり、マシンはこのスキルの組み合わせを処理できません。



コンピューター化された定理証明者は2つのカテゴリーに分類されます。自動定理証明者（ATP）は通常、ブルートフォース法を使用して膨大な数の山を粉砕します。インタラクティブ定理証明者（ITP）は人間の助手として機能し、議論の正確さをチェックしたり、既存の証明の誤りを探したりすることができます。ただし、これら2つの戦略を組み合わせても（より現代的な証明者が行うように）、自動推論システムはそれらから出現しません。





カーネギーメロン大学の認知科学者サイモンデデオは、人間と機械が同様の方法で数学的な証拠を作成することを実証するのに役立ちました。



さらに、これらのツールは歓迎される人が非常に少なく、ほとんどの数学者はそれらを使用または承認していません。 「これは数学者にとって物議を醸すトピックです」とデデオは言いました。 「彼らのほとんどはその考えを好まない。」



この分野で未解決の難しい問題の1つは、プルーフ作成プロセスをどれだけ自動化できるかという問題です。システムは興味深い仮説を生成し、人々が理解できる方法でそれを証明することができますか？世界中のラボからの最近の一連のブレークスルーは、この質問に答えるための人工知能（AI）の方法を提供します。プラハのチェコ情報・ロボット・サイバネティクス研究所のジョセフ・アーバンは、既存の証明者の有効性を高めるために機械学習を使用するさまざまなアプローチを模索しています。 7月に彼のグループマシンによって作成および検証された一連の元の仮説と証拠を示しました。 6月、ChristianSzegediが率いるGoogleResearchのグループは、自然言語処理システムの長所を使用して、コンピューターの証拠の構造と説明を人間のものとより類似させる試みの結果を発表しました。



一部の数学者は、定理証明者を、学生が証明を書くことを学ぶ方法に革命を起こすことができるツールと見なしています。他の人は、コンピュータに高度な数学の証明を書かせることは不可能ではないにしても不要であると言います。しかし、有用な仮説を予測し、新しい定理を証明することができるシステムは、何か新しいことを達成することができます-ある種の機械版の理解です、とSzegediは言いました。そして、これは自動推論の可能性を示唆しています。

便利なマシン

数学者、論理学者、哲学者は、証明作成のどの部分が本質的に人間であるかについて長い間議論してきました。数学の機械化についての議論は今日も続いています。特に、コンピューターサイエンスが純粋な数学と融合する場合はそうです。



コンピュータ科学者にとって、定理の証明者は物議を醸すものではありません。それらは、プログラムが機能していることを確認する明確な方法を提供し、直感と創造性に関する議論は、問題を解決するための効果的な方法を見つけることほど重要ではありません。たとえば、マサチューセッツ工科大学のコンピューター科学者であるAdam Chlipalaは、生成する定理証明ツールを開発しました。インターネット上のトランザクションを保護する暗号化アルゴリズム-通常、人々がそのようなアルゴリズムを思い付くという事実にもかかわらず。彼のグループコードは、GoogleChromeブラウザのほとんどの通信ですでに使用されています。





ジョンズホプキンス大学のエミリーリエルは、定理証明者を使用して学生とコンピューターアシスタントを訓練します。



「任意の数学的なステートメントを1つのツールでコーディングし、すべての引数を組み合わせて、安全性の証明を得ることができます」とChlipala氏は述べています。



数学では、定理の証明者は、そうでなければ数千人の数学的な人年を要したであろう複雑で計算集約的な証明を作成するのに役立ちました。印象的な例はケプラーの仮説です三次元空間でのボールの最も密なパッキングについて（歴史的に、これらはオレンジまたは砲弾でした）。 1998年、ThomasHalesと彼の学生であるSamFergusonは、さまざまなコンピューター化された数学的手法を使用してこの証明を完成させました。結果は非常に面倒で、証明には3 GBかかりました。そのため、12人の数学者が数年間分析してから99％確信していると発表しました。



ケプラーの仮説は、機械によって解決される唯一の有名な問題ではありません。四色定理は、同じ色の2つの接触領域がない2次元マップをペイントするには、常に4色で十分であると主張し、1977年に、5色マップを処理するコンピュータープログラムを使用して計算し、すべてを4色に変換できることを示しました。2016年、3人の数学者がコンピュータープログラムを使用して、ピタゴリアントリプレットの長年のブール問題を証明しましたが、証明の最初のバージョンは200TBでした。十分に高速なインターネット接続があれば、3週間でダウンロードできます。

混合感情

これらの例は成功として宣伝されることがよくありますが、論争に独自の味を追加します。 40年以上前に4色の定理を証明したコンピューターコードは、人間が検証することはできませんでした。 「それ以来、数学者たちはこれが証拠であるかどうかについて議論してきました」とコロンビア大学の数学者マイケル・ハリスは言いました。





多くの数学者は、コロンビア大学のMichael Harrisとともに、コンピューター化された定理証明者を作成する必要性に疑問を投げかけています。後者は数学者を不要にするでしょう。



数学者のもう1つの不満は、定理証明者を使用する場合、最初にプログラミング方法を学び、次にコンピューターが理解できる言語で問題を表現する方法を理解する必要があるという事実に関連しています。これらすべてが数学の邪魔になります。 「私がこの技術に適した方法で質問を再定式化する時までに、私はこの問題を自分で解決するでしょう」とハリスは言いました。



多くの人々は、定理ソルバーの必要性を認識していません。 「彼らは独自のシステム、鉛筆、紙を持っていて、それは機能します」とケビン・バザードは言いました。、インペリアルカレッジロンドンの数学者。3年前に研究の方向を純粋な数学から定理の証明者と正式な証明に変えました。 「コンピューターは私たちのために素晴らしい計算を行いますが、難しい問題を自分たちで解決することは決してありませんでした」と彼は言いました。 「そしてそれが起こるまで、数学者はそれを買わないでしょう。」



しかし、Buzzardやその他の人々は、テクノロジーをさらに詳しく調べる必要があるかもしれないと考えています。たとえば、「コンピューターの証拠は、私たちが考えるほど異質ではないかもしれません」とデデオは言いました。最近、スタンフォード大学のコンピューター科学者であるスコット・ヴィテリと一緒に、彼はいくつかの有名な正規の証明（いくつかの始まりを含む）を逆設計しました。Euclid）と、類似点を探しているCoqの定理を証明するためにコンピュータープログラムによって生成された数十の証明。彼らは、機械の証明の分岐構造が人工の証明の分岐構造と非常に類似していることを発見しました。この共通の特性は、研究者が方法を見つけるのに役立つ可能性があると彼は言いました。



デデオ氏は、ヘルパープログラムに「機械の証明は見た目ほど謎めいたものではないかもしれない」と説明し、定理の証明



者はコンピュータサイエンスと数学の両方を教えるのに役立つツールになる可能性があると述べています。ジョンズホプキンス大学の数学者エミリーリエル学生が定理証明者を使用して証明を書くコースを開発しました。 「それは彼らを非常に組織化し、明確に考えるようにします」と彼女は言いました。 「初めて証明を書く学生は、彼らに何が必要かをすぐに理解したり、論理構造を理解したりできないかもしれません。」



リエルはまた、最近、彼の仕事で定理証明者をますます使用していると言います。 「常に使用する必要はなく、紙の落書きに取って代わることは決してありません。しかし、証拠にコンピューターアシスタントを使用することで、証拠の書き方についての私の理解が変わりました。」と彼女は言いました。



定理証明者は、数学を正直に保つ方法も提供します。 1999年、ソビエト、ロシア、アメリカの数学者ウラジミール・アレクサンドロヴィッチ・ボエボドスキーは、彼の証明の1つに誤りを発見しました。それから2017年に亡くなるまで、彼は証拠を検証するためにコンピューターの使用を積極的に推進しました。ヘイルズは、彼とファーガソンがコンピューターでテストしたところ、元の証明に何百ものエラーが見つかったと述べました。 Euclid'sElementsの最初の定理でさえ理想的ではありません。機械が数学者がそのような間違いを避けるのを助けることができるなら、なぜそれを利用しませんか？ハリスはこの提案に実際的な異議を唱えましたが、どれほど合理的かはわかりません。数学者がコンピューターが理解するために数学の形式化に時間を費やさなければならない場合、新しい数学にその時間を費やすことはできません。



ただし、Timati Gowers数学者でケンブリッジフィールズ賞を受賞した数学者は、さらに進んでいきたいと考えています。彼は、定理の証明者が将来、主要なジャーナルの人間の査読者に取って代わる方法を想像しています。「これがどのように標準的な慣行になるかわかります。あなたの仕事が受け入れられることを望むなら、あなたはそれを自動化されたレビュアーを通して実行しなければなりません。」

コンピューターとの会話

コンピューターが証拠をテストまたは開発する前に、研究者はまず重大なハードルを克服する必要があります：人間とコンピューターの言語間のコミュニケーションの障壁。



今日の定理証明者は、数学者の使いやすさを考慮せずに設計されています。最初のタイプであるATPは、ステートメントの真実をテストするために一般的に使用され、多くの場合、考えられるすべてのオプションをテストしました。 ATPにマイアミからシアトルへの旅行が可能かどうか尋ねると、彼はおそらくマイアミからの道路が通じるすべての都市を通り抜け、最終的にはシアトルに通じる都市を見つけるでしょう。





CambridgeUniversityのTimatiGowersは、定理の証明者がいつか人間の査読者に取って代わると信じています



プログラマーはATPを使用して、すべてのルールまたは公理をコーディングし、特定の仮説がそれらのルールに従っているかどうかを質問できます。そして、コンピュータがすべての作業を行います。 「証明したい仮説を入力し、答えを得たいと思っています」と、最近UCバークレーを離れてスタートアップを始めたコンピューター科学者のダニエル・ファンは言いました。



しかし、問題があります。ATPはその動作を説明していません。すべての計算はマシン内で行われ、人にとっては0と1の長いシーケンスのように見えます。黄氏は、すべてがランダムなデータの束のように見えるため、証明を見て推論をテストすることは不可能であると述べました。 「誰もそのような証拠を見て言うことはできません：すべてが明確です」と彼は言いました。



2番目のカテゴリであるITPには、数万の定理と証明を含む巨大なデータセットがあり、証明の正確さを確認できます。単に応答を発行するブラックボックス内で機能するATPとは異なり、ITPは相互作用を必要とし、場合によっては人からの指示を必要とするため、それほど近づきがたいものではありません。 「人は座って、証明するためにどのような技術が使用されているかを理解することができます」とファンは言いました。そのような証拠はDedeoとViteriによって研究されました。



近年、ITPはますます人気が高まっています。 2017年、ピタゴリアントリプルのブール問題を証明した三位一体は、Coqと呼ばれるITPを使用して、その証明の正式なバージョンを作成およびテストしました。 2005年、Microsoft ResearchCambridgeのGeorgesGontierは、Coqを使用して4色の定理を形式化しました。ヘイルズはまた、HOLライトおよびイザベルと呼ばれるITPを使用して、ケプラーの推測を正式に証明しました（HOLは高次ロジックの略です）。



今日、この分野の最前線は、学習と推論を組み合わせようとしています。多くの場合、ATPをITPと組み合わせて機械学習を統合し、両方の手法のパフォーマンスを向上させます。専門家は、ATP / ITPプログラムは推論を使用でき、人間と同じ方法で、または少なくとも同様の方法で数学的なアイデアを交換できると信じています。

推論の限界

ジョセフ・アーバンは、そのような組み合わせたアプローチは、証拠を得るために必要な推論と誘導の推論を組み合わせることができると信じています。彼のグループは、機械学習を利用した定理証明者を作成し、コンピューターが自分で経験から学習できるようにしました。過去数年にわたって、彼らはニューラルネットワークの力を探求してきました。これは、脳内のニューロンの動作とほぼ同じ方法でマシンが情報を処理するのに役立つコンピューティングユニットのレイヤーです。 7月に、彼らのグループは、定理の証明で訓練された神経ネットワークによって生成された新しい仮説を報告しました。



アーバンは、数年前に神経ネットワークを訓練して数学的なナンセンスを生み出すアンドレイ・カルパティの仕事に触発されました。しかし、アーバンはナンセンスを必要としませんでした-彼とグループは、何百万もの定理で訓練して、証拠を検索する独自のツールを開発しました。彼らはネットワークを使用して新しい仮説を生成し、Eと呼ばれるATPプログラムを使用してそれらの妥当性をテストしました。



ネットワークは50,000以上の新しい式を発行しましたが、それらの数万が繰り返されています。 「これ以上興味深い仮説を証明することはまだできないようです」とUrban氏は述べています。



Google ResearchのSzegediは、コンピューターの証拠における自動推論の問題を、はるかに広い分野の一部と見なしています。自然な言語処理には、単語や文の使用パターンの認識が含まれます。パターン認識は、Szegediが以前にGoogleで取り組んだコンピュータービジョンのコアアイデアでもあります。他のグループと同様に、彼のチームは、有用な証拠を見つけて説明できる定理証明者を作成したいと考えています。



AlphaZero（チェス、ゴー、ショギで人間を打ち負かすことができるDeepMindのソフトウェア）のようなAIツールの急速な開発に触発されて、Szegediグループは、証拠を記録するために言語認識の最新の進歩を使用したいと考えています。彼は、言語モデルは驚くほど正確な数学的推論を示すことができると述べました。



Google Researchの彼のグループは最近、ニューラルネットワークがよく使用する言語モデルを使用して新しい証拠を生成する方法について説明しました。証明された定理のツリー構造を認識するようにモデルをトレーニングした後、彼らは無料の実験を開始し、監督なしで定理を生成して証明するようにニューラルネットワークに依頼しました。生成された何千もの仮説のうち、13％は証明可能で新しいことが判明しました（データベース内の他の定理を繰り返さない）。彼は、そのような実験は、神経ネットワークが、ある意味で、証拠がどのように見えるかを理解することを学ぶことができると言っています。



「ニューラルネットワークは、人工的な直感の類似性を開発することができます」とSzegedi氏は述べています。



もちろん、これらの試みが40年前のコーエンの予言を実現するかどうかはまだ明らかではありません。ガワーズ氏は、2099年までにコンピューターが数学者を上回ることができると信じていると述べた。最初は、数学者は黄金時代を楽しむだろうと彼は言います。「彼らが面白いことをし、コンピューターが退屈なとき。しかし、それはそれほど長くは続かないと思います。」



結局のところ、マシンがますます開発を続け、膨大な量のデータにアクセスできる場合、マシンは非常にうまく、興味深いことを行うことを学ぶ必要があります。 「彼らは彼ら自身の要求をすることを学ぶでしょう」とGowersは言いました。



ハリスは同意しません。彼は、コンピューターによる証明が必要であるとは考えていません。あるいは、コンピューターによる証明が「人間の数学者を不要にする」ことになるとは考えていません。コンピューター科学者が合成直感をプログラムできるとしても、それでも人間の直感と競合することはありません。「コンピュータが理解しても、人間の意味では理解できません。」