در روزهایی که هیاهوی دستیابی به هوش جامع مصنوعی (AGI) و حل خودکار پیچیدهترین مسائل علمی به اوج خود رسیده، یک پژوهش علمی جدید واقعیتِ توانایی واقعی مدلهای هوش مصنوعی را به نمایش گذاشته است. محققان با انتشار بنچمارک FrontierMath Erdős، توان استدلال هوش مصنوعی را با ۶۸ مسئله باز و حلنشده ریاضی محک زدند؛ آزمونی که نشان داد بزرگترین مدلهای جهان در مواجهه با مرزهای واقعی دانش بشری هنوز در نقطه آغاز قرار دارند.
بنچمارک FrontierMath Erdős چیست و چرا اهمیت دارد؟
پژوهشگران مؤسسه Epoch AI با همکاری دانشگاه منچستر، بنچمارک جدیدی تحت عنوان FrontierMath Erdős (FME) طراحی کردهاند. هدف این پروژه ارزیابی دقیق، مستقل و بدون تعصبِ سیستمهای هوش مصنوعی در برابر مسائل واقعی و حلنشده ریاضیات است. این مجموعه شامل ۶۸ مسئله حلنشده ریاضی برگرفته از حدسهای مشهور پل اردوش (Paul Erdős)، ریاضیدان نامدار سده بیستم، است که از میان صدها مسئله باز موجود در وبسایت جامع erdosproblems انتخاب شدهاند.
برخلاف آزمونهای رایج گذشته نظیر GSM8k یا مسائل مسابقات ریاضی (IMO) که پیشتر پاسخهای آنها در دادههای آموزشی مدلها وجود داشت، مسائل بنچمارک FME تا پیش از این توسط هیچ انسانی حل نشدهاند. بنابراین، هیچ امکانی برای حفظ کردن دادهها یا «نشت اطلاعات» (Data Contamination) وجود ندارد و مدلها ناچارند توانایی واقعی خود در تولید دانش جدید را به نمایش بگذارند.
شرایط سختگیرانه آزمون و استفاده از دستیار اثبات Lean
یکی از بزرگترین چالشهای ارزیابی هوش مصنوعی در ریاضیات، پدیده توهم (Hallucination) و ساخت برهانهای غلطِ اما بهظاهر منطقی است. برای حل این مشکل، بنچمارک FrontierMath مدلها را موظف کرده تا راهحلهای خود را در قالب نرمافزار اثباتگر صوری Lean بنویسند. Lean یک زبان برنامهنویسی و سیستم کنترل منطقی است که درستی گامبهگام هر اثبات ریاضی را با دقت مطلق بررسی میکند و اجازه هیچگونه مغالطه یا خطای پنهانی را نمیدهد.
سیستمهای هوش مصنوعی برای قبولی در این بنچمارک باید نهتنها یک حدس ریاضی را اثبات یا رد کنند، بلکه کد صوری آن را در سیستم Lean تحویل دهند تا بدون دخالت انسان اعتبارسنجی شود.
نتایج ناامیدکننده اما واقعی: برتری قاطع نبوغ انسانی
در جریان این آزمایش، ۵ مدل پیشرو هوش مصنوعی با بودجه پردازشی مشخص (معادل ۳۰۰ دلار هزینه محاسباتی برای هر مسئله) مورد ارزیابی قرار گرفتند. نتایج حاصل، شکاف عمیق میان ابزارهای زبانی و درک عمیق منطقی را آشکار کرد:
| نام مدل / سیستم ارزیابیشده | بودجه برای هر مسئله | نرخ موفقیت در حل مسائل | وضعیت اعتبارسنجی در Lean |
|---|---|---|---|
| GPT-6 Astra | ۳۰۰ دلار | ۳ درصد (۲ مسئله از ۶۸) | تأیید صوری در Lean |
| مدلهای رقیب (۴ مدل پیشرفته دیگر) | ۳۰۰ دلار | ۰ درصد | رد کامل |
همانطور که جدول بالا نشان میدهد، تنها یکی از مدلها (مدل فرضی نسل جدید GPT-6 Astra) موفق شد حدود ۳ درصد از مسائل را حل کند و سایر مدلهای تراز اول حتی به یک پاسخ درست نیز دست نیافتند. این آمار نشان میدهد که حتی صرف منابع مالی و پردازشی سنگین در جریان استنتاج، هنوز نمیتواند جایگزین شهود و خلاقیت ریاضی شود.
پیامدهای این نتایج بر بازار هوش مصنوعی و سرمایهگذاران
شکست سنگین سیستمها در بنچمارک FME نشاندهنده چند واقعیت کلیدی در صنعت فناوری است:
- اشباع استدلال زبانی: مدلهای صرفاً مبتنی بر پیشبینی توکن، علیرغم پیشرفت شگفتانگیز در استدلالهای چندمرحلهای کوتاهمدت، در اکتشافات بلندمدت و استنتاجهای انتزاعی متوقف میشوند.
- تغییر رویکرد سرمایهگذاری: غولهای فناوری برای رسیدن به پیشرفتهای حقیقی در حوزه علوم پایه و بیوتکنولوژی باید معماریهای متفاوتی مانند مدلهای ترکیبی نوروسیمبولیک (ترکیب شبکههای عصبی و منطق صوری) را در اولویت قرار دهند.
- واقعگرایی بهجای هایپ تبلیغاتی: نشان داده شد که نتایج درخشان در آزمونهای گذشته تا حد زیادی متأثر از شباهت مسائل با دادههای آموزشی پیشین بوده و ادعای دستیابی قریبالوقوع به هوش جامع علمی مبالغهآمیز است.
آینده استدلال ماشینی در ریاضیات
با وجود نرخ موفقیت بسیار پایین، ثبت همان ۳ درصد موفقیت اولیه اثبات میکند که استفاده از دستیارهای اثبات صوری مانند Lean، مسیر درست آینده است. اتصال مدلهای بزرگ به محیطهای راستیآزمایی ریاضی میتواند بهمرور زمان از خطاها بکاهد و هوش مصنوعی را از یک تولیدکننده متن به یک «دستیار واقعی پژوهشگر» تبدیل کند.
جمعبندی
بنچمارک FrontierMath Erdős تصویر شفاف و دقیقی از موقعیت کنونی هوش مصنوعی ترسیم میکند. این پژوهش اثبات کرد که حل مسائل اصیل و مرزی علم، فراتر از توانایی مدلهای امروزی در بازتولید دانش موجود است. تا زمانی که هوش مصنوعی نتواند شهود خلاقانه و استدلال صوری را بهطور پایدار تلفیق کند، رهبری اکتشافات بزرگ علمی همچنان در انحصار ذهن انسان باقی خواهد ماند.
سؤالات متداول
بنچمارک FrontierMath Erdős چیست؟
یک آزمون استاندارد شامل ۶۸ مسئله باز و حلنشده ریاضی از حدسهای پل اردوش است که برای سنجش استدلال صوری هوش مصنوعی در محیط نرمافزار Lean طراحی شده است.
چرا حل مسائل ریاضی در سیستم Lean اهمیت دارد؟
چون سیستم اثباتگر صوری Lean مانع از توهم هوش مصنوعی میشود و درستی منطقی هر استدلال را بهصورت قطعی و بدون دخالت دست تأیید میکند.
نتیجه ارزیابی پیشرفتهترین مدلهای هوش مصنوعی در این آزمون چه بود؟
از بین ۵ مدل ارزیابیشده، ۴ مدل نمره صفر درصد گرفتند و تنها یک مدل پیشرفته توانست ۳ درصد از مسائل را حل کند.
تفاوت این بنچمارک با آزمونهای المپیادی مثل IMO چیست؟
مسائل این بنچمارک تاکنون توسط هیچ انسانی حل نشدهاند و مدل نمیتواند راهحل آنها را از قبل در دادههای آموزشی خود دیده باشد.
