自動推論
自動推論︵じどうすいろん、Automated Reasoning︶は計算機科学と数理論理学の一分野であり、推論の様々な側面を理解することでコンピュータによる完全︵あるいはほぼ完全︶自動な推論を行うソフトウェアを開発することを目的とする。人工知能研究の一部と考えられるが、理論計算機科学や哲学とも深い関係がある。
自動推論のなかでも最も研究が進んでいるのは、自動定理証明︵および完全自動ではないがより現実的な対話型定理証明︶と自動定理検証︵固定の前提条件下での推論と見なすことができる︶であるが、他にも類推、帰納、アブダクションによる推論の研究も盛んである。他の重要なトピックとしては、不確かさのある状況での推論と非単調推論である。不確かさに関する研究では論証︵argumentation︶が重要である。それはすなわち、標準的な自動推論へのさらなる極小性と一貫性の適用である。John Pollock の Oscar システムは単なる自動定理証明機よりも自動論証システムといえるものである。
自動推論のツールや手法としては、古典的論理学や代数学があるが、他にもファジィ論理、ベイズ推定、最大エントロピー原理に基づく推論、その他のあまり形式的でない技法などがある。
歴史
編集
数理論理学の発展は自動推論の分野で大きな役割を果たし、自動推論自体も人工知能の発展に寄与した。形式的証明 (formal proof) は、すべての論理的結論を基本的な数学の公理にまで遡ってチェックした証明である。すべての中間的な論理段階が示され、例外はない。直観から論理への変換が普通であっても、直観にたよることはない。したがって形式的証明は直観的ではなく、論理的誤りも少ない[1]。
1957年、多くの論理学者と計算機科学者が一堂に会した Cornell Summer が自動推論または自動定理証明の起源とされることがある[2]。それ以前のアレン・ニューウェル、クリフ・ショー、ハーバート・サイモンらが1955年に開発した Logic Theorist や、マーチン・デービスが1954年にプレスブルガーの決定手続きを実装したもの︵2つの偶数の和が偶数であることを証明︶[3]が起源だとすることもある。自動推論は重要な領域として盛んに研究が行われていたが、1980年代から90年代初頭の﹁AIの冬﹂の時代を経験し、その後運よく復興した。例えば2005年、マイクロソフトは多くの社内プロジェクトでのソフトウェア開発に検証技術を使い始め、Visual C++ の2012年版に論理的に検証する機能を追加した[2]。
重要な貢献
編集
アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルの﹃プリンキピア・マテマティカ﹄︵数学原理︶は数理論理学の画期をなした著作であり、あらゆる数式を論理によって導出することを目的として書かれた。同書は3巻に分かれており、それぞれ1910年、1912年、1913年に出版された[4]。
Logic Theorist (LT) は1956年、アレン・ニューウェル、クリフ・ショー、ハーバート・サイモンが開発した人間の行う推論を真似て定理を証明するプログラムであり、﹃プリンキピア・マテマティカ﹄の第2章にある52の定理のうち38を証明してみせた[5]。さらに言えば、単に証明しただけでなく、そのうちの1つはホワイトヘッドとラッセルが示した証明よりも洗練されていた。彼らは1958年にその成果を The Next Advance in Operation Research にて発表した。
今や世界には思考し、学習し、創造する機械が存在する。さらに、それらの能力は︵近い将来︶急速に適用範囲を広げようとしており、それと共に人の精神が扱える範囲も広がっていく。[6]
| 年 | 定理 | 証明系 | 形式化した人 | もともと証明した人 |
|---|---|---|---|---|
| 1986 | 第1不完全性定理 | Boyer- Moore | Shankar | ゲーデル |
| 1990 | 平方剰余の相互法則 | Boyer- Moore | Russinoff | アイゼンシュタイン |
| 1996 | 微分積分学の基本定理 | HOL Light | Harrison | Henstock |
| 2000 | 代数学の基本定理 | Mizar | Milewski | Brynski |
| 2000 | 代数学の基本定理 | Coq | Geuvers 他 | クネーザー |
| 2004 | 四色定理 | Coq | Gonthier | ロバートソン他 |
| 2004 | 素数定理 | Isabelle | Avigad 他 | セルバーグ-エルデシュ |
| 2005 | ジョルダン曲線定理 | HOL Light | Hales | Thomassen |
| 2005 | ブラウワーの不動点定理 | HOL Light | Harrison | Kuhn |
| 2006 | Flyspeck 1 | Isabelle | Bauer- Nipkow | Hales |
| 2007 | コーシーの留数定理 | HOL Light | Harrison | 古典的 |
| 2008 | 素数定理 | HOL Light | Harrison | 解析的証明 |
| 2012 | Feit–Thompsonの定理 | Coq | Gonthier 他 | Bender, Glauberman, Peterfalvi |
主な証明システム
編集
Boyer-Moore Theorem Prover (Nqthm)
LISPで構築された完全自動の定理証明機。ジョン・マッカーシーと Woody Bledsoe の影響を受けた設計である。1971年、スコットランドのエジンバラで開発が始まった。次のような特徴がある。
(一)LISPにより論理を構築
(二)すべてを再帰関数で定義することを基本としている。
(三)﹁記号評価﹂と書き換えを多用。
(四)記号評価の失敗に基づいた帰納的ヒューリスティックを使用[7]
HOL Light
OCamlで書かれており、論理的基盤が単純かつ明快になるよう設計され、実装もきれいである。古典的高階論理の証明を支援する[8]。
Coq
フランスで開発された証明支援システムで、仕様記述から実行可能なプログラムを自動生成できる︵生成するソースコードはOCamlまたはHaskell︶。仕様記述や証明の記述に使われる言語は Calculus of Inductive Constructions (CIC) と呼ばれている[9]。
応用
編集脚注
編集
(一)^ Thomas, C. Hales. “Formal Proof”. University of Pittsburgh. 2010年10月19日閲覧。
(二)^ ab“Automated Deduction (AD)”. The Nature of PRL Project. 2010年10月19日閲覧。
(三)^ Martin Davis, "The Prehistory and Early History of Automated Deduction," in Automation of Reasoning, eds. Siekmann and Wrightson, vol. 1, 1-28 at p. 15
(四)^ “Principia Mathematica”. Stanford University. 2010年10月19日閲覧。
(五)^ “The Logic Theorist and its Children”. 2010年10月18日閲覧。
(六)^ Shankar, Natarajan. “Little Engines of Proof”. Computer Science Laboratory, SRI International. 2010年10月19日閲覧。
(七)^ “The Boyer- Moore Theorem Prover”. 2010年10月23日閲覧。
(八)^ Harrison, John. “HOL Light: an overview”. 2010年10月23日閲覧。
(九)^ “Introduction to Coq”. 2010年10月23日閲覧。
(十)^ “Automated Reasoning”. Stanford Encyclopedia. 2010年10月10日閲覧。
関連項目
編集外部リンク
編集学術会議とワークショップ
編集- International Joint Conference on Automated Reasoning (IJCAR)
- Conference on Automated Deduction (CADE)
- International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX)
- International Workshop on the Implementation of Logics
- Workshop Series on Empirically Successful Topics in Automated Reasoning
学会と学会誌
編集Association for Automated Reasoning（AAR、自動推論学会）は以下の学会誌を出している。