Loading article…
コンピュータ科学、特に知識表現と推論、メタ論理の分野において、自動推論は推論の様々な側面を理解することに特化している。自動推論の研究は、コンピュータが完全に、あるいはほぼ完全に自動的に推論できるようなコンピュータプログラムの開発に役立つ。自動推論は人工知能の一分野とみなされているが、理論計算機科学や哲学とも関連がある。
自動推論の最も発展した分野は、自動定理証明（および自動化は低いが実用的な対話型定理証明の分野）と自動証明チェック（固定された仮定の下での正しい推論が保証されていると見なされる）である。帰納法とアブダクションを用いた類推による推論についても広範な研究が行われている。[ 1 ]
その他の重要なトピックとしては、不確実性下での推論や非単調推論などが挙げられる。不確実性分野の重要な部分の一つが議論であり、そこではより標準的な自動演繹に加えて、最小性や一貫性といった制約がさらに適用される。ジョン・ポロックのOSCARシステムは、単なる自動定理証明器にとどまらない、より具体的な自動議論システムの一例である。
自動推論のツールと技術には、古典論理と古典計算、ファジー論理、ベイズ推論、最大エントロピーによる推論、そして多くの非形式的なアドホックな技術が含まれる。
2020年代には、大規模言語モデルが複雑な問題を解決する能力を高めるために、AI研究者は、答えを生成する前に問題にさらに時間を費やすことができる推論言語モデル[ 2 ]や、幻覚を防ぐために記号推論システムを使用するニューロシンボリックアーキテクチャを設計しました。[ 3 ] [ 4 ] [ 5 ]
形式論理の発展は、自動推論の分野で大きな役割を果たし、それが人工知能の発展につながった。形式的証明とは、すべての論理的推論が数学の基本公理に照らして検証された証明である。すべての中間的な論理的ステップが例外なく示されている。直観から論理への変換がルーチンであっても、直観に頼ることはない。したがって、形式的証明は直観的ではなく、論理的誤りも起こりにくい。[ 6 ]
1957年にコーネル大学で開催された、多くの論理学者やコンピュータ科学者が集まった夏季会議を、自動推論、あるいは自動演繹の起源と考える人もいる。[ 7 ]一方、ニューウェル、ショー、サイモンによる1955年のLogic Theoristプログラム、あるいはマーティン・デイビスによる1954年のプレスバーガーの決定手続き（2つの偶数の和が偶数であることを証明したもの）の実装から始まったと言う人もいる。[ 8 ]
自動推論は、重要かつ人気のある研究分野であるにもかかわらず、80年代から90年代初頭にかけて「 AIの冬」を経験しました。しかし、その後この分野は復活しました。例えば、2005年にマイクロソフトは多くの社内プロジェクトで検証技術の使用を開始し、2012年版のVisual Cに論理仕様とチェック言語を含めることを計画しています。[ 7 ]
『プリンキピア・マテマティカ』は、アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルによって書かれた形式論理学の画期的な著作である。その目的は、すべての数学的表現または一部の数学的表現を記号論理の観点から導出することであった。『プリンキピア・マテマティカ』は、当初1910年、1912年、1913年に3巻で出版された。[ 9 ]これは、バートランド・ラッセルが1903年に著した『数学の原理』の後継書であり、ラッセルはこの中で有名なパラドックスを提示し、数学と論理学は同一であるというテーゼを主張した。
Logic Theorist (LT) は、1956 年にAllen Newell、Cliff Shaw、Herbert A. Simonによって開発された、定理の証明において「人間の推論を模倣する」最初のプログラムであり、Principia Mathematica の第 2 章の 52 の定理で実証され、そのうち 38 を証明しました。[ 10 ]定理を証明することに加えて、このプログラムは、ホワイトヘッドとラッセルが提供した証明よりも洗練された定理の 1 つの証明を見つけました。結果を公表しようと試みたものの失敗に終わった後、Newell、Shaw、Herbert は、1958 年に出版したThe Next Advance in Operation Researchで次のように報告しました。
形式的証明の例
自動推論は、自動定理証明器の構築に最も一般的に使用されてきました。しかし、多くの場合、定理証明器は効果的に機能するために人間のガイダンスを必要とするため、より一般的には証明支援器として分類されます。場合によっては、そのような証明器が定理を証明するための新しいアプローチを考案しています。Logic Theorist はその良い例です。このプログラムは、Principia Mathematicaの定理の 1 つについて、Whitehead と Russell が提供した証明よりも効率的な (より少ないステップで済む) 証明を考案しました。自動推論プログラムは、形式論理、数学、コンピュータ科学、論理プログラミング、ソフトウェアおよびハードウェア検証、回路設計、その他多くの分野で、ますます多くの問題を解決するために適用されています。TPTP (Sutcliffe と Suttner 1998)は、定期的に更新されるそのような問題のライブラリです。CADE 会議 (Pelletier、Sutcliffe と Suttner 2002) では、自動定理証明器のコンペティションが定期的に開催されています。競技の問題はTPTPライブラリから選ばれます。[ 20 ]