هوش مصنوعی یک مسئله ریاضی حل‌نشده ۵۶ ساله را حل کرد؛ پژوهش انقلابی دیپ‌مایند در Science منتشر شد

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

اندکی پس از آنکه OpenAI مجموعه‌ای شامل ۷۲۲ اثبات ریاضی را به‌صورت یک‌جا منتشر کرد و با واکنش گسترده جامعه ریاضی‌دانان درباره روش انتشار آن‌ها روبه‌رو شد، پژوهش ریاضی گوگل دیپ‌مایند در مجله Science منتشر شد.

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

دو ریاضی‌دان از دانشگاه کارنگی ملون و دانشگاه کارولینای جنوبی در همان شماره Science یادداشتی با عنوان «هوش مصنوعی برای پژوهش ریاضی از راه رسیده است» منتشر کردند.

در شرایطی که OpenAI همچنان درگیر بحث‌های داغ درباره شیوه انتشار اثبات‌های ریاضی است، دیپ‌مایند توانسته است تحسین عمومی ریاضی‌دانان را به دست آورد.

قهرمان دیپ‌مایند در این پروژه AlphaProof Nexus است؛ چارچوبی از عامل‌های هوش مصنوعی برای اثبات‌های ریاضی که با Gemini هدایت می‌شود.

این سامانه ۹ مسئله باز اردوش را حل کرده که دو مورد از آن‌ها به مدت کامل ۵۶ سال حل‌نشده باقی مانده بودند.

علاوه بر این ۹ مسئله، AlphaProof Nexus توانسته ۴۴ حدس را در دانشنامه دنباله‌های صحیح OEIS اثبات کند، یک مسئله حل‌نشده ۱۵ ساله در هندسه جبری را حل کند و مرز نظری تثبیت‌شده‌ای را در بهینه‌سازی محدب بهبود دهد.

شکستن سد مسئله جایزه‌ای ۵۶ ساله

دیپ‌مایند ۳۵۳ مسئله را از میان نسخه‌های رسمی‌شده در Lean انتخاب کرد، آن‌ها را برای حل در اختیار AlphaProof Nexus قرار داد و در نهایت ۹ مورد را با موفقیت حل کرد.

در میان آن‌ها، Erdős #12 که در سال ۱۹۷۰ مطرح شده بود، تا امروز ۵۶ سال بدون پاسخ مانده بود.

این مسئله می‌پرسد: آیا می‌توان مجموعه‌ای بی‌نهایت از اعداد صحیح ساخت که اعضای آن محدودیت‌های سخت‌گیرانه بخش‌پذیری را رعایت کنند و در عین حال به اندازه کافی متراکم باشند؟

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

از سال ۱۹۷۰ تاکنون هیچ‌کس نتوانسته بود ساخت کامل چنین مجموعه‌ای را ارائه کند. پیشرفت‌های جزئی مختلفی وجود داشت، اما این نتایج هرگز به یک راه‌حل کامل تبدیل نشده بودند.

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

مسئله دیگر، Erdős #125 است که در سال ۱۹۹۶ مطرح شد و نزدیک به ۳۰ سال بدون نتیجه باقی ماند.

فرض کنید دو مجموعه عددی داریم: مجموعه نخست شامل اعداد صحیحی است که در مبنای ۳ فقط رقم‌های صفر و یک دارند؛ مجموعه دوم نیز شامل اعدادی است که در مبنای ۴ فقط از رقم‌های صفر و یک تشکیل شده‌اند.

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

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

AlphaProof Nexus پاسخ داد: چگالی پایین‌تر برابر صفر است.

کلید این اثبات در این واقعیت است که نسبت log₄ به log₃ عددی گنگ است. این موضوع باعث می‌شود توان‌های ۳ و ۴ در مقیاس‌های مناسب بتوانند به‌طور دلخواه به یکدیگر نزدیک شوند.

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

