自動定理証明

自動定理証明( ATPまたは自動演繹とも呼ばれる) は、コンピュータ プログラムによる数学定理の証明を扱う自動推論と数学論理のサブフィールドです。数学的証明よりも自動推論が重視されたことが、コンピュータ サイエンスの発展の大きな要因でした。

形式化された論理の起源はアリストテレスに遡るが、19世紀末から20世紀初頭にかけては、近代論理学と形式化された数学が発展した。フレーゲのBegriffsschrift (1879) は、完全な命題計算と本質的に近代的な述語論理の両方を導入した。^[1] 1884年に出版された彼のFoundations of Arithmetic ^{[2] は}、数学（の一部）を形式論理で表現した。このアプローチは、ラッセルとホワイトヘッドによって継承され、影響力のあったPrincipia Mathematicaは1910年から1913年に初めて出版され、^[3] 1927年に改訂第2版が出版された。^[4]ラッセルとホワイトヘッドは、形式論理の公理と推論規則を使用してすべての数学的真理を導き出すことができると考え、原理的にはプロセスを自動化できるとした。 1920年、トラルフ・スコーレムはレオポルド・レーヴェンハイムの以前の結果を簡略化し、レーヴェンハイム・スコーレムの定理を導き、1930年にはエルブラン宇宙の概念とエルブラン解釈を導き、これにより一階述語論理式の充足可能性（および定理の妥当性）が（潜在的に無限に多い）命題充足可能性問題に還元されることが認められた。^[5]

1929年、モイジェシュ・プレスブルガーは、加法と等式を含む自然数の第一階理論（現在では彼に敬意を表してプレスブルガー算術と呼ばれている）が決定可能であることを示して、その言語で与えられた文が真か偽かを判定できるアルゴリズムを与えた。 ^{[6] [7]}

しかし、この肯定的な結果の直後に、クルト・ゲーデルは『プリンキピア・マテマティカと関連システムの形式的に決定不能な命題について』 （1931年）を出版し、十分に強い公理系には、そのシステムでは証明できない真の命題が存在することを示した。このテーマは1930年代にアロンゾ・チャーチとアラン・チューリングによってさらに発展させられ、彼らは一方では計算可能性の2つの独立だが同等な定義を与え、他方では決定不能な問題の具体的な例を示した。

第二次世界大戦後まもなく、最初の汎用コンピュータが利用可能になった。1954年、マーティン・デイビスは、ニュージャージー州プリンストン高等研究所のJOHNNIAC 真空管コンピュータ用にプレスバーガーのアルゴリズムをプログラムした。デイビスによると、「その偉大な功績は、2つの偶数の和が偶数であることを証明したことだった」。^{[7] [8]}さらに野心的なのは、1956年のLogic Theoristで、これはアレン・ニューウェル、ハーバート・A・サイモン、JC・ショーによって開発されたプリンキピア・マセマティカの命題論理のための演繹システムであった。これもJOHNNIAC上で動作し、Logic Theoristは、少数の命題公理と3つの演繹規則、すなわち可能性、（命題的）変数置換、および定義による式置き換えから証明を構築した。このシステムはヒューリスティックなガイダンスを使用し、プリンキピアの最初の52の定理のうち38を証明することに成功した。^[7]

論理学者の「ヒューリスティック」なアプローチは、人間の数学者を模倣しようとしたが、原理的にさえすべての有効な定理の証明が見つかる保証はなかった。対照的に、他のより体系的なアルゴリズムは、少なくとも理論的には、一階述語論理の完全性を達成した。初期のアプローチは、エルブランとスコーレムの結果に依存し、エルブラン宇宙の項で変数をインスタンス化することにより、一階述語論理式を連続的に大きな命題論理式の集合に変換した。その後、いくつかの方法を使用して命題論理式の不充足性をチェックできた。ギルモアのプログラムは、論理式の充足性が明らかである形式である選言標準形への変換を使用した。^{[7] [9]}

基礎となる論理に応じて、式の妥当性を決定する問題は、自明なものから不可能なものまでさまざまです。一般的な命題論理の場合、問題は決定可能ですが、NP完全であるため、一般的な証明タスクには指数時間アルゴリズムのみが存在すると考えられています。一階述語計算の場合、ゲーデルの完全性定理は、定理（証明可能なステートメント）がまさに意味的に有効な整形式の式であるため、有効な式は計算可能に列挙可能であると述べています。つまり、無制限のリソースが与えられれば、有効な式はすべて最終的に証明できます。ただし、無効な式（特定の理論によって含意され ない式）は常に認識できるとは限りません。

