Loading article…
自動定理証明（ ATPまたは自動演繹とも呼ばれる）は、コンピュータプログラムによる数学的定理の証明を扱う、自動推論および数理論理学の一分野である。数学的証明における自動推論は、コンピュータ科学の発展における主要な動機の一つであった。
形式論理の起源はアリストテレスに遡るが、19世紀末から20世紀初頭にかけて、近代論理と形式数学が発展した。フレーゲの『概念論』（1879年）は、完全な命題論理と、本質的には現代の述語論理の両方を導入した。[ 1 ] 1884年に出版された彼の『算術の基礎』[ 2 ]は、数学（の一部）を形式論理で表現した。このアプローチは、ラッセルとホワイトヘッドによって、影響力のある『プリンキピア・マテマティカ』で引き継がれ、1910年から1913年に初版が出版され、[ 3 ] 1927年に改訂版が出版された。 [ 4 ]ラッセルとホワイトヘッドは、形式論理の公理と推論規則を用いてすべての数学的真理を導き出すことができると考え、原理的には自動化への道を開いた。[ 5 ] 1920年、トーラルフ・スコレムはレオポルド・レーヴェンハイムによる以前の結果を簡略化し、レーヴェンハイム＝スコレムの定理を導き、1930年には、一階述語論理式の充足可能性（およびそれゆえ定理の妥当性）を（潜在的に無限に多くの）命題充足可能性問題に還元できるヘルブランド宇宙とヘルブランド解釈の概念を提唱した。[ 6 ]
1929年、モイジェシュ・プレスブルガーは、加算と等号を含む自然数の1階理論（現在では彼の名誉を称えてプレスブルガー算術と呼ばれている）が決定可能であることを示し、その言語で与えられた文が真か偽かを判定できるアルゴリズムを与えた。 [ 7 ] [ 8 ]
しかし、この肯定的な結果の直後、クルト・ゲーデルは『プリンキピア・マテマティカおよび関連システムの形式的に決定不可能な命題について』 （1931年）を出版し、十分に強力な公理系には、そのシステムで証明できない真の命題が存在することを示した。[ 9 ]このテーマは1930年代にアロンゾ・チャーチとアラン・チューリングによってさらに発展し、一方では計算可能性の2つの独立した同等の定義を与え、他方では決定不可能な問題の具体的な例を示した。[ 10 ]
1954年、マーティン・デイビスは、ニュージャージー州プリンストンの高等研究所で、JOHNNIAC真空管コンピュータ用にプレスバーガーのアルゴリズムをプログラムした。デイビスによれば、「その最大の功績は、2つの偶数の和が偶数であることを証明したことである」。 [ 8 ] [ 11 ] 1956年にアレン・ニューウェル、ハーバート・A・サイモン、JC・ショーによって開発された、プリンキピア・マテマティカの命題論理の演繹システムであるロジック・セオリストは、より野心的であった。同じくJOHNNIAC上で動作するロジック・セオリストは、少数の命題公理と3つの演繹規則（モーダス・ポネンス、（命題）変数置換、式を定義に置き換える）から証明を構築した。このシステムはヒューリスティックなガイダンスを使用し、プリンキピアの最初の52の定理のうち38を証明することに成功した。[ 8 ]
論理理論家の「ヒューリスティック」アプローチは人間の数学者を模倣しようとしたが、原理的にもすべての有効な定理の証明が見つかることを保証できなかった。対照的に、他のより体系的なアルゴリズムは、少なくとも理論的には、一階述語論理の完全性を達成した。初期のアプローチは、ヘルブランドとスコレムの結果に依拠し、ヘルブランド宇宙の項で変数をインスタンス化することによって、一階述語論理式を、より大規模な命題論理式の集合に順次変換した。命題論理式は、さまざまな方法を使用して充足不可能性をチェックすることができた。ギルモアのプログラムは、論理式の充足可能性が明白な形式である選言標準形への変換を使用した。 [ 8 ] [ 12 ]
基礎となる論理によって、式の妥当性を判断する問題は、自明なものから不可能なものまで様々です。命題論理の一般的なケースでは、この問題は決定可能ですが、co-NP完全であるため、一般的な証明タスクには指数時間アルゴリズムしか存在しないと考えられています。 [ 13 ]一階述語論理では、ゲーデルの完全性定理によれば、定理（証明可能な命題）は意味的に妥当な整形式式と全く同じであるため、妥当な式は計算可能列挙可能です。つまり、無制限のリソースが与えられれば、任意の妥当な式は最終的に証明できます。しかし、無効な式（与えられた理論によって含意されない式）は、常に認識できるとは限りません。[ 14 ]
上記は、ペアノ算術などの一階理論に当てはまります。ただし、一階理論で記述できる特定のモデルの場合、いくつかの命題は、そのモデルを記述するために使用される理論では真であっても決定不能である可能性があります。たとえば、ゲーデルの不完全性定理により、公理のリストが無限列挙可能であっても、自然数に対して真である公理を持つ無矛盾な理論では、自然数に対してすべての一階命題が真であることを証明できないことがわかります。[ 15 ]したがって、自動定理証明器は、調査対象の命題が、使用されている理論では決定不能である場合に、たとえそれが対象となるモデルでは真であっても、証明を探索中に終了しないことになります。この理論的な限界にもかかわらず、実際には、定理証明器は、一階理論で完全に記述されていないモデル（整数など）であっても、多くの難しい問題を解決できます。
より単純ではあるが関連する問題として、定理の既存の証明が有効であることを証明するという証明検証がある。この場合、一般的には、証明の各ステップを原始的な再帰関数またはプログラムで検証できることが求められるため、この問題は常に決定可能である。
自動定理証明器によって生成される証明は通常非常に大きいため、証明の圧縮の問題は極めて重要であり、証明器の出力を小さくし、結果として理解しやすく検証しやすくすることを目的とした様々な技術が開発されてきた。
証明支援システムでは、人間ユーザーがシステムにヒントを与える必要があります。自動化の度合いによっては、証明者は基本的に証明チェッカーに縮小され、ユーザーが形式的な方法で証明を提供するか、重要な証明タスクを自動的に実行することができます。対話型証明システムはさまざまなタスクに使用されますが、完全自動システムでも、人間の数学者が長い間解決できなかった少なくとも1つの定理、すなわちロビンス予想を含む、興味深く難しい定理が数多く証明されています。[ 16 ] [ 17 ]しかし、これらの成功は散発的であり、難しい問題に取り組むには通常、熟練したユーザーが必要です。
定理証明とその他の手法の間には、別の区別が設けられることがあります。定理証明とは、公理から始めて推論規則を用いて新たな推論ステップを生成する、伝統的な証明プロセスから成る場合を指します。その他の手法としてはモデル検査があり、最も単純なケースでは、多くの可能な状態を総当たりで列挙します（ただし、モデルチェッカーの実際の実装には高度な工夫が必要であり、単に総当たりで列挙するだけではありません）。
推論規則としてモデル検査を用いるハイブリッド型の定理証明システムも存在する。また、特定の定理を証明するために書かれたプログラムもあり、そのプログラムが特定の結果で終了すれば定理が真であるという（通常は非公式な）証明が付随している。その好例として、機械支援による四色定理の証明が挙げられる。これは、プログラムの計算量が膨大であるため、人間による検証が事実上不可能であると主張された最初の数学的証明として、非常に物議を醸した（このような証明は非検証可能な証明と呼ばれる）。プログラム支援による証明のもう一つの例は、コネクトフォーのゲームは必ず先手プレイヤーが勝つことを示す証明である。
自動定理証明の商用利用は、主に集積回路の設計と検証に集中しています。Pentium FDIV バグ以降、現代のマイクロプロセッサの複雑な浮動小数点演算ユニットは、より厳密な検証のもとで設計されています。AMD 、Intelなどは、自動定理証明を使用して、プロセッサ内で除算やその他の演算が正しく実装されていることを検証しています。[ 18 ]
定理証明器の他の用途としては、形式仕様を満たすプログラムを構築するプログラム合成などがあります。[ 19 ]自動定理証明器は、 Isabelle/HOLなどの証明支援システムと統合されています。[ 20 ]
定理証明器の応用は、自然言語処理や形式意味論にも見られ、談話表現の分析に用いられている。[ 21 ] [ 22 ]
1960年代後半、自動推論の研究に資金提供している機関は、実用化の必要性を強調し始めた。最初に実を結んだ分野の1つはプログラム検証であり、 Pascal、Adaなどの言語で書かれたコンピュータプログラムの正しさを検証する問題に、一階定理証明器が適用された。初期のプログラム検証システムの中で注目すべきは、スタンフォード大学のDavid Luckhamによって開発されたStanford Pascal Verifierである。[ 23 ] [ 24 ] [ 25 ]これは、同じくスタンフォード大学でJohn Alan Robinsonの分解原理を使用して開発されたStanford Resolution Proverに基づいていた。これは、正式な解答が発表される前にアメリカ数学会の通知で発表された数学的問題を解決する能力を示した最初の自動推論システムであった。
一階述語論理による定理証明は、自動定理証明の最も成熟したサブフィールドの 1 つです。この論理は、任意の問題を、多くの場合、かなり自然で直感的な方法で指定できるほど表現力があります。一方で、まだ半決定可能であり、完全かつ健全な計算体系が多数開発されているため、完全に自動化されたシステムが可能です。[ 26 ]高階論理などのより表現力の高い論理では、一階述語論理よりも幅広い問題を便利に表現できますが、これらの論理の定理証明はあまり発展していません。[ 27 ] [ 28 ]
一階自動定理証明器とSMT ソルバーの間にはかなりの重複があります。一般的に、自動定理証明器は量化子を含む完全な一階論理をサポートすることに重点を置いていますが、SMT ソルバーはさまざまな理論 (解釈された述語記号) をサポートすることに重点を置いています。ATP は量化子が多い問題に優れていますが、SMT ソルバーは量化子のない大きな問題に優れています。[ 29 ]この境界線は曖昧で、一部の ATP は SMT-COMP に参加し、一部の SMT ソルバーはCASCに参加しています。[ 30 ]
実装されたシステムの品質は、標準的なベンチマーク例の大規模なライブラリである定理証明器のための数千の問題（TPTP）問題ライブラリ[ 31 ]の存在と、多くの重要なクラスの一階問題に対する一階システムの年次競技であるCADE ATPシステムコンペティション（CASC）の恩恵を受けています。
以下に、重要なシステム（いずれもCASC競技会で少なくとも1部門優勝経験あり）をいくつか挙げます。
定理証明器博物館[ 33 ]は、定理証明器システムのソースコードを将来の分析のために保存する取り組みであり、それらは重要な文化的/科学的遺物である。同博物館には、上記で述べたシステムの多くのソースコードが保管されている。
ATPとSMTソルバーは相補的な強みを持っています。前者は量化子をよりエレガントに処理しますが、後者は主に地上の大規模な問題で優れています。
近年、SMT-COMP と CASC の境界線が曖昧になり、SMT ソルバーが CASC で競い合い、ATP が SMT-COMP で競い合うようになっている。
この資料は、教育目的であれば複製可能です。