自動推論

コンピュータサイエンス、特に知識表現と推論およびメタロジックにおいて、自動推論の分野は推論のさまざまな側面を理解することに専念しています。自動推論の研究は、コンピュータが完全に、またはほぼ完全に自動的に推論できるようにするコンピュータプログラムの作成に役立ちます。自動推論は人工知能のサブフィールドと見なされていますが、理論コンピュータサイエンスや哲学とも関連があります。

自動推論の最も発達したサブ領域は、自動定理証明（およびそれほど自動化されていないがより実用的なサブフィールドである対話型定理証明）と自動証明チェック（固定された仮定の下での正しい推論が保証されていると見なされる）である。^{[要出典]また、}帰納法と帰納法を使用した類推による推論についても広範な研究が行われてきた。^[1]

その他の重要なトピックには、不確実性の下での推論と非単調推論が含まれます。不確実性分野の重要な部分は議論であり、ここでは、より標準的な自動演繹に加えて、最小性と一貫性のさらなる制約が適用されます。ジョン・ポロックのOSCARシステム^[2]は、単なる自動定理証明器よりも具体的な自動議論システムの例です。

自動推論のツールと手法には、古典的な論理と計算、ファジー論理、ベイズ推論、最大エントロピーによる推論、およびそれほど形式的ではない多くのアドホック手法が含まれます。

形式論理の発展は自動推論の分野で大きな役割を果たし、それ自体が人工知能の発展につながりました。形式的証明とは、すべての論理的推論が数学の基本公理に照らして検証された証明です。中間の論理的ステップはすべて例外なく提供されます。直感から論理への変換が日常的であっても、直感に頼ることはありません。したがって、形式的証明は直感的ではなく、論理的エラーの影響を受けにくいです。^[3]

自動推論、あるいは自動演繹の起源は、多くの論理学者やコンピュータ科学者が集まった1957年のコーネル大学夏季会議だと考える人もいます。^[4]また、それ以前に、ニューウェル、ショー、サイモンによる1955年の論理理論プログラム、あるいはマーティン・デイビスによる1954年のプレスバーガーの決定手順（2つの偶数の和は偶数であることを証明した）の実装から始まったと言う人もいます。^[5]

自動推論は、重要かつ人気のある研究分野であるにもかかわらず、80年代から90年代初頭にかけて「 AIの冬」を経験しました。しかし、その後この分野は復活しました。たとえば、2005年にマイクロソフトは多くの社内プロジェクトで検証技術を使用し始め、2012年版のVisual Cに論理仕様とチェック言語を組み込む予定です。^[4]

『プリンキピア・マテマティカ』は、アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルによって書かれた形式論理学の画期的な著作である。 『プリンキピア・マテマティカ』は数学原理とも呼ばれ、数式の一部または全部を記号論理学の観点から導く目的で書かれた。『プリンキピア・マテマティカ』は、1910年、1912年、1913年に3巻で最初に出版された。 ^[6]

ロジック・セオリスト（LT）は、1956年にアレン・ニューウェル、クリフ・ショー、ハーバート・A・サイモンによって開発された、定理を証明する際に「人間の推論を模倣する」史上初のプログラムであり、プリンキピア・マテマティカの第2章の52の定理で実証され、そのうち38の定理を証明しました。 ^[7]定理を証明することに加えて、プログラムはホワイトヘッドとラッセルが提供したものよりもエレガントな定理の1つを見つけました。結果を発表する試みが失敗した後、ニューウェル、ショー、ハーバートは1958年に出版物「オペレーション・リサーチの次の進歩」で次のように報告しました。

「今や世界には、考え、学び、創造する機械が存在する。さらに、これらの能力は急速に向上し、（近い将来には）機械が扱える問題の範囲は、人間の頭脳が適用してきた範囲と同等になるだろう。」^[8]

形式的証明の例

ボイヤー・ムーア定理証明器 (NQTHM)

NQTHMの設計は、John McCarthy と Woody Bledsoe の影響を受けています。1971 年にスコットランドのエディンバラで開始されたこのシステムは、Pure Lisp を使用して構築された完全自動定理証明器でした。NQTHM の主な特徴は次のとおりです。

1. 実用的なロジックとしての Lisp の使用。
2. 全再帰関数の定義の原理への依存。
3. 書き換えと「記号評価」の広範な使用。
4. 記号評価の失敗に基づく帰納的ヒューリスティック^{[13] [14]}

HOLライト

OCamlで書かれたHOL Lightは、シンプルでクリーンな論理基盤とすっきりとした実装を持つように設計されています。本質的には、古典的な高階論理のもう一つの証明支援ツールです。^[15]

コック

フランスで開発されたCoqは、仕様から実行可能なプログラムをObjective CAMLまたはHaskellソースコードとして自動的に抽出できるもう1つの自動証明支援ツールです。プロパティ、プログラム、証明は、帰納的構成の計算（CIC）と呼ばれる同じ言語で形式化されています。^[16]

自動推論は、自動定理証明器の構築に最も一般的に使用されています。ただし、定理証明器が効果を発揮するには人間による指導が必要になることが多く、より一般的には証明アシスタントと呼ばれます。場合によっては、このような証明器が定理を証明する新しいアプローチを考案しました。Logic Theorist はその良い例です。このプログラムは、Principia Mathematicaの定理の 1 つに対して、Whitehead と Russell が提供した証明よりも効率的 (必要な手順が少ない) な証明を考案しました。自動推論プログラムは、形式論理、数学とコンピューター サイエンス、論理プログラミング、ソフトウェアとハ​​ードウェアの検証、回路設計など、ますます多くの問題を解決するために適用されています。TPTP (Sutcliffe と Suttner 1998) は、定期的に更新されるこのような問題のライブラリです。CADEカンファレンスでは、自動定理証明器のコンテストも定期的に開催されている（Pelletier、Sutcliffe、Suttner 2002）。コンテストの問題はTPTPライブラリから選ばれる。^[17]

• 自動機械学習（AutoML）
• 自動定理証明
• 推論システム
• セマンティック推論
• プログラム分析（コンピュータサイエンス）
• 人工知能の応用
• 人工知能の概要
• ケーススタディ•事例に基づく推論
• 帰納的推論
• 推論エンジン
• 常識的な推論

• 自動推論に関する国際合同会議(IJCAR)
• 自動控除に関する会議(CADE)
• 分析的タブローと関連手法による自動推論に関する国際会議

• 自動推論ジャーナル

• 自動推論協会(AAR)

• ロジックの実装に関する国際ワークショップ
• 自動推論における実証的に成功したトピックに関するワークショップシリーズ