上記は、ペアノ算術などの一階理論に当てはまります。しかし、一階理論で記述できる特定のモデルでは、一部のステートメントは真であっても、そのモデルを記述するために使用される理論では決定不能である場合があります。たとえば、ゲーデルの不完全性定理により、公理が自然数に対して真である一貫した理論は、公理のリストが無限に列挙可能であるとしても、自然数に対して真であるすべての一階ステートメントを証明できないことが分かっています。したがって、自動化された定理証明器は、調査対象のステートメントが使用されている理論で決定不能である場合に、たとえそれが対象のモデルでは真であっても、証明の検索中に終了できなくなります。この理論上の制限にもかかわらず、実際には、定理証明器は、どの一階理論でも完全には記述されないモデル (整数など) でも、多くの難しい問題を解決できます。

より単純だが関連する問題として、定理の既存の証明が有効であることが証明される証明検証がある。このためには、通常、個々の証明ステップが原始的な再帰関数またはプログラムによって検証できることが要求され、したがって、問題は常に決定可能である。

自動定理証明器によって生成される証明は一般に非常に大きいため、証明の圧縮の問題は重要であり、証明器の出力を小さくし、その結果、より簡単に理解および検証できるようにすることを目的としたさまざまな手法が開発されてきました。

証明アシスタントでは、人間のユーザーがシステムにヒントを与える必要があります。自動化の程度に応じて、証明器は基本的に証明チェッカーに縮小され、ユーザーが正式な方法で証明を提供することも、重要な証明タスクを自動的に実行することもできます。対話型証明器はさまざまなタスクに使用されますが、完全に自動化されたシステムでさえ、少なくとも長い間人間の数学者が解決できなかったロビンズ予想など、多くの興味深く難しい定理を証明してきました。^{[10] [11]}ただし、これらの成功は散発的であり、難しい問題に取り組むには通常、熟練したユーザーが必要です。

定理証明と他の技法の間には別の区別が付けられることがあります。定理証明とは、公理から始めて推論規則を使用して新しい推論ステップを生成するという従来の証明で構成されるプロセスを指します。他の技法にはモデル検査が含まれます。これは、最も単純なケースでは、多くの可能な状態を力ずくで列挙する処理です (ただし、モデル検査の実際の実装には多くの巧妙さが必要であり、単純に力ずくで済むわけではありません)。

モデル検査を推論規則として使用するハイブリッド定理証明システムがあります。また、特定の定理を証明するために書かれたプログラムもあり、そのプログラムには、プログラムが特定の結果で終了した場合、その定理が真であるという（通常は非公式の）証明が含まれます。この良い例は、4色定理の機械支援証明です。これは、プログラムの計算が膨大なため人間が検証することが本質的に不可能である最初の数学的証明として非常に物議を醸しました（このような証明は、非調査証明と呼ばれます）。プログラム支援証明の別の例としては、コネクトフォーのゲームでは常に最初のプレーヤーが勝つことができること を示す証明があります。

自動定理証明の商用利用は、主に集積回路の設計と検証に集中しています。Pentium FDIVのバグ以来、現代のマイクロプロセッサの複雑な浮動小数点ユニットは、さらに綿密に設計されています。AMD 、Intelなどの企業は、自動定理証明を使用して、除算やその他の演算がプロセッサに正しく実装されているかどうかを検証しています。^[12]

定理証明器の他の用途としては、プログラム合成、形式仕様を満たすプログラムの構築などがある。^[13]自動定理証明器は、Isabelle/HOLなどの証明支援システムと統合されている。^[14]

定理証明器の応用は自然言語処理や形式意味論にも見られ、談話表現の分析に使用されています。^{[15] [16]}

