自動推論

自動推論（じどうすいろん、Automated Reasoning）は計算機科学と数理論理学の一分野であり、推論の様々な側面を理解することでコンピュータによる完全（あるいはほぼ完全）自動な推論を行うソフトウェアを開発することを目的とする。人工知能研究の一部と考えられるが、理論計算機科学や哲学とも深い関係がある。

自動推論のなかでも最も研究が進んでいるのは、自動定理証明（および完全自動ではないがより現実的な）と（固定の前提条件下での推論と見なすことができる）であるが、他にも類推、帰納、アブダクションによる推論の研究も盛んである。他の重要なトピックとしては、不確かさのある状況での推論と非単調推論である。不確かさに関する研究では論証（argumentation）が重要である。それはすなわち、標準的な自動推論へのさらなる極小性と一貫性の適用である。John Pollock の Oscar システムは単なる自動定理証明機よりも自動論証システムといえるものである。

自動推論のツールや手法としては、古典的論理学や代数学があるが、他にもファジィ論理、ベイズ推定、最大エントロピー原理に基づく推論、その他のあまり形式的でない技法などがある。

歴史数理論理学の発展は自動推論の分野で大きな役割を果たし、自動推論自体も人工知能の発展に寄与した。形式的証明 (formal proof) は、すべての論理的結論を基本的な数学の公理にまで遡ってチェックした証明である。すべての中間的な論理段階が示され、例外はない。直観から論理への変換が普通であっても、直観にたよることはない。したがって形式的証明は直観的ではなく、論理的誤りも少ない。

1957年、多くの論理学者と計算機科学者が一堂に会した Cornell Summer が自動推論または自動定理証明の起源とされることがある。それ以前のアレン・ニューウェル、クリフ・ショー、ハーバート・サイモンらが1955年に開発した Logic Theorist や、マーチン・デービスが1954年にプレスブルガーの決定手続きを実装したもの（2つの偶数の和が偶数であることを証明）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が起源だとすることもある。自動推論は重要な領域として盛んに研究が行われていたが、1980年代から90年代初頭の「AIの冬」の時代を経験し、その後運よく復興した。例えば2005年、マイクロソフトは多くの社内プロジェクトでのソフトウェア開発に検証技術を使い始め、Visual C++ の2012年版に論理的に検証する機能を追加した。

重要な貢献アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルの『プリンキピア・マテマティカ』（数学原理）は数理論理学の画期をなした著作であり、あらゆる数式を論理によって導出することを目的として書かれた。同書は3巻に分かれており、それぞれ1910年、1912年、1913年に出版された。

Logic Theorist (LT) は1956年、アレン・ニューウェル、クリフ・ショー、ハーバート・サイモンが開発した人間の行う推論を真似て定理を証明するプログラムであり、『プリンキピア・マテマティカ』の第2章にある52の定理のうち38を証明してみせた。さらに言えば、単に証明しただけでなく、そのうちの1つはホワイトヘッドとラッセルが示した証明よりも洗練されていた。彼らは1958年にその成果を The Next Advance in Operation Research にて発表した。

+ 形式的証明の例年定理証明系形式化した人もともと証明した人 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により論理を構築すべてを再帰関数で定義することを基本としている。「記号評価」と書き換えを多用。記号評価の失敗に基づいた帰納的ヒューリスティックを使用 HOL Light OCamlで書かれており、論理的基盤が単純かつ明快になるよう設計され、実装もきれいである。古典的高階論理の証明を支援する。 Coq フランスで開発された証明支援システムで、仕様記述から実行可能なプログラムを自動生成できる（生成するソースコードはOCamlまたはHaskell）。仕様記述や証明の記述に使われる言語は Calculus of Inductive Constructions (CIC) と呼ばれている。

応用自動推論の最大の応用は自動定理証明機の構築である。時にはそういった証明機が定理の新たな証明方法をもたらすこともあり、Logic Theorist がよい例である。自動推論プログラムは、論理学、数学、計算機科学、論理プログラミング、ソフトウェアおよびハードウェアの設計検証、回路設計など様々な分野の問題を解くのに利用されている。TPTPはそういった問題を集めたライブラリであり、定期的に更新されている。また、CADEという学会で定期的に自動定理証明機の競技会が開催されており、競技会で使用する問題はTPTPライブラリから選ばれている。

脚注

Źródło i licencja