自動定理証明

提供: miniwiki
移動先:案内、検索
ファイル:ANL-E aerial 22037k4.jpg
アルゴンヌ国立研究所は1960年代以降2000年代まで、自動定理証明のリーダーだった。

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

歴史

論理学的背景

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

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

最初の実装

第二次世界大戦後、第一世代のコンピュータが登場。1954年、マーチン・デービス（English版）がプリンストン高等研究所にて真空管コンピュータJOHNNIAC（English版）上にプレスブルガーのアルゴリズムを実装した。デービスによれば「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 で優勝している）。

主な技法

比較

名称 ライセンス ウェブサービス ライブラリ スタンドアロン バージョン 最新 作者 備考
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, ウプサラ大学 -

フリーソフトウェア

プロプライエタリ

関連著名人

脚注

  1. ↑ Frege, Gottlob (1879). Begriffsschrift. Verlag Louis Neuert. 
  2. ↑ Frege, Gottlob (1884). Die Grundlagen der Arithmetik. Breslau: Wilhelm Kobner. 
  3. ↑ Bertrand Russell; Alfred North Whitehead (1910-1913). Principia Mathematica, 1st, Cambridge University Press. 
  4. ↑ Bertrand Russell; Alfred North Whitehead (1927). Principia Mathematica, 2nd, Cambridge University Press. 
  5. ↑ Herbrand, Jaques (1930). Recherches sur la théorie de la démonstration. 
  6. ↑ Presburger, Mojżesz (1929). “Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt”. Comptes Rendus du I congrès de Mathématiciens des Pays Slaves (Warszawa): 92–101. 
  7. ↑ 7.0 7.1 7.2 7.3 Davis, Martin (2001), “The Early History of Automated Deduction”, in Robinson, Alan; Voronkov, Andrei, Handbook of Automated Reasoning, 1, Elsevier, http://cs.nyu.edu/cs/faculty/davism/early.ps )
  8. ↑ Bibel, Wolfgang (2007). “Early History and Perspectives of Automated Deduction”. KI 2007. LNAI (Springer) (4667): 2–18. http://www.intellektik.de/resources/OsnabrueckBuchfassung.pdf . 2012閲覧.. 
  9. ↑ Gilmore, Paul (1960). “A proof procedure for quantification theory: its justification and realisation”. IBM Journal of Research and Development 4: 28–35. 
  10. ↑ W.W. McCune (1997). “Solution of the Robbins Problem”. Journal of Automated Reasoning 19 (3). http://www.springerlink.com/content/h77246751668616h/. 
  11. ↑ Gina Kolata (1996年12月10日). “Computer Math Proof Shows Reasoning Power”. The New York Times. http://www.nytimes.com/library/cyber/week/1210math.html . 2008閲覧. 
  12. ↑ Sutcliffe, Geoff. “The TPTP Problem Library for Automated Theorem Proving”. . 2012閲覧.
  13. ↑ “SRI International Computer Science Laboratory - John Rushby”. SRI International. . 22 September 2012閲覧.

参考文献

関連項目

外部リンク



「http:///http:///mymemo.xyz/mymemo.xyz/wiki/index.php?title=自動定理証明&oldid=110375」から取得