نظریه پرداز منطقی

نظریه پرداز منطقی (منطق‌دان) یک برنامه کامپیوتری است که در سال ۱۹۵۶ توسط آلن نیوئل، هربرت ای. سایمون، و کلیف شا نوشته شد. این برنامه اولین برنامه‌ای بود که به طور عمدی برای انجام استدلال خودکار طراحی شده بود و به عنوان «اولین برنامه هوش مصنوعی» توصیف شده است. منطق‌دان ۳۸ قضیه از ۵۲ قضیه اول در فصل دوم کتاب مبادی ریاضیات نوشته وایت‌هد و برتراند راسل را اثبات کرد و برای برخی از آنها اثبات‌های جدید و کوتاه‌تری پیدا کرد.

تاریخچه

در سال ۱۹۵۵، زمانی که نیوئل و سایمون شروع به کار بر روی نظریه پرداز منطقی کردند، حوزه هوش مصنوعی هنوز وجود نداشت. حتی خود اصطلاح "هوش مصنوعی" نیز تا تابستان سال بعد ابداع نشده بود.

سایمون یک دانشمند علوم سیاسی بود که پیش از این، کارهای کلاسیکی در زمینه مطالعه چگونگی عملکرد بروکراسی‌ها انجام داده بود و همچنین نظریه عقلانیت محدود خود را توسعه داده بود (که بعدها برای آن برنده جایزه نوبل شد). مطالعه سازمان‌های تجاری، همانند هوش مصنوعی، نیازمند بینش در مورد ماهیت حل مسئله و تصمیم‌گیری انسانی است. سایمون به یاد می‌آورد که در اوایل دهه ۱۹۵۰ در شرکت RAND مشاوره می‌داد و مشاهده کرد که یک چاپگر با استفاده از حروف و علائم نگارشی معمولی، نقشه‌ای را تایپ می‌کند. او متوجه شد که یک ماشینی که بتواند نمادها را دستکاری کند، به همان اندازه می‌تواند تصمیم‌گیری را شبیه‌سازی کند و حتی ممکن است فرایند تفکر انسانی را نیز شبیه‌سازی کند.

برنامه‌ای که نقشه را چاپ کرده بود، توسط نیوئل، یک دانشمند شرکت RAND که در حال مطالعه لجستیک و نظریه سازمان بود، نوشته شده بود. برای نیوئل، لحظه تعیین‌کننده در سال ۱۹۵۴ بود، زمانی که الیور سلفریج به شرکت RAND آمد تا کار خود را در زمینه تطبیق الگو توصیف کند. با تماشای این ارائه، نیوئل ناگهان فهمید که چگونه تعامل واحدهای ساده و قابل برنامه‌ریزی می‌تواند رفتار پیچیده‌ای از جمله رفتار هوشمندانه انسان‌ها را انجام دهد. او بعدها گفت: "همه اینها در یک بعدازظهر اتفاق افتاد." این یک لحظه نادر از روشن‌بینی علمی بود.

"چنان حس روشنی داشتم که این یک مسیر جدید است و من قصد دارم آن را دنبال کنم. این حس را خیلی زیاد تجربه نکرده‌ام. معمولاً آدم شکاکی هستم و به راحتی هیجان‌زده نمی‌شوم، اما در این مورد شدم. کاملاً در آن غرق شده بودم - بدون اینکه با دو یا سه سطح از آگاهی وجود داشته باشم که همزمان در حال کار باشی، و آگاه باشی که در حال کار هستی، و از عواقب و مفاهیم آن آگاه باشی، حالت معمول فکر کردن. نه. کاملاً برای ده تا دوازده ساعت غرق آن شده بودم."