Erdős #846 که در سال ۱۹۹۲ مطرح شد نیز ۳۴ سال ریاضی‌دانان را متوقف کرده بود.

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

اما اگر تلاش کنیم کل مجموعه بی‌نهایت را به تعداد متناهی مجموعه تقسیم کنیم که در هیچ‌کدام سه نقطه هم‌خط وجود نداشته باشد، این کار ممکن نباشد.

به زبان ساده، این مجموعه در مقیاس محلی منظم به نظر می‌رسد، اما هرگز نمی‌توان آن را به‌طور کامل به بخش‌هایی با این ویژگی تقسیم کرد.

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

به این ترتیب یک مسئله هندسه صفحه‌ای با تبدیل به مسئله‌ای در نظریه گراف و ترکیبیات حل شد.

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

پس از حل مسائل اردوش، این سامانه ۴۴ حدس باز دیگر را در دانشنامه دنباله‌های صحیح OEIS اثبات کرد.

این سامانه حوزه هندسه جبری و بهینه‌سازی محدب را نیز کنار نگذاشت. AlphaProof Nexus یک مورد حل‌نشده ۱۵ ساله درباره لگاریتمی‌محدب بودن توابع هیلبرت در هندسه جبری را حل کرد و مرز نظری یک روش گرادیان نزولی تثبیت‌شده در بهینه‌سازی محدب را بهبود داد.

Gemini اثبات می‌نویسد، Lean آن‌ها را ارزیابی می‌کند

مکانیزم اصلی کار AlphaProof Nexus چنین است:

Gemini 3.1 Pro اثبات را می‌نویسد ← Lean آن را بررسی می‌کند ← گزارش خطاها به Gemini بازگردانده می‌شود ← اثبات اصلاح می‌شود ← دوباره بررسی می‌شود تا زمانی که کل اثبات تأیید شود.

دیپ‌مایند بر پایه این روند چهار پیکربندی عامل طراحی کرد.

عامل A ساده‌ترین نسخه است و شامل چند عامل مستقل است که هم‌زمان تلاش می‌کنند مسائل را اثبات کنند. هر عامل فرعی با Gemini کد Lean تولید می‌کند و بر اساس بازخورد کامپایلر آن را اصلاح می‌کند.

عامل B قابلیت AlphaProof را اضافه می‌کند؛ یک سامانه اختصاصی اثبات ریاضی که پیش‌تر توسط دیپ‌مایند توسعه یافته بود و در مسائل دشوار می‌تواند برای جست‌وجوی هدفمند فراخوانی شود.

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

عامل D نسخه کامل است که AlphaProof و جست‌وجوی تکاملی را با هم ترکیب می‌کند و پیکربندی اصلی مورد استفاده در این بررسی گسترده مسائل باز بوده است.

از نظر نظری، هرچه یک پیکربندی امکانات بیشتری داشته باشد، باید قدرتمندتر باشد. اما آزمایش‌های کنترل‌شده دیپ‌مایند نشان دادند ساده‌ترین نسخه، یعنی عامل A، نیز توانسته هر ۹ مسئله اردوش را حل کند.

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

در مسائل دشواری مانند #125 و #138، نسخه کامل عامل حدود ۲ تا ۵ برابر از نظر بهره‌وری هزینه بهتر از نسخه پایه عمل می‌کند.

در مجموع، هزینه حل هر مسئله توسط AlphaProof Nexus در این پروژه حدود چند صد دلار بوده است.

کد کامل اثبات‌های Lean این پروژه عمومی شده و افراد می‌توانند آن را مشاهده کنند.

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

امروز، علاوه بر هوش ریاضی‌دانان، توان محاسباتی نیز به عاملی مهم برای گشودن این مسائل جایزه‌ای تبدیل شده است.

این مقاله از حساب رسمی وی‌چت QbitAI است؛ نویسنده: Focus on cutting-edge technology. انتشار با مجوز 36Kr.