رمزگشایی از مخزن ریاضی اوپن ای آی؛ گامی به سوی استدلال منطقی
مخزن ریاضی اوپن‌ای‌آی: این مستندات در ۳۷۲ دسته‌بندی یا خانواده موضوعی قرار می‌گیرند و مباحثی نظیر فرضیه ریمان و حدس‌های پیچیده ریاضی را شامل می‌شوند.
خلاصه
شرکت OpenAI مجموعه‌ای گسترده شامل ۷۲۲ دست‌نوشته ریاضی را در قالب یک مخزن عمومی منتشر کرده است که حاصل پردازش مدل‌های داخلی و منتشرنشده این سازمان هستند. این مستندات در ۳۷۲ دسته‌بندی یا خانواده موضوعی قرار می‌گیرند و مباحثی نظیر فرضیه ریمان و حدس‌های پیچیده ریاضی را شامل می‌شوند. هدف اصلی از این انتشار، نمایش توانمندی هوش مصنوعی در عبور از مرزهای دانش فعلی و حل مسائلی است که پیش‌تر برای مدل‌های زبانی اشباع شده بودند.
چرا هوش مصنوعی به سراغ ریاضیات محض رفته است؟
توسعه‌دهندگان هوش مصنوعی متوجه شده‌اند که ارزیابی‌های متداول برای سنجش هوش مدل‌ها دیگر کافی نیست. زمانی که یک مدل زبانی به سقف توانایی خود در پاسخ‌گویی به سوالات عمومی می‌رسد، ریاضیات به عنوان سخت‌ترین سنگ محک برای سنجش «استدلال منطقی» وارد میدان می‌شود. در ریاضیات، برخلاف ادبیات، پاسخ‌ها سیاه یا سفید هستند و کوچک‌ترین خطا در زنجیره استدلال، کل نتیجه را ویران می‌کند.
پروژه ریاضی OpenAI که در مخزن گیت‌هاب این شرکت در دسترس است، نشان می‌دهد که مدل‌های هوش مصنوعی چگونه می‌توانند برای ساعت‌ها روی یک مسئله واحد تمرکز کنند. به طور متوسط، هر نتیجه ثبت شده در این کاتالوگ حاصل ۳ ساعت پردازش مداوم مدل داخلی OpenAI بوده است. این یعنی ما از مرحله پاسخ‌های آنی عبور کرده‌ایم و به عصری وارد شده‌ایم که هوش مصنوعی برای حل مسائل، زمان صرف «فکر کردن» می‌کند.
ساختار مخزن ریاضی و نحوه استفاده از آن
این مجموعه تنها یک فهرست ساده از فرمول‌ها نیست. ساختار آن به گونه‌ای طراحی شده که پژوهشگران بتوانند مسیر استدلال ماشین را دنبال کنند. محتوای این مخزن به بخش‌های زیر تقسیم می‌شود:
۱. خانواده‌های موضوعی: مسائل مرتبط در گروه‌هایی دسته‌بندی شده‌اند که شامل نتیجه اصلی، استدلال‌های مکمل و اثبات‌های جایگزین است. ۲. کتابخانه Lean: بخش مهمی از این تلاش، فرموله کردن نتایج با زبان Lean است. Lean یک زبان برنامه‌نویسی و دستیار اثبات است که اجازه می‌دهد صحت منطق ریاضی توسط کامپیوتر به صورت ۱۰۰ درصدی تایید شود. ۳. پیش‌نویس‌های علمی: در پوشه preprints، فایل‌های PDF و سورس‌های مربوط به هر مقاله قرار گرفته است که شباهت زیادی به مقالات منتشر شده در ArXiv دارد.
کاربران ایرانی که از طریق پلتفرم‌هایی مانند هوش مصنوعی نهال به مدل‌های پیشرفته بین‌المللی دسترسی دارند، می‌توانند با بررسی این الگوها، نحوه صحیح پرسشگری برای حل مسائل فنی و مهندسی را بیاموزند. در واقع، این مخزن به ما نشان می‌دهد که برای رسیدن به نتایج دقیق، باید مسئله را به قطعات کوچک‌تر تقسیم کرد و از هوش مصنوعی خواست تا گام‌به‌گام پیش برود.
نتایج برجسته و دستاوردهای مدل
در میان صدها سند منتشر شده، برخی نتایج به دلیل اهمیت تاریخی و علمی خود برجسته‌تر هستند. برای نمونه، مدل توانسته است در زمینه‌های زیر خروجی‌های قابل توجهی تولید کند:
- توزیع اعداد اول: کار روی ناحیه بدون صفر تابع زتا ریمان که یکی از بزرگ‌ترین معماهای ریاضی جهان است.
- نظریه گراف و پیچیدگی محاسباتی: بررسی مسائل مربوط به NP-hardness که در بهینه‌سازی سیستم‌های نرم‌افزاری کاربرد فراوان دارد.
- فیزیک کوانتوم: تحلیل مغناطش خودبه‌خودی در مدل‌های هایزنبرگ که نشان‌دهنده توانایی مدل در درک فیزیک نظری است.
نکته حائز اهمیت این است که تمامی این نتایج توسط انسان بازبینی نشده‌اند. OpenAI به صراحت اعلام کرده است که برخی از نتایج تایید نشده ممکن است دارای خطا باشند و از جامعه علمی درخواست کرده است تا در فرآیند بررسی و اصلاح این نتایج مشارکت کنند.
چالش اثبات و تایید انسانی
یکی از بزرگ‌ترین چالش‌ها در این پروژه، تفاوت میان «تولید متن ریاضی» و «اثبات ریاضی» است. یک مدل هوش مصنوعی ممکن است متنی بنویسد که در ظاهر بسیار منطقی به نظر برسد، اما در باطن حاوی یک مغلطه ظریف باشد. به همین دلیل، استفاده از زبان‌های فرمال مانند Lean ضروری است. در حال حاضر، بسیاری از ۷۲۲ دست‌نوشته موجود هنوز به طور کامل فرموله نشده‌اند و این نشان می‌دهد که حتی پیشرفته‌ترین مدل‌ها نیز در گام نهایی تاییدیه رسمی با چالش مواجه هستند.
برای متخصصان و دانشجویان در ایران، مطالعه این مخزن فرصتی است تا ببینند چگونه می‌توان از هوش مصنوعی نهال یا سایر ابزارهای مشابه برای پیشبرد پژوهش‌های آکادمیک استفاده کرد. این رویکرد که «محاسبات فکری» نامیده می‌شود، نشان‌دهنده آینده‌ای است که در آن هوش مصنوعی نه فقط یک ابزار چت، بلکه یک همکار علمی در آزمایشگاه‌های مجازی خواهد بود.
نکات کلیدی
- مخزن ریاضی OpenAI شامل ۷۲۲ مقاله علمی در ۳۷۲ دسته مختلف است که توسط مدل‌های داخلی تولید شده‌اند.
- هر نتیجه به طور میانگین حاصل ۳ ساعت پردازش مداوم مدل در حالت استدلال عمیق بوده است.
- بخشی از این نتایج با زبان Lean فرموله شده‌اند تا صحت منطقی آن‌ها توسط ماشین تایید شود.
- این پروژه شامل تلاش‌هایی برای حل مسائل بسیار پیچیده نظیر فرضیه ریمان و حدس‌های مهلر است.
منبع: github.com