مدل آسترا (Astra) شرکت OpenAI ده مسئله حل‌نشده ریاضی را با اثبات‌های تأییدشده حل کرد؛ یک پیشرفت علمی بی‌سابقه

در اکتبر ۲۰۲۵، OpenAI پس از ادعای نادرست یک مدیر اجرایی سابق مبنی بر حل شدن ده مسئله ریاضی حل‌نشده توسط مدل GPT-۵ این شرکت، که به سرعت توسط ریاضیدانان رد شد، تحت نظارت شدید قرار گرفت. ده ماه بعد، این آزمایشگاه هوش مصنوعی با دست پر به همان عرصه بازگشته است. در ۱ اوت، OpenAI اعلام کرد که یک نسخه داخلی از مدل آتی خود به نام «آسترا» (Astra) با موفقیت راه‌حل‌هایی برای ده مسئله باز و دیرینه در ریاضیات و علوم کامپیوتر نظری تولید کرده است. این بار، شرکت از جامعه علمی نخواست که صرفاً حرف آن‌ها را بپذیرد.[2][3]

برای جلوگیری از یک شرمساری دیگر، OpenAI یک دست‌نوشته ۲۴۹ صفحه‌ای را به همراه گواهی‌های اثبات قابل بررسی توسط ماشین در گیت‌هاب (GitHub) تحت مجوز Apache ۲.۰ منتشر کرد. این اثبات‌ها در Lean ۴، یک زبان برنامه‌نویسی و دستیار اثبات، رسمی‌سازی شده بودند که هر گام منطقی یک استدلال ریاضی را مجبور می‌کند تا با جزئیات قابل خواندن توسط ماشین بیان شود. از آنجا که هسته Lean یک اثبات را یا به طور کامل می‌پذیرد یا رد می‌کند، تأیید مستقل چیزی جز اجرای گواهی‌ها از طریق کامپایلر نیاز ندارد. تعداد «sorry» در مخزن – یک مکان‌نگهدار که هنگام نادیده گرفتن یک گام اثبات استفاده می‌شود – صفر است، که نشان می‌دهد هر گام در تمام ده اثبات رسمی‌شده به طور کامل تأیید شده است.[1][2]

مسائلی که آسترا حل کرد، تمرین‌های کتاب درسی نیستند؛ آن‌ها راه‌حل‌های واقعی برای سؤالاتی هستند که ریاضیدانان را برای دهه‌ها به چالش کشیده‌اند. مهم‌ترین یافته‌ها، ساختار صریح یک گروه غیرسوفیک است که به سؤالی که از زمان ارائه مفهوم سوفیسیته توسط میخائیل گروموف (Mikhail Gromov) در سال ۱۹۹۹ بی‌پاسخ مانده بود، پاسخ داد. این مدل همچنین حدس سختی کانز (Connes's rigidity conjecture) در مورد جبرهای فون نویمان را رد کرد، حدس حجم ارهارت (Ehrhart's volume conjecture) را اثبات کرد و سه مسئله از کاتالوگ پاول اردوش (Paul Erdős) از جمله مسئله ۱۸۳ در مورد اعداد رمزی چندرنگ را حل نمود.[1][3]

قابلیت‌های آسترا به هندسه با ابعاد بالا و پیچیدگی کوانتومی نیز گسترش می‌یابد. این مدل سقف سخت‌تری را برای چگالی بسته‌بندی کره با ابعاد بالا اثبات کرد که اولین بهبود در این مرز خاص از سال ۱۹۷۸ محسوب می‌شود. همچنین یک قضیه تکرار موازی نمایی برای بازی‌های کوانتومی را اثبات کرد و به سختی مسئله نزدیک‌ترین بردار در رمزنگاری شبکه‌ای پرداخت. توماس بلوم، ریاضیدانی که پایگاه داده مسائل اردوش را مدیریت می‌کند و ادعای قبلی OpenAI را رد کرده بود، ده نتیجه جدید را «خبر بزرگ» توصیف کرد و اهمیت آن‌ها را بالاتر از یک مثال نقض فاصله واحد دانست که توسط یک مدل داخلی OpenAI در ماه مه تولید شده بود.[1][3]

