形式的推論
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2022/03/08 08:13 UTC 版)
人工知能は、人間の思考過程を機械で再現できるという前提に基づいている。機械的あるいは形式的推論の歴史は長い。中国、インド、ギリシアの哲学者らは、いずれも紀元前に形式的推論の構造化された手法を発展させた。その発展に寄与した哲学者としては、アリストテレス(三段論法を定式化して分析した)、エウクレイデス(その『原論』は形式的推論の原型となった)、フワーリズミー(代数学を発展させ、その名は「アルゴリズム」として残っている)、ヨーロッパスコラ学の哲学者であるオッカムのウィリアムとヨハネス・ドゥンス・スコトゥスなどが挙げられる。 マジョルカ人哲学者ラモン・リュイ (1232–1315) は論理的方法で知識を生み出すことを意図した「論理機械」をいくつか開発した。リュイは自身の機械について、単純な論理操作で基本的かつ紛れもない真理を結合する機械的要素群であり、機械的手段で生み出された真理が考えられるあらゆる知識を生み出すとした。リュイの業績はゴットフリート・ライプニッツに大きな影響を及ぼした。 17世紀になると、ライプニッツ、トマス・ホッブズ、ルネ・デカルトらはあらゆる理性的思考は代数学や幾何学のように体系化できるのではないかという可能性を探究した。ホッブズは『リヴァイアサン』で「推論は計算以外のなにものでもない」と記している。ライプニッツは推論のための汎用言語 (characteristica universalis) を想像し、論証を計算に還元しようと考えた。それによって「2人の哲学者の論争は2人の会計士の論争程度のことになる。彼らは論証を石版に書き記し(必要な友人を証人に立て)『計算』してみればよい」とした。これらの哲学者の考え方から物理記号システム(英語版)仮説が明確化していき、それがAI研究の指針となった。 20世紀になると、数理論理学の研究が人工知能の実現可能性への根本的なブレークスルーを提供する。その基盤となったのは、ブールの The Laws of Thought とフレーゲの『概念記法』である。フレーゲの体系に基づき、1913年、ラッセルとホワイトヘッドが重要な著作『プリンキピア・マテマティカ』において数学的基礎の形式的記述を行った。ラッセルの成果に触発されたダフィット・ヒルベルトは、当時の数学者らに「数学におけるあらゆる推論は形式化できるか?」という根本的問題を提示した(ヒルベルト・プログラム)。この問題への解答が、ゲーデルの不完全性定理、チューリングの機械、チャーチのラムダ計算である。その解答は2つの意味で驚くべきものだった[要出典]。第一に彼らは数理論理が成し遂げられることには限界があることを証明した[要出典]。 詳細は「ゲーデルの不完全性定理#誤解(哲学等による誤解・誤用)」、「不完全性定理が成立しない体系」、および「ゲーデルの完全性定理」を参照 @media screen{.mw-parser-output .fix-domain{border-bottom:dashed 1px}}第二に(こちらがAIにとっては重要)、彼らの業績が意味するのは、その限界の中でなら任意の数学的推論を機械化できるという事実だった[要出典]。チャーチ=チューリングのテーゼでは、0と1といった単純な記号群だけで任意の数学的推論過程を模倣できることが暗示されている。鍵となる洞察はチューリングマシンであり、記号操作を抽象化した単純な理論上の機械である。チューリングマシンは一部の科学者が思考する機械の可能性を議論しはじめるきっかけとなった。
※この「形式的推論」の解説は、「人工知能の歴史」の解説の一部です。
「形式的推論」を含む「人工知能の歴史」の記事については、「人工知能の歴史」の概要を参照ください。
- 形式的推論のページへのリンク