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

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

مقاله حاضر با عنوان “LINC: رویکردی نوروسمبولیک برای استدلال منطقی با ترکیب مدل‌های زبانی و اثبات‌گرهای منطق مرتبه اول” به بررسی روش جدیدی برای حل این مشکل می‌پردازد. این رویکرد، که LINC (Logical Inference via Neurosymbolic Computation) نامیده می‌شود، وظایف استدلال منطقی را به صورت برنامه‌نویسی نوروسمبولیک مدولار بازتعریف می‌کند.

این مقاله توسط تیمی از محققان برجسته در زمینه هوش مصنوعی و پردازش زبان طبیعی نوشته شده است:

• تئو ایکس. اولاوسون
• الکس گو
• بنجامین لیپکین
• سدگائو ای. ژانگ
• آرماندو سولار-لِزاما
• جاشوا بی. تننبام
• راجر لوی

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

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

نویسندگان نشان داده‌اند که با استفاده از این رویکرد، می‌توان به دستاوردهای قابل توجهی در عملکرد در مجموعه‌های داده FOLIO و زیرمجموعه متوازن ProofWriter دست یافت. جالب توجه است که استفاده از LINC با مدل نسبتاً کوچک StarCoder+ (با ۱۵.۵ میلیارد پارامتر) حتی از GPT-3.5 و GPT-4 با روش prompting زنجیره‌ای اندیشه (Chain-of-Thought – CoT) عملکرد بهتری داشته است. به طور خاص، StarCoder+ با LINC در مجموعه داده ProofWriter به طور مطلق ۳۸٪ بهتر از GPT-3.5 و ۱۰٪ بهتر از GPT-4 عمل کرده است. همچنین، LINC در ترکیب با GPT-4 در مجموعه داده ProofWriter، ۲۶٪ بهتر از روش CoT عمل کرده است، در حالی که در مجموعه داده FOLIO عملکرد قابل مقایسه‌ای داشته است.

تجزیه و تحلیل بیشتر نشان می‌دهد که اگرچه هر دو روش (LINC و CoT) به طور متوسط تقریباً به یک اندازه در این مجموعه داده موفق می‌شوند، اما حالت‌های شکست متمایز و مکمل دارند. این یافته‌ها، شواهد امیدوارکننده‌ای را ارائه می‌دهند که نشان می‌دهد چگونه استدلال منطقی بر روی زبان طبیعی می‌تواند از طریق بهره‌گیری مشترک از LLMها در کنار اثبات‌گرهای نمادین مورد بررسی قرار گیرد.

روش‌شناسی تحقیق در این مقاله شامل چندین مرحله کلیدی است:

1. تعریف چارچوب LINC: نویسندگان چارچوب LINC را به عنوان یک رویکرد نوروسمبولیک برای استدلال منطقی تعریف می‌کنند که از LLMها برای ترجمه زبان طبیعی به عبارات منطقی و از اثبات‌گرهای قضیه برای انجام استنتاج قیاسی استفاده می‌کند.
2. انتخاب مدل‌های زبانی و اثبات‌گرهای قضیه: محققان چندین مدل زبانی بزرگ مختلف از جمله GPT-3.5، GPT-4 و StarCoder+ را انتخاب کرده‌اند. آن‌ها همچنین از یک اثبات‌گر قضیه خارجی برای انجام استنتاج منطقی استفاده کرده‌اند. (نام اثبات گر قضیه مشخص نشده)
3. مجموعه‌های داده: برای ارزیابی عملکرد LINC، از دو مجموعه داده FOLIO و ProofWriter استفاده شده است. FOLIO شامل مسائل استدلال منطقی با پیچیدگی نسبتاً کم است، در حالی که ProofWriter شامل مسائل پیچیده‌تر با استدلال چند مرحله‌ای است.
4. مقایسه با روش‌های پایه: عملکرد LINC با روش‌های پایه مختلف از جمله prompting زنجیره‌ای اندیشه (CoT) مقایسه شده است. CoT یک تکنیک prompting است که به LLMها کمک می‌کند تا با ارائه یک سری مراحل استدلال میانی، وظایف استدلال را به طور موثرتری انجام دهند.
5. تجزیه و تحلیل نتایج: نویسندگان نتایج تجربی را به دقت تجزیه و تحلیل کرده‌اند تا نقاط قوت و ضعف LINC و روش‌های پایه را شناسایی کنند. آن‌ها همچنین حالت‌های شکست متمایز هر روش را بررسی کرده‌اند.

