AlphaProof Nexus گوگل دیپ‌مایند: حل مسائل ریاضی دهه‌ها-پاسخ‌نداده
هوش مصنوعی
گوگلخلاصهٔ کامل‌تر
گوگل دیپ‌مایند یه فریم‌ورک جدید به اسم AlphaProof Nexus منتشر کرده که توانسته ۹ تا از ۳۵۳ مسئله‌ی باز مجموعه‌ی اِردوش رو به‌صورت خودکار حل کنه — از جمله دو سؤالی که از سال ۱۹۶۹ بی‌جواب مونده بودند. علاوه بر اون، ۴۴ تا از ۴۹۲ حدس باز از دانشنامه‌ی آنلاین دنباله‌های اعداد صحیح (OEIS) هم حل شدن. هزینه‌ی محاسباتی برای هر مسئله فقط چند صد دلار بوده، که در مقایسه با مقیاس مسائل، رقم قابل‌توجهیه.
ایده‌ی اصلی سیستم اینه که مدل زبانی — اینجا Gemini 3.1 Pro — نباید تمام زنجیره‌ی منطقی رو به‌تنهایی توی زبان طبیعی حمل کنه. به‌جاش، گام‌های اثبات رو توی Lean تولید می‌کنه؛ Lean یه زبان برنامه‌نویسی رسمیه که برای تأییدیه‌ی ریاضی طراحی شده. کامپایلر Lean هر قدم رو بررسی می‌کنه و اگه اشتباهی باشه، پیام خطا مستقیم به مدل برمی‌گرده تا دوباره تلاش کنه. این حلقه‌ی بازخورد نمادین، ضعف مدل‌های زبانی در استدلال منطقی رو تا حد خوبی جبران می‌کنه.
سیستم از چهار نوع عامل (Agent) با پیچیدگی فزاینده تشکیل شده. ساده‌ترین نوع (A) فقط از مدل زبانی و بازخورد کامپایلر استفاده می‌کنه. نوع (B) از AlphaProof — سیستم یادگیری تقویتی قبلی گوگل برای ریاضی المپیک — هم کمک می‌گیره. نوع (C) یه مؤلفه‌ی تکاملی اضافه می‌کنه که عامل‌های فرعی روی مجموعه‌ای از «طرح‌های اثبات» با هم کار می‌کنن و این طرح‌ها با یه سیستم Elo رتبه‌بندی می‌شن. نوع (D) همه‌ی این قابلیت‌ها رو داره و برای حل مسائل اِردوش استفاده شد.
یه نتیجه‌ی جالب از تحلیل پسین به دست اومد: عامل ساده‌ی نوع A هم تونسته تمام ۹ مسئله‌ی حل‌شده رو اثبات کنه، هرچند روی سخت‌ترین‌ها هزینه‌اش بیشتر بود. محققان این رو نشانه‌ای از یه روند بزرگ‌تر می‌دونن: «حلقه‌های ساده‌ی عاملی» دارن جای سیستم‌های تخصصی پیچیده رو می‌گیرن، چون مدل‌های زبانی پایه خودشون دارن قوی‌تر می‌شن.
موفقیت‌های سیستم بیشتر توی حوزه‌هایی مثل ترکیبیات، بهینه‌سازی محدب و نظریه‌ی اعداد بوده؛ جایی که کتابخانه‌ی ریاضی Lean یعنی Mathlib بالغه و مسائل به زیرهدف‌های قابل‌مدیریت تقسیم می‌شن. بیشتر مسائل اِردوش هنوز دست‌نیافتنی موندن. اما محققان نکته‌ی جالبی اضافه می‌کنن: حتی اثبات‌های ناموفق هم برای ریاضی‌دان‌ها ارزش داشتن، چون فهم‌شون از مسئله رو عمیق‌تر کردن و زیرهدف‌های حل‌نشده رو برجسته کردن.
توی این فضا، OpenAI هم دستاوردهایی داشته: مدل استدلالی اون شرکت حدس فاصله‌ی واحد اِردوش رو رد کرد، و GPT-5.2 و GPT-5.4 هم هر کدام یه مسئله‌ی اِردوش حل کردن — بدون تکیه به Lean. ترنس تائو اما هشدار می‌ده که نباید زیادی ذوق کرد: نرخ موفقیت واقعی هوش مصنوعی روی مسائل اِردوش هنوز حول یک تا دو درصده.
نکات کلیدی:
- AlphaProof Nexus از Gemini 3.1 Pro برای تولید گام‌های اثبات در Lean استفاده می‌کنه و بازخورد کامپایلر حلقه‌ی یادگیری رو می‌بنده
- ۹ مسئله از ۳۵۳ مسئله‌ی باز اِردوش حل شد، از جمله دو مورد که ۵۶ سال بی‌جواب بودند
- هزینه‌ی استنتاج برای هر مسئله فقط چند صد دلار بود
- حتی ساده‌ترین نوع عامل هم تونست همه‌ی مسائل حل‌شده رو اثبات کنه
- حتی اثبات‌های ناموفق هم برای محققان ارزش داشتن — سیستم به‌عنوان ابزار تحقیق روزمره طراحی شده
- کد و اثبات‌ها روی GitHub در دسترس عموم هستند