1960 年代後半、自動演繹の研究に資金を提供する機関は、実用的なアプリケーションの必要性を強調し始めました。^[要出典]最初の実りある分野の 1 つはプログラム検証であり、そこでは、 Pascal、Adaなどの言語で書かれたコンピュータ プログラムの正しさを検証する問題に、一階定理証明器が適用されました。初期のプログラム検証システムの中で注目すべきは、スタンフォード大学のDavid Luckhamが開発した Stanford Pascal Verifier です。^{[17] [18] [19]これは、同じくスタンフォードで}John Alan Robinsonの解決原理を使用して開発された Stanford Resolution Prover に基づいています。これは、アメリカ数学会の通知で正式に解が発表される前に発表された数学の問題を解く能力を実証した最初の自動演繹システムでした。^[要出典]

一次定理証明は、自動定理証明の最も成熟したサブフィールドの 1 つです。この論理は表現力に富んでいるため、多くの場合、自然で直感的な方法で任意の問題を指定できます。一方で、まだ半決定可能であり、完全で健全な計算が多数開発されており、完全に自動化されたシステムを実現しています。^[20]高階論理などのより表現力豊かな論理では、一次論理よりも幅広い問題を簡単に表現できますが、これらの論理の定理証明はあまり開発されていません。^{[21] [22]}

一次自動定理証明器とSMTソルバーの間には、かなりの重複があります。一般的に、自動定理証明器は量指定子付きの完全な一次論理のサポートに重点を置いていますが、SMTソルバーはさまざまな理論（解釈された述語記号）のサポートに重点を置いています。ATPは量指定子の多い問題に優れていますが、SMTソルバーは量指定子のない大規模な問題に適しています。^{[23]一部のATPはSMT-COMPに参加し、一部のSMTソルバーは}CASCに参加しているほど、境界線は曖昧です。^[24]

実装されたシステムの品質は、標準的なベンチマーク例の大規模なライブラリ（定理証明者のための数千の問題（TPTP）問題ライブラリ^[25]）の存在と、多くの重要な一階問題クラスに対する一階システムの年次コンテストであるCADE ATPシステムコンペティション（CASC）の存在の恩恵を受けています。

いくつかの重要なシステム（いずれも CASC 競技部門で少なくとも 1 つの賞を獲得しています）を以下にリストします。

• E は完全な一階述語論理のための高性能な証明器ですが、純粋に方程式の計算に基づいて構築されており、もともとはミュンヘン工科大学の自動推論グループでWolfgang Bibelの指導の下で開発され、現在はシュトゥットガルトのバーデン・ヴュルテンベルク州立大学で使用されています。
• アルゴンヌ国立研究所で開発されたOtter は、一次分解能とパラモジュレーションに基づいています。Otter はその後、 Mace4とペアになっているProver9に置き換えられました。
• SETHEO は、目標指向モデル消去計算に基づく高性能システムであり、もともとWolfgang Bibelの指導の下、チームによって開発されました。E と SETHEO は、複合定理証明器 E-SETHEO で (他のシステムと) 統合されました。
• ヴァンパイアはもともとマンチェスター大学のアンドレイ・ヴォロンコフとクリシュトフ・ホダーによって開発され、実装されました。現在は成長を続ける国際チームによって開発されています。2001年以来、CADE ATPシステムコンペティションのFOF部門（他の部門も含む）で定期的に優勝しています。^[26]
• Waldmeister は、Arnim Buch と Thomas Hillenbrand によって開発された単位等式一階論理に特化したシステムです。14 年連続 (1997 ～ 2010 年)、CASC UEQ 部門で優勝しました。
• SPASS は、等式を持つ一階論理定理証明器です。これは、マックス・プランク計算機科学研究所のAutomation of Logic 研究グループによって開発されました。

定理証明器博物館^[27]は、定理証明器システムのソースを将来の分析のために保存するための取り組みです。定理証明器システムは重要な文化的/科学的遺物であるためです。この博物館には、上記のシステムの多くのソースが保管されています。

• 統合による第一階層の解決
• モデルの排除
• 分析的タブロー法
• 重ね合わせと項の書き換え
• モデルチェック
• 数学的帰納法^[28]
• 二分決定図
• DPLL
• 高階統一
• 数量詞の除去^[29]

• アルトエルゴ
• オートマス
• VC-1000
• え
• アイサプランナー
• LCF
• ミザール
• ニューPRL
• パラドックス
• 諺9
• PVS
• SPARK（プログラミング言語）
• 十二
• Z3 定理証明器

• カリーヌ
• ウルフラムマセマティカ
• リサーチサイクル

• 定理証明ツールのリスト