برای مثال، در یکی از آزمایش‌ها، محققان مسئله‌ای را از مجموعه داده ProofWriter انتخاب کردند که شامل مجموعه‌ای از فرضیات و یک نتیجه است. LLM در LINC وظیفه دارد این فرضیات و نتیجه را به عبارات منطق مرتبه اول ترجمه کند. سپس این عبارات به اثبات‌گر قضیه منتقل می‌شوند که سعی می‌کند با استفاده از قوانین استنتاج منطقی، نتیجه را از فرضیات استنتاج کند. اگر اثبات‌گر قضیه موفق به استنتاج نتیجه شود، LINC به درستی نتیجه رسیده است.

یافته‌های کلیدی این مقاله به شرح زیر است:

• LINC به طور قابل توجهی عملکرد LLMها را در وظایف استدلال منطقی بهبود می‌بخشد.
• LINC در مجموعه داده‌های FOLIO و ProofWriter عملکرد بهتری نسبت به روش‌های پایه دارد.
• LINC با مدل کوچک StarCoder+ حتی از GPT-3.5 و GPT-4 با روش CoT بهتر عمل می‌کند.
• LINC و CoT حالت‌های شکست متمایز و مکمل دارند.

به عنوان مثال، نویسندگان دریافتند که LINC در مسائلی که نیاز به استدلال چند مرحله‌ای دارند، عملکرد بهتری دارد. این نشان می‌دهد که ترکیب LLMها با اثبات‌گرهای قضیه می‌تواند به حل مسائل پیچیده‌تری که LLMها به تنهایی قادر به حل آن‌ها نیستند، کمک کند.

این تحقیق دارای کاربردها و دستاوردهای بالقوه مهمی است:

• بهبود استدلال منطقی در هوش مصنوعی: LINC یک رویکرد امیدوارکننده برای بهبود استدلال منطقی در سیستم‌های هوش مصنوعی ارائه می‌دهد.
• کاربردهای متنوع: این رویکرد می‌تواند در زمینه‌های مختلف از جمله علوم، ریاضیات، مهندسی و حقوق مورد استفاده قرار گیرد.
• کشف نقاط قوت و ضعف LLMها: این تحقیق به درک بهتر نقاط قوت و ضعف LLMها در وظایف استدلال منطقی کمک می‌کند.
• ایجاد سیستم‌های هوشمندتر: با ترکیب LLMها با اثبات‌گرهای قضیه، می‌توان سیستم‌های هوشمندتری ایجاد کرد که قادر به حل مسائل پیچیده‌تر و تصمیم‌گیری‌های بهتری باشند.

به عنوان مثال، LINC می‌تواند در سیستم‌های تشخیص پزشکی برای کمک به پزشکان در تشخیص بیماری‌ها بر اساس اطلاعات پزشکی موجود مورد استفاده قرار گیرد. همچنین، می‌تواند در سیستم‌های حقوقی برای کمک به وکلا در استدلال و ارائه شواهد در دادگاه مورد استفاده قرار گیرد.

مقاله LINC یک گام مهم در جهت ایجاد سیستم‌های هوش مصنوعی است که قادر به انجام استدلال منطقی به شیوه‌ای کارآمد و قابل اعتماد هستند. با ترکیب قدرت مدل‌های زبانی بزرگ و دقت اثبات‌گرهای منطق مرتبه اول، LINC می‌تواند به حل مسائل پیچیده‌تری که LLMها به تنهایی قادر به حل آن‌ها نیستند، کمک کند. این تحقیق، شواهد امیدوارکننده‌ای را ارائه می‌دهد که نشان می‌دهد چگونه می‌توان از طریق بهره‌گیری مشترک از LLMها در کنار اثبات‌گرهای نمادین، به استدلال منطقی بر روی زبان طبیعی دست یافت. کد مربوط به این تحقیق به صورت عمومی در دسترس است (https://github.com/benlipkin/linc) و به پژوهشگران دیگر این امکان را می‌دهد تا این روش را بررسی و توسعه دهند.