انتشار AlphaProof Nexus از دیپ‌مایند در Science؛ هوش مصنوعی ۹ مسئله ریاضی حل‌نشده اردوش را به‌طور مستقل حل کرد

جامعه هوش مصنوعی و ریاضیات در روزهای اخیر شاهد تحولات چشمگیری بوده است. در ۶ اکتبر، OpenAI به‌یک‌باره ۷۲۲ دست‌نوشته ریاضی تولیدشده با هوش مصنوعی را در گیت‌هاب منتشر کرد؛ اقدامی که بلافاصله بازتاب گسترده‌ای در محافل ریاضی داشت و انجمن ریاضی‌دانان انسانی (AHM) به ریاست ترنس تائو با انتشار بیانیه‌ای خواستار تحریم این اقدام شد.

در همان هفته، مقاله‌ای از گوگل دیپ‌مایند نیز در ۸ اکتبر، پس از طی فرایند رسمی داوری همتا، در مجله Science منتشر شد.

بر اساس گزارش‌های رسانه‌ای، موضوع اصلی این مقاله AlphaProof Nexus، سامانه‌ای خودکار برای کشف اثبات‌های ریاضی، است. این سامانه از میان ۳۵۳ مسئله حل‌نشده اردوش، ۹ مسئله را به‌طور مستقل حل کرده است که دو مورد از آنها از سال ۱۹۷۰، یعنی ۵۶ سال، بدون حل باقی مانده بودند.

لینک مقاله: https://www.science.org/doi/10.1126/science.aej2213

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

نکته مهم این است که هیچ‌یک از این ۳۵۳ مسئله، اهداف آسانی نیستند که دیپ‌مایند خودش انتخاب کرده باشد. اینها تمام مسائلی از مجموعه مسائل اردوش هستند که تا فوریه ۲۰۲۶ در مخزن متن‌باز Formal Conjectures به زبان Lean ترجمه شده بودند. سامانه همه آنها را پردازش می‌کند، برای هر مسئله حداکثر ۳۰۰۰ دور تلاش انجام می‌دهد و اگر نتواند اثباتی تولید کند، از ادامه کار صرف‌نظر می‌کند. ۹ مسئله‌ای که سرانجام حل شدند، از جمله مسئله دوازدهمِ مطرح‌شده توسط اردوش و شِرکی در سال ۱۹۷۰ را شامل می‌شوند.

این دستاوردها به همین‌جا ختم نمی‌شود. از میان ۴۹۲ حدس باز در دانشنامه دنباله‌های اعداد صحیح OEIS، تعداد ۴۴ مورد اثبات شده‌اند؛ همچنین یک مسئله حل‌نشده ۱۵ ساله در هندسه جبری، یعنی حدس مربوط به توابع هیلبرت، حل شده است. افزون بر این، سامانه طرحی جدید برای تنظیم پارامترها در بهینه‌سازی مینیمکس پیدا کرده که کران بالای شناخته‌شده را بهبود می‌دهد. این سامانه همچنین به حل یک مسئله باز از فهرست ریاضی‌دان، بن گرین، کمک کرده و اکنون برای پشتیبانی از پروژه‌های پژوهشی در حال انجام در حوزه‌های اپتیک کوانتومی و نظریه گراف نیز به کار گرفته می‌شود.

از نظر هزینه، مقاله رقم سربار استنتاجی چندصد دلار برای هر مسئله را اعلام کرده است.

چگونه اثبات‌ها را تولید می‌کند

چرخه اصلی سامانه را می‌توان در یک جمله خلاصه کرد: مدل زبانی بزرگ مسئول نوشتن است و کامپایلر مسئول داوری.

به‌طور مشخص، Gemini 3.1 Pro با استفاده از زبان صوری Lean پیش‌نویس اثبات‌ها را می‌نویسد. پس از هر بازبینی، کامپایلر Lean آن را خط‌به‌خط بررسی می‌کند و پیام‌های خطا برای هدایت پیش‌نویس بعدی به سامانه بازگردانده می‌شوند. این سامانه چندین سازوکار حفاظتی نیز دارد: تغییر متن قضیه‌ها مجاز نیست، استفاده از جای‌خالی‌های «sorry» در اثبات ممنوع است، هیچ اصل موضوع اضافی نمی‌توان وارد کرد و کل فرایند راستی‌آزمایی در یک محیط ایزوله انجام می‌شود.

پژوهشگران علاوه بر این چرخه، یک چارچوب «تکامل» نیز ایجاد کرده‌اند. گروهی از عامل‌های فرعی به‌طور مستقل به جست‌وجوی اثبات می‌پردازند و در قالب رقابت‌هایی با نظام امتیازدهی Elo، مشابه شطرنج، با یکدیگر رقابت می‌کنند. ایده‌های امیدوارکننده حفظ و مسیرهای بن‌بست کنار گذاشته می‌شوند. هنگام مواجهه با مسائل فرعی دشوار نیز این عامل‌ها می‌توانند از AlphaProof، اثبات‌کننده تخصصی‌ای که در المپیاد بین‌المللی ریاضی ۲۰۲۴ به سطح مدال نقره دست یافت، کمک بگیرند.

