自動定理証明

時は一九五〇年代。まだ計算機科学という分野が産声を上げたばかりの頃、アレン・ニューウェルとハーバード・サイモンという二人の研究者が、後の世に大きな影響を与える画期的なプログラムを開発しました。その名は「ロジック・セオリスト」。このプログラムは、それまでの計算機とは一線を画す、まるで人間のように論理的に考え、数学の定理を証明することができたのです。 当時、計算機はもっぱら膨大な数の計算を高速で行うための道具と見なされていました。複雑な計算を瞬時に行えるその能力は確かに驚異的でしたが、あくまで人間の指示に従って動くだけの存在であり、自ら考えて問題を解くことは夢物語でした。そんな時代に登場したロジック・セオリストは、機械が人間の思考過程を模倣できることを初めて示した、まさに人工知能研究における記念碑と言えるでしょう。 ロジック・セオリストは、ホワイトヘッドとラッセルの数学の基礎に関する本「プリンキピア・マテマティカ」に載っている定理をいくつか証明してみせ、当時の学会を騒然とさせました。まるで人間のように論理を組み立て、複雑な問題を解くその能力は、多くの人々に衝撃を与えました。機械が自ら考え、問題を解くという、かつては想像の域を出なかったことが現実のものとなったのです。 この出来事は、単に計算機科学の世界だけにとどまらず、広く社会全体にも大きな影響を及ぼしました。ロジック・セオリストの成功は、人間のように考える機械、すなわち「思考機械」の実現可能性を初めて示しただけでなく、人間の知能そのものについても新たな視点を与えてくれるものでした。そして、この画期的なプログラムの誕生は、後に続く人工知能研究の礎となり、今日の目覚ましい発展へと繋がる第一歩となったのです。