گردش کار پشت این موفقیت، پارادایم جدیدی از همکاری انسان و هوش مصنوعی را برجسته می‌کند. آسترا، با استفاده از معماری زیرعاملی که برای استدلال با افق طولانی طراحی شده است، روی مسائل کار کرد تا بینش‌ها و استراتژی‌های اصلی را تولید کند. سپس محققان انسانی خروجی مدل را به دست‌نوشته‌های سنتی و قابل خواندن مناسب برای انتشار ترجمه کردند. در نهایت، آسترا هر اثبات را دوباره به نحو دقیق Lean رسمی‌سازی کرد. OpenAI همچنین راهنماهای استدلالی را منتشر کرد که در آن‌ها مدل نحوه برخورد با هر مسئله را روایت می‌کند و شفافیتی را در فرآیند حل مسئله خود ارائه می‌دهد.[1][2]

فراتر از نقاط عطف ریاضی، این دستاورد نشان‌دهنده یک تغییر چشمگیر در اقتصاد تحقیقات علمی است. OpenAI فاش کرد که کل هزینه محاسباتی برای تولید ده راه‌حل موفق تقریباً ۲۰۰۰ دلار بوده است که با نرخ‌های API مدل فعلی GPT-۵.۶ Sol آن محاسبه شده است. اگرچه این رقم هزینه‌های هنگفت ساخت و آموزش مدل یا محاسبات صرف شده برای تلاش‌های ناموفق را در بر نمی‌گیرد، اما نشان‌دهنده کارایی قابل توجهی است. یک اجرای محاسباتی با این محدوده قیمت که نتایجی را تولید می‌کند که معمولاً نیازمند سال‌ها تلاش از سوی تیمی از محققان انسانی است، نشان می‌دهد که هزینه کشف نظری در حال سقوط است.[1][2]

پیامدهای گسترده‌تر برای صنعت هوش مصنوعی قابل توجه است. موفقیت آسترا نشان می‌دهد که مدل‌های هوش مصنوعی اکنون می‌توانند تمرکز خود را در طول جلسات طولانی حل مسئله حفظ کنند و چالش‌های پیچیده را به اجزای قابل مدیریت تقسیم نمایند. سباستین بوبک، رئیس تحقیقات ریاضی OpenAI، نتایج را تأیید کرد و آن‌ها را «زیبا» خواند، در حالی که نوام براون، دانشمند محقق، این دستاورد را گامی بزرگ برای استدلال علمی توصیف کرد. در حالی که OpenAI آسترا را برای انتشار عمومی نهایی آماده می‌کند – که منوط به بررسی‌های ایمنی هوش مصنوعی فدرال است – قابلیت‌های استدلال قابل تأیید این مدل به آینده‌ای اشاره دارد که در آن سیستم‌های هوش مصنوعی به طور معمول پیشرفت‌ها را در حوزه‌های علمی حیاتی تسریع می‌کنند.[1][2]

اگرچه نتایج هنوز تحت بررسی سنتی همتا قرار نگرفته‌اند، اما ماهیت قابل بررسی توسط ماشین اثبات‌های Lean یک لایه اعتبار فوری فراهم می‌کند. موفقیت آسترا یک روند رو به رشد را تقویت می‌کند که در آن توسعه‌دهندگان هوش مصنوعی تأیید رسمی را برای ایجاد اعتماد به خروجی مدل‌های خود در اولویت قرار می‌دهند. OpenAI با اثبات ظرفیت خود برای مقابله با اسرار ریاضی چند دهه‌ای با شواهد دقیق و قابل تکرار، نه تنها اشتباهات گذشته خود را جبران کرده، بلکه استاندارد جدیدی را برای کشف علمی مستقل تعیین کرده است.[2][4]