روند کاری AlphaProof Nexus به این شکل است: ریاضی‌دانان زمینه را به زبان طبیعی، مسائل صورت‌بندی‌شده در Lean و پایگاه دانش را در اختیار سامانه قرار می‌دهند. عامل‌های فرعی تولید اثبات، عامل‌های فرعی بازبینی و راستی‌آزمای سامانه پیرامون یک «پایگاه جمعیت» به‌صورت تکرارشونده کار می‌کنند تا در نهایت اثبات‌های صوری تولید شوند.

بااین‌حال، یک نتیجه بسیار کاربردی از آزمایش حذف اجزای سامانه در مقاله وجود دارد: اگر چارچوب پیچیده کنار گذاشته شود و فقط نسخه ساده‌شده «مدل زبانی بزرگ به‌علاوه بازخورد Lean» باقی بماند، هر ۹ مسئله اردوش همچنان قابل حل هستند؛ تنها مسائل دشوارتر هزینه بیشتری نیاز دارند. به بیان دیگر، عامل اصلی موفقیت، خودِ ترکیب مدل پایه با بازخورد کامپایلر است.

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

چند نکته احتیاطی

نخست، نرخ موفقیت. حل ۹ مسئله از ۳۵۳ مسئله، معادل حدود ۲.۵ درصد است. این نسبت تقریباً با برآورد ترنس تائو مبنی بر اینکه «نرخ موفقیت هوش مصنوعی در حل مسائل اردوش حدود ۱ تا ۲ درصد است» همخوانی دارد. هنوز اکثریت قریب‌به‌اتفاق مسائل باز خارج از دسترس سامانه هستند. خود مقاله نیز اذعان می‌کند که موفقیت‌ها عمدتاً در حوزه‌هایی متمرکز شده‌اند که کتابخانه ریاضی Lean در آنها نسبتاً بالغ است و مسائلی که به ایجاد حجم زیادی از نظریه‌های جدید نیاز دارند، هنوز برای سامانه قابل حل نیستند.

دوم، ممکن است تعداد مسائل حل‌شده بیش از واقع اعلام شده باشد. پس از عمومی شدن تمام اثبات‌های Lean در مقاله، یک بررسی مستقل نشان داد که اگرچه اثبات مسئله ۸۴۶ معتبر است، یک قضیه از ری، رودل و سیلز که در سال‌های گذشته ارائه شده بود، در واقع از پیش پاسخ این مسئله را نتیجه می‌داد. بنابراین، با تعریف سخت‌گیرانه‌تر «مسائل تازه‌حل‌شده»، این عدد باید از ۹ به ۸ کاهش یابد. افزون بر این، مسائل ۷۴۱ و ۸۴۶ نیز به‌طور مستقل توسط مدل داخلی OpenAI حل شده بودند.

سوم، سامانه متن‌باز نیست. فایل‌های اثبات برای دانلود در گیت‌هاب در دسترس هستند، اما خود AlphaProof Nexus برای عموم قابل دسترسی نیست و دیگران نمی‌توانند آن را شخصاً بازتولید کنند. دمیس هسابیس، مدیرعامل دیپ‌مایند، نیز پیش‌تر اعلام کرده بود که این سامانه هنوز AGI نیست.

زمان‌بندی و شیوه انتشار این دستاوردها نیز قابل تأمل است.

در ۶ اکتبر، OpenAI تعداد ۷۲۲ دست‌نوشته را که ۳۷۲ مجموعه نتیجه را پوشش می‌دادند، در گیت‌هاب بارگذاری کرد و مدعی شد که در این کار به پیشنهادهای گروه مشورتی مستقل مؤسسه مطالعات پیشرفته پرینستون توجه کرده است. در نتیجه، سه مورد از این دست‌نوشته‌ها ظرف یک روز به دلیل خطاهای نمادین پس گرفته شدند.

سپس AHM به ریاست ترنس تائو بیانیه‌ای منتشر کرد و این اقدام را نوعی نمایش قدرت دانست و از ریاضی‌دانان خواست آن را تحریم کنند. در ۹ اکتبر نیز ترنس تائو مقاله‌ای از ریاضی‌دان، توماس هیلز، با عنوان Lean Theorem Provers That Mathematicians Should Know About: Reliability and Artificial Intelligence Issues را در وبلاگ شخصی خود بازنشر کرد.

اما دیپ‌مایند ابتدا پیش‌نسخه مقاله را در ۲۱ مه منتشر کرد، سپس راه‌حل‌ها را پیشاپیش در انجمن ErdosProblems در اختیار متخصصان قرار داد تا آنها بتوانند راه‌حل‌ها را بررسی و خطاهای احتمالی را شناسایی کنند و در نهایت مقاله را برای فرایند داوری همتا به Science ارسال کرد. اثبات‌های Lean مربوط به این ۹ مسئله نیز از مدت‌ها قبل در صفحه ویکی «AI Contributions to Erdős Problems» که ترنس تائو نگهداری می‌کند، ثبت شده‌اند.

این مقاله متعلق به حساب رسمی وی‌چت «Big Data Digest» است و با اجازه صاحب اثر توسط 36Kr منتشر شده است.