自動定理証明

自動定理証明（じどうていりしょうめい、英: automated theorem proving, ATP）とは、自動推論 (AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理に対する証明を発見すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。

アルゴンヌ国立研究所は1960年代以降2000年代まで、自動定理証明のリーダーだった。

歴史

論理学的背景

論理学の起源はアリストテレスまで遡るが、現代的数理論理学は19世紀末から20世紀初頭に発展した。フレーゲの『概念記法』(1879) が完全な命題論理と一階述語論理の基本的なものを導入^[1]。同じくフレーゲの『算術の基礎』(1884)^[2]でも、形式論理の数学（の一部）を説明している。この流れを受け継いだのがラッセルとホワイトヘッドの『プリンキピア・マテマティカ』で、初版は1910年から1913年に出版され^[3]、1927年に第2版が出ている^[4]。ラッセルとホワイトヘッドは、公理と形式論理の推論規則からあらゆる数学的真理が導き出せると考え、証明自動化への道を拓いた。1920年、トアルフ・スコーレムはレオポールト・レーヴェンハイム（英語版）の成果を単純化したレーヴェンハイム-スコーレムの定理をもたらし、1930年にはエルブラン領域とエルブラン解釈により、一階の論理式の充足（不）可能性（および定理の妥当性）を命題論理の充足可能性問題に還元できることが示された^[5]。

1929年、Mojżesz Presburger はプレスブルガー算術（加法と等号のある自然数の理論）が決定可能であり、その言語内の任意の文の真偽を判定できるアルゴリズムを示した^[6][7]。しかしその直後、クルト・ゲーデルが Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I (1931) を発表し、十分に強力な公理系はその体系内で証明も反証もできない文を含みうることを示した。1930年代にこの課題を研究したのがアロンゾ・チャーチとアラン・チューリングで、それぞれ独自に等価な計算可能性の定義を与え、決定不能な具体例も示した。

最初の実装

第二次世界大戦後、第一世代のコンピュータが登場。1954年、マーチン・デービス（英語版）がプリンストン高等研究所にて真空管コンピュータJOHNNIAC（英語版）上にプレスブルガーのアルゴリズムを実装した。デービスによれば「2つの偶数の総和も偶数であることを証明するという大きな成果があった」という^[7][8]。さらに野心的な試みとして Logic Theorist がある。これはアレン・ニューウェルとハーバート・サイモンとクリフ・ショーが開発したもので、『プリンキピア・マテマティカ』の命題論理を対象とした推論システムだった。こちらもJOHANNIAC上で動作し、命題論理の少数の公理と推論規則（モーダスポネンス、命題変数の置換など）から証明を構築した。ヒューリスティックによる誘導を使っており、『プリンキピア・マテマティカ』の52の定理のうち38の証明に成功した^[7]。

Logic Theoristのヒューリスティックとは人間の数学者のエミュレートを試みることであり、妥当な定理すべてについて証明できることを保証できなかった。対照的に、より体系的なアルゴリズムで（少なくとも理論上は）一階述語論理の完全性を達成できている。初期の手法ではエルブランとスコーレムの成果に基づき、一階述語論理の論理式を複数の命題論理の論理式に変換していた。そして、いくつかの技法で命題論理式の充足不可能性をチェックする。ギルモアのアルゴリズムは加法標準形に変換することで充足可能性を判定しやすくしていた^[7][9]。

問題の決定可能性

使用する論理によって、論理式の妥当性の判定は自明なものから不可能なものまで様々である。命題論理の多くの問題では、定理は決定可能だがco-NP完全問題であり、汎用的な証明には指数時間アルゴリズムしかないと考えられている。一階述語論理では、完全性定理より妥当な論理式は証明可能であり、その逆も成り立つから、妥当な論理式の全体は再帰的に枚挙可能である。したがって、妥当な論理式の証明を機械的に探索することはできる。

妥当でない文、すなわち与えられた定理から意味論的に導かれない式は認識可能とは限らない。さらにゲーデルの不完全性定理によれば、ある程度の算術を含む無矛盾な体系は本質的不完全であり、本質的不完全な体系は本質的決定不可能であるから、とくに決定不可能である。そのような場合、一階述語論理の定理証明機は証明探索の完了に失敗する（停止しない）可能性がある。このような理論上の制限はあるが、実用的な定理証明機は様々な難しい問題の証明をすることができる。

関連する問題

関連した問題に、自動証明検証と、証明のコンピュータによる支援がある。定理の証明の正当性を検証するには、証明の各段階を原始再帰関数やプログラムで検証できる必要があり、そうすることで問題は常に決定可能となる。

自動定理証明で生成される証明は長大なものとなることが多く、証明の圧縮 (proof compression) という問題が重要となり、様々な技法が考案されている。

対話型定理証明機では人間のユーザーがシステムにヒントを与える必要がある。自動化の度合いによっては、証明機が単なる証明検証機的なものとなってユーザーが提供した形式的証明を検証するだけの場合もあるし、大部分の証明を自動的に行う場合もある。対話型証明機は様々なタスクに使えるが、完全自動システムは長期にわたって人間の数学者がてこずってきた困難な問題を証明してきた^[10][11]。しかし、そのような成功例は稀で、一般に困難な問題を解くには熟練したユーザーの補助が必要である。

定理証明とそれ以外の区別の観点として、公理から出発して推論規則に従って推論を行い、いわゆる証明を行うものを定理証明と呼ぶ。モデル検査などのそれ以外の技術では、考えられる全ての状態を列挙するようなものである（モデル検査の実装ではもう少し賢さが必要であるが、それで力づくの手法でなくなるわけではない）。

モデル検査的手法を推論規則として利用するハイブリッド型の定理証明システムも存在する。また、特定の定理を証明するために書かれたプログラムも存在し、プログラムがある結果を返して終了したときに定理が真であることが証明される。そのようなプログラムの好例として四色定理の計算機支援証明がある。人間の手では証明できなかった問題を証明したことで物議をかもしたそのプログラムは、非常に複雑で検証不可能と言われた。他の例として重力付き四目並べゲームで先手が必ず勝つことを証明したことが挙げられる。

産業への応用

産業分野での応用例としては、LSIの設計とその検証が挙げられ、モデル的手法とともに使われている。Pentium FDIV バグ 以来、FPUの設計は極めて厳密に行われている。AMDやインテルはプロセッサの設計検証に自動定理証明を使っている。

一階述語論理の定理証明

一階述語論理の定理証明は自動定理証明の中でも最も研究が進んでいる。この論理は適度に自然で直感的な方法で様々な問題を記述できる程度に表現豊かである。一方、半決定的で健全で完全な計算方法が開発されており、完全自動システムを構築することが可能である。さらに表現力のある論理（高階述語論理や様相論理）は、さらに様々な問題を記述可能だが、それらの定理証明は一階述語論理ほど開発が進んでいない。

ベンチマークと競技会

実装システムの品質は標準ベンチマーク例の大きなライブラリ Thousands of Problems for Theorem Provers (TPTP) の存在によって高められている^[12]。また、Conference on Automated Deduction(CADE) 主催の ATP System Competition (CASC) は一階述語論理システムの競技会であり、これもシステムの品質向上に寄与している。

以下に主なシステムを列挙する（いずれも少なくとも1回は CASC で優勝している）。

• E は Purely Equational Calculus に基づいた高性能証明機。ミュンヘン工科大学の自動推論グループが開発した。
• Otter はアルゴンヌ国立研究所で開発された世界で初めて広く使われた高性能証明機である。導出と導出における統合推論に基づいている。Otterの後継としてProver9とMasce4がある。
• SETHEO はゴール指向の model elimination 法に基づいた高性能システム。ミュンヘン工科大学の自動推論グループが開発した。E と SETHEO は統合され、E-SETHEO となった。
• Vampire はマンチェスター大学の Andrei Voronkov と Krystof Hoder が開発・実装した。かつては Alexandre Riazanov も参加していた。定理証明機のワールドカップ（the CADE ATP System Competition）の最高の CNF (MIX) 部門で7年間優勝している（1999年、2001～2006年）。
• Waldmeister は unit-equational な一階述語論理に特化したシステムである。10年間にわたって CASC UEQ 部門で優勝している（1997年～2006年）。
• SPASSは等号を含む一階述語論理の定理証明機である。マックス・プランク研究所が開発した。

主な技法

• 導出とユニフィケーション
• 項書き換え
• モデル検査
• 数学的帰納法
• 二分決定図
• DPLLアルゴリズム
• 分析的タブロー法

比較

名称	ライセンス	ウェブサービス	ライブラリ	スタンドアロン	バージョン	最新	作者	備考
ACL2	GPL v2	No	No	Yes	5.0	2012-8-23	Matt Kaufmann, J. Strother Moore	-
Prover9 / Mace4	GPLv2	No	Yes	Yes	v05	2009-11-04/	William McCune / アルゴンヌ国立研究所	-
Otter	パブリックドメイン	System on TPTPを使用	Yes	No	3.3f	2004-9	William McCune / Argonne National Laboratory	Prover9 / Mace4 が後継
j'Imp	?	No	No	Yes	-	2010-5-28	André Platzer	-
Metis	?	No	Yes	No	2.2	2010-5-24	Joe Hurd	-
Jape	?	Yes	Yes	No	1.0	2010-3-22	Adolfo Gustavo Neto, USP	-
PVS	?	No	Yes	No	4.2	2008-7	SRIインターナショナル	-
Leo II	?	System on TPTPを使用	Yes	Yes	1.2.8	2011	Christoph Benzmüller, Frank Theiss, Larry Paulson. ベルリン自由大学とケンブリッジ大学	-
EQP	?	No	Yes	No	0.9e	2009-5	William McCune / アルゴンヌ国立研究所	-
SAD	?	Yes	Yes	No	2.3-2.5	2008-8-27	Alexander Lyaletski, Konstantin Verchinine, Andrei Paskevich	-
PhoX	?	No	Yes	No	0.88.100524	-	Christophe Raffalli, Philippe Curmin, Pascal Manoury, Paul Roziere	-
KeYmaera	GPL	Java Web Startを使用	Yes	Yes	2.1	2012-5	André Platzer, Jan-David Quesel; Philipp Rümmer; David Renshaw	-
Gandalf	?	No	Yes	No	3.6	2009	Matt Kaufmann, J. Strother Moore, テキサス大学オースティン校	-
Tau	?	No	Yes	No	-	2005	Jay R. Halcomb, Randall R. Schulz, H&S Information Systems	-
E	GPL	System on TPTPを使用	No	Yes	E 1.4	2011-8-20	Stephan Schulz, ミュンヘン工科大学	-
SNARK	Mozilla Public License	No	Yes	No	snark-20080805r018b	2008	Mark E. Stickel	-
Vampire	?	System on TPTPを使用	Yes	Yes	Third re-incarnation Vampire	2011	Andrei Voronkov, Alexandre Riazanov, Krystof Hoder	-
Waldmeister	?	Yes	Yes	No	-	-	Thomas Hillenbrand, Bernd Löchner, Arnim Buch, Roland Vogt, Doris Diedrich	-
Saturate	?	No	Yes	No	2.5	1996-10	Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela	-
Theorem Proving System (TPS)	?	No	Yes	No	-	2004-6-24	カーネギーメロン大学	-
SPASS	?	Yes	Yes	Yes	3.7	2005-11	マックス・プランク研究所	-
IsaPlanner	GPL	No	Yes	Yes	IsaPlanner 2	2007	Lucas Dixon, Johansson Moa	-
KeY	GPL	Yes	Yes	Yes	1.6	2010-10	カールスルーエ大学, チャルマース工科大学, コブレンツ大学	-
Theorem Checker	?	Yes	No	No	0	2010	Robert J. Swartz, 北イリノイ大学	-
Princess	GPL	Java Web StartとSystem on TPTPを使用	Yes	Yes	2012-11-02	2012	Philipp Rümmer, ウプサラ大学	-

フリーソフトウェア

• Automath
• CVC
• IsaPlanner
• LCF
• LoTREC
• MetaPRL
• NuPRL
• Paradox
• Twelf
• SPARK (プログラミング言語)（英語版）
• Coq ※ 証明支援システム

プロプライエタリ

• Acumen RuleManager
• ALLIGATOR
• CARINE
• KIV
• Prover Plug-In
• ProverBox
• ResearchCyc

関連著名人

• ジャック・エルブラン - 自動定理証明の基本となるエルブランの定理の発見者
• Woody Bledsoe - 人工知能のパイオニア。
• Robert S. Boyer - ボイヤー-ムーア定理証明機（英語版）の開発者の1人。1999年エルブラン賞（英語版）を共同受賞。
• Alan Bundy - エディンバラ大学教授。帰納的証明のメタレベル推論で知られる。
• William McCune - アルゴンヌ国立研究所。初期の高性能自動定理証明機 Otter 開発者の1人。2000年 エルブラン賞受賞。
• Hubert Comon - CNRSを経てENS Cachan。多くの重要な論文で知られる。
• Robert Lee Constable - コーネル大学。型理論、NuPRLで知られる。
• Martin Davis - "Handbook of Artificial Reasoning" の著者。DPLLアルゴリズムの開発者の1人。2005年エルブラン賞受賞。
• Branden Fitelson - カリフォルニア大学バークレー校。論理系の最短の公理基盤発見の自動化。
• Harald Ganzinger - superposition calculus の開発者の1人。MPI Saarbrücken 代表。2004年、エルブラン賞を受賞。
• Michael Genesereth - スタンフォード大学教授。
• Michael J. C. Gordon - HOL theorem prover の開発責任者。
• Gérard Huet - 項書き換え、HOL。1998年、エルブラン賞受賞。
• Robert Kowalski - 連結グラフ定理証明機と論理プログラミングの推論エンジン SLD resolutionを開発。
• Donald W. Loveland - デューク大学。DPLLの開発者の1人。model eliminationの開発者。2001年 エルブラン賞を受賞。
• Norman Megill、自動証明された定理に関するデータベース metamath.orgの管理人。
• J Strother Moore - ボイヤー-ムーア定理証明機の開発者の1人。1999年 エルブラン賞を共同受賞。
• Ross Overbeek - アルゴンヌ国立研究所。The Fellowship for Interpretation of Genomes を設立。
• Lawrence C. Paulson - ケンブリッジ大学。高階論理システムの研究。Isabelle proof assistant の開発者の1人。
• J. Alan Robinson - シラキュース大学。独自の推論とユニフィケーション、ユニフィケーションに基づく一階定理証明を開発。"Handbook of Automated Reasoning" の著者。1996年、エルブラン賞受賞。
• John Rushby - SRIインターナショナル^[13]
• Jürgen Schmidhuber - Gödel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements を開発。
• Stephan Schulz - E theorem Prover を開発。
• Natarajan Shankar - SRIインターナショナル。PVS開発者の1人。
• Geoff Sutcliffe - マイアミ大学。TPTP collection の管理人、CADE コンテストの主催者。
• Dolph Ulrich - パデュー大学。論理系の最短の公理基盤発見の自動化。
• Robert Veroff - ニューメキシコ大学。多くの重要な論文で知られる。
• Andrei Voronkov - Vampire の開発者にして "Handbook of Automated Reasoning" の共編者。
• Larry Wos - アルゴンヌ国立研究所。多くの重要な論文で知られる。
• Wen-Tsun Wu - 幾何学定理証明 Wu's method を研究。1997年、エルブラン賞受賞。