نیوئل و سایمون شروع به صحبت درباره امکان آموزش دادن ماشین‌ها برای فکر کردن کردند. اولین پروژه آن‌ها برنامه‌ای بود که می‌توانست قضایای ریاضی را مانند آن‌هایی که در کتاب مبادی ریاضیات برتراند راسل و آلفرد نورث وایت‌هد استفاده شده بود، اثبات کند. آن‌ها از کلیف شا، برنامه‌نویس کامپیوتر از شرکت RAND، برای توسعه این برنامه کمک گرفتند. (نیوئل می‌گوید "کلیف تنها دانشمند واقعی کامپیوتر از بین ما سه نفر بود"). نسخه اول به صورت دستی شبیه‌سازی شده بود: آن‌ها برنامه را روی کارت‌های 3x5 نوشتند و به گفته سایمون:

"در ژانویه ۱۹۵۶، من همسر و سه فرزندم را همراه با چند دانشجوی تحصیلات تکمیلی جمع کردیم. به هر عضو گروه یکی از کارت‌ها را دادیم، به طوری که هر یک از آن‌ها به نوعی بخشی از برنامه کامپیوتری شد... اینجا طبیعت از هنر تقلید می‌کرد که خود از طبیعت تقلید می‌کرد."

آن‌ها موفق شدند نشان دهند که برنامه می‌تواند به خوبی یک ریاضی‌دان با استعداد، قضایا را اثبات کند. در نهایت، شا توانست برنامه را بر روی کامپیوتر در مرکز RAND در سانتا مونیکا اجرا کند. در تابستان ۱۹۵۶، جان مک‌کارتی، ماروین مینسکی، کلود شانون و ناتان روچستر کنفرانسی در مورد موضوعی که آن را "هوش مصنوعی" نامیدند (اصطلاحی که مک‌کارتی برای این مناسبت ابداع کرد) سازماندهی کردند. نیوئل و سایمون با افتخار برنامه منطق‌دان را به گروه معرفی کردند. این برنامه با استقبال ملایمی روبرو شد. پاملا مک‌کوردوک می‌نویسد: "شواهد نشان می‌دهد که هیچ‌کس به جز نیوئل و سایمون خودشان به اهمیت بلندمدت کاری که انجام می‌دادند پی نبرد." سایمون اذعان می‌کند که "احتمالاً ما در این مورد نسبتاً متکبر بودیم" و اضافه می‌کند:

"آن‌ها نمی‌خواستند از ما چیزی بشنوند و ما هم مطمئناً نمی‌خواستیم از آن‌ها چیزی بشنویم: ما چیزی برای نشان دادن به آن‌ها داشتیم!... از یک جهت این موضوع طعنه‌آمیز بود زیرا ما قبلاً اولین نمونه از چیزی که آن‌ها دنبال آن بودند را انجام داده بودیم؛ و دوم اینکه آن‌ها به آن توجه چندانی نکردند."

منطق‌دان به سرعت ۳۸ قضیه از ۵۲ قضیه اول در فصل دوم کتاب مبادی ریاضیات را اثبات کرد. اثبات قضیه ۲.۸۵ در واقع برازنده‌تر از اثباتی بود که به‌سختی توسط راسل و وایت‌هد اثبات شده بود. سایمون توانست اثبات جدید را به خود راسل نشان دهد که "با خوشحالی پاسخ داد". آن‌ها تلاش کردند تا اثبات جدید را در مجله منطق نمادین منتشر کنند، اما مقاله به این دلیل رد شد که اثبات جدید یک قضیه ریاضی ابتدایی قابل توجه نیست، و ظاهراً این واقعیت که یکی از نویسندگان یک برنامه کامپیوتری بود را نادیده گرفتند.

نیوئل و سایمون یک همکاری پایدار شکل دادند و یکی از اولین آزمایشگاه‌های هوش مصنوعی را در دانشگاه کارنگی ملون تأسیس کردند و یک سری از برنامه‌ها و ایده‌های تأثیرگذار هوش مصنوعی را توسعه دادند، از جمله حل‌کننده مسئله عمومی، Soar ، و نظریه یکپارچه شناخت.

ساختار

این یک ارائه مختصر بر اساس این است که نظریه پرداز منطقی یک برنامه است که فرآیندهای منطقی را بر روی عبارات منطقی انجام می‌دهد.

عبارات

• یک عبارت از عناصر تشکیل شده است.

• دو نوع حافظه وجود دارد: حافظه کاری و حافظه ذخیره‌سازی.

• هر حافظه کاری حاوی یک عنصر واحد است. منطق‌دان معمولاً از ۱ تا ۳ حافظه کاری استفاده می‌کند.

• هر حافظه ذخیره‌سازی یک لیست است که نمایانگر یک عبارت کامل یا مجموعه‌ای از عناصر است. به‌ویژه، حاوی تمام اصول و قضایای منطقی اثبات شده است.

• یک عبارت یک درخت نحو انتزاعی است که هر گره آن یک عنصر با حداکثر ۱۱ ویژگی است.

برای مثال، عبارت منطقی P→(Q∧¬P)¬ به صورت یک درخت نمایش داده می‌شود که ریشه آن نشان‌دهنده → است. ویژگی‌های ریشه شامل اشاره‌گرهایی به دو عنصر زیرعبارت‌های P¬ و Q∧¬P می‌باشد.

فرایندها

چهار نوع فرآیند وجود دارد، از پایین‌ترین تا بالاترین سطح.

• دستور: این‌ها مشابه کد مونتاژ هستند. ممکن است یک عملیات ابتدایی را بر روی یک عبارت در حافظه کاری انجام دهند یا به یک دستور پیش‌شرطی بروند. مثالی از این نوع فرآیند: "زیر عنصر راست حافظه کاری ۱ را به حافظه کاری ۲ بگذار".

• فرآیند ابتدایی: این‌ها مشابه زیربرنامه‌ها هستند. یک دنباله از دستورالعمل‌ها که می‌توانند فراخوانی شوند.
• روش: یک دنباله از فرآیندهای ابتدایی. فقط ۴ روش وجود دارد:

1. جایگذاری: با داشتن یک عبارت، سعی می‌کند آن را با جایگذاری متغیرها و اتصالات منطقی به یک قضیه یا اصل اثبات‌شده تبدیل کند.
2. جداشدگی: با داشتن عبارت B، سعی می‌کند قضیه یا اصل اثبات‌شده‌ای به شکل 'A→B را پیدا کند، که در آن 'B ، پس از جایگذاری، به B منتهی شود. سپس سعی می‌کند A را با جایگذاری اثبات کند.
3. زنجیره‌سازی به جلو: با داشتن عبارت A→C، سعی می‌کند یک قضیه یا اصل اثبات‌شده به شکل A→B را پیدا کند، سپس سعی می‌کند B→C را با جایگذاری اثبات کند.
4. زنجیره‌سازی به عقب: با داشتن عبارت A→C، سعی می‌کند یک قضیه یا اصل اثبات‌شده به شکل B→C را پیدا کند، سپس سعی می‌کند A→B را با جایگذاری اثبات کند.

• روش کنترل اجرایی: این روش هر یک از این ۴ روش را به ترتیب به هر قضیه‌ای که باید اثبات شود، اعمال می‌کند.

تاثیر نظریه پرداز منطقی بر هوش مصنوعی

نظریه پرداز منطقی چندین مفهوم را معرفی کرد که در تحقیقات هوش مصنوعی نقش اساسی دارند:

استدلال به عنوان جستجو

منطق‌دان یک درخت جستجو را بررسی کرد: ریشه آن فرضیه اولیه بود و هر شاخه، یک استنتاج بر اساس قوانین منطق بود. در جایی از این درخت، هدف وجود داشت: گزاره‌ای که برنامه قصد اثبات آن را داشت. مسیر طی شده در امتداد شاخه‌ها که به هدف منجر می‌شد، یک اثبات بود - مجموعه‌ای از اظهارات که هر کدام با استفاده از قوانین منطق استنتاج شده بودند و از فرضیه به گزاره‌ای که باید اثبات می‌شد، می‌رسیدند.

هیوریستیک

نیوئل و سایمون متوجه شدند که درخت جستجو به‌صورت نمایی رشد خواهد کرد و نیاز است که برخی از شاخه‌ها را "هرس" کنند، با استفاده از "قواعد سرانگشتی" تعیین کنند که کدام مسیرها احتمالاً به راه‌حل منجر نمی‌شوند. آن‌ها این قوانین موقتی را "هیوریستیک" نامیدند، اصطلاحی که توسط جورج پولیا در کتاب کلاسیک خود درباره اثبات ریاضی، "چگونه مسئله را حل کنیم"، معرفی شده بود. (نیوئل در استنفورد دوره‌هایی با پولیا گذرانده بود.) هیوریستیک‌ها به یک حوزه مهم از تحقیقات در هوش مصنوعی تبدیل شدند و هنوز هم به عنوان یک روش مهم برای کنترل انفجار ترکیبی جستجوهایی که به‌صورت نمایی رشد می‌کنند، استفاده می‌شوند.

پردازش لیست

برای پیاده سازی نظریه پرداز منطقی بر روی کامپیوتر، سه پژوهشگر یک زبان برنامه‌نویسی به نام IPL توسعه دادند که از همان شکل پردازش لیست نمادین استفاده می‌کرد که بعدها اساس زبان برنامه‌نویسی Lisp مک‌کارتی شد، زبانی مهم که هنوز هم توسط پژوهشگران هوش مصنوعی استفاده می‌شود.

پیامدهای فلسفی

پاملا مک‌کوردوک می‌نویسد که نظریه‌پرداز منطقی "اثبات قطعی بود که یک ماشین می‌تواند وظایفی را انجام دهد که پیش از این هوشمندانه، خلاق و منحصر به انسان محسوب می‌شدند." و به همین دلیل، این برنامه یک نقطه عطف در توسعه هوش مصنوعی و درک ما از هوش به طور کلی را نشان می‌دهد. سایمون در ژانویه ۱۹۵۶ به یک کلاس تحصیلات تکمیلی گفت: "در طول کریسمس، آل نیوئل و من یک ماشین فکری اختراع کردیم"، و نوشت:

"[ما] یک برنامه کامپیوتری اختراع کردیم که قادر به تفکر غیرعددی است و بدین ترتیب مسئله قدیمی ذهن-جسم را حل کردیم و توضیح دادیم که چگونه یک سیستم مادی می‌تواند ویژگی‌های ذهنی داشته باشد."

این اظهار که ماشین‌ها می‌توانند ذهن‌هایی همانند انسان‌ها داشته باشند، بعدها توسط فیلسوف جان سرل به عنوان "هوش مصنوعی قوی" نام‌گذاری شد. این موضوع همچنان تا به امروز موضوع بحث‌های جدی است.

پاملا مک‌کوردوک همچنین در منطق‌دان آغاز یک نظریه جدید درباره ذهن، مدل پردازش اطلاعات (که گاهی به آن محاسبات‌گرایی یا شناخت‌گرایی نیز گفته می‌شود) را می‌بیند. او می‌نویسد که "این دیدگاه به مرکزیت کارهای بعدی آن‌ها تبدیل شد و به نظر آن‌ها، همان‌قدر برای درک ذهن در قرن بیستم مهم بود که اصل انتخاب طبیعی داروین برای درک زیست‌شناسی در قرن نوزدهم مهم بود." نیوئل و سایمون بعداً این پیشنهاد را به عنوان فرضیه سیستم‌های نمادین فیزیکی رسمی کردند.

منابع

• Crevier, Daniel (1993). AI: The Tumultuous Search for Artificial Intelligence

• McCorduck, Pamela (2004), Machines Who Think (2nd ed.)

• (4th ed.) Russell, Stuart J.; Norvig, Peter. (2021) Artificial Intelligence: A Modern Approach