سفر DeepMind به سوی تسلط هوش مصنوعی در ریاضیات، سال گذشته با AlphaProof و AlphaGeometry یک جهش بزرگ برداشت و تقریباً مدال طلا را در المپیاد بین‌المللی ریاضی (IMO) به دست آورد. اکنون، با آخرین ارتقاء، AlphaGeometry2 (AG2) رسماً از برترین رقبای انسانی در هندسه پیشی گرفته و نقطه عطفی را در استدلال ریاضی مبتنی بر هوش مصنوعی رقم زده است. اجماع کلی در بین شرکت‌کنندگان IMO این است که مسائل هندسه از سخت‌ترین مسائل در هر روز المپیاد هستند.

AG2 نشان‌دهنده پیشرفت چشمگیری در استدلال ریاضی مبتنی بر هوش مصنوعی، به‌ویژه در حل مسائل هندسه المپیاد است. AG2 با تکیه بر نسخه قبلی خود، AlphaGeometry، از عملکرد یک مدال‌آور طلای متوسط در المپیاد بین‌المللی ریاضی (IMO) فراتر می‌رود. این مقاله یک بررسی فنی از معماری AG2، بهبودهای کلیدی و مشارکت‌های گسترده‌تر آن در هوش مصنوعی ارائه می‌دهد.

بنابراین ما ایده‌ای از پیچیدگی مسائل هندسه در IMO داریم، به مثال زیر از مقاله نگاه کنید:

AG2 از یک رویکرد عصبی-نمادین استفاده می‌کند که شبکه‌های عصبی و موتورهای نمادین را ترکیب می‌کند. معماری آن از سه جزء اصلی تشکیل شده است:

1. مدل زبان (LM): مدل زبان مبتنی بر معماری Gemini، عبارات مسئله را تفسیر می‌کند، ساختارهای کمکی را تولید می‌کند و مراحل اثبات را پیشنهاد می‌دهد.
2. موتور نمادین (DDAR): موتور استدلال حسابی پایگاه داده قیاسی (DDAR) مراحل اثبات را با استفاده از قوانین و اصول موضوعه از پیش تعریف شده تأیید می‌کند.
3. الگوریتم جستجو: الگوریتم مجموعه دانش مشترک درخت‌های جستجو (SKEST) چندین جستجوی پرتو را به موازات اجرا می‌کند و دانش را برای بهبود فرآیند جستجو به اشتراک می‌گذارد.

زبان دامنه گسترده

AG2 زبان دامنه اصلی AlphaGeometry را گسترش می‌دهد و پوشش آن از مسائل هندسه IMO را از 66٪ به 88٪ افزایش می‌دهد. اضافات کلیدی عبارتند از:

• محمول‌های Find x: محمول‌های acompute و rcompute زوایای یا نسبت‌های خاص را حل می‌کنند.
• معادلات خطی: محمول‌های distmeq، distseq و angeq معادلات خطی شامل مقادیر هندسی را بیان می‌کنند.
• مسائل مکان هندسی: نشانه * مکان نگهدار ثابت را نشان می‌دهد.
• بررسی‌های نمودار: محمول‌های sameclock، noverlap و lessthan استنتاج‌های معتبر را تضمین می‌کنند.
• مسائل غیر سازنده: اجازه می‌دهد نقاط تعریف شده توسط سه یا چند محمول.

موتور نمادین قوی‌تر و سریع‌تر

موتور DDAR AG2 چندین بهینه‌سازی را در خود جای داده است:

• نقاط دوتایی: نقاط با مختصات یکسان اما نام‌های مختلف را مدیریت می‌کند.
• الگوریتم سریع‌تر: الگوریتم DDAR2 از جستجوهای کدگذاری شده و تکنیک‌های هشینگ برای کارایی استفاده می‌کند.
• پیاده‌سازی سریع‌تر: محاسبات اصلی از C++ استفاده می‌کنند و به بهبود سرعت 300 برابری دست می‌یابند.

مدل زبان پیشرفته

مدل زبان، مبتنی بر معماری Gemini، بر روی یک مجموعه داده متنوع از 300 میلیون قضیه مصنوعی آموزش داده شده است. بهبودها عبارتند از:

• نمودارهای بزرگتر و پیچیده‌تر
• قضایایی با پیچیدگی بیشتر و اثبات‌های طولانی‌تر
• توزیع داده متعادل‌تر در انواع مسئله
• قضایای نوع «مکان هندسی» جدید

در طول استنتاج، AG2 از نمونه‌برداری top-k با دمای 1.0 و k = 32 استفاده می‌کند و پیشنهادات متنوعی برای ساخت کمکی ایجاد می‌کند.

SKEST چندین جستجوی پرتو را به موازات با پیکربندی‌های مختلف اجرا می‌کند و دانش را از طریق یک پایگاه داده مرکزی به اشتراک می‌گذارد. تغییرات درخت جستجو عبارتند از:

• درخت جستجوی کلاسیک (مشابه AG1)
• درخت‌هایی که چندین نقطه کمکی را پیش‌بینی می‌کنند
• درخت‌های عمیق و باریک
• درخت‌های کم‌عمق و پهن

این رویکرد فرآیند جستجو را تسریع می‌کند و عملکرد کلی را بهبود می‌بخشد.

نتایج و عملکرد

AG2 به نرخ حل 84 درصدی در مسائل هندسه IMO (2000–2024) دست می‌یابد و از یک مدال‌آور طلای متوسط پیشی می‌گیرد. همچنین 20 مسئله از 30 مسئله سخت فهرست نهایی IMO را حل می‌کند.

• افزایش اندازه مدل، تلفات سردرگمی را کاهش می‌دهد.
• دمای بالا و نمونه‌های متعدد برای موفقیت ضروری هستند.
• پیکربندی بهینه درخت جستجو: اندازه پرتو 128، عمق 4 و 32 نمونه.

تأثیر گسترده‌تر و مسیرهای آینده

موفقیت AG2 پتانسیل رویکردهای عصبی-نمادین را در وظایف استدلال پیچیده برجسته می‌کند. تحقیقات آینده ممکن است به بررسی موارد زیر بپردازد:

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

آیا چندوجهی بودن آینده است؟

آموزش چندوجهی با استفاده از Gemini 1.5 (ترکیب متن و نمودارها) نرخ حل را بهبود نبخشید، احتمالاً به دلیل پیچیدگی نمودارهای IMO و محدودیت‌ها در نشانه‌گذاری تصویر. با این حال، ترکیب مدل‌های چندوجهی با چارچوب‌های دیگر همچنان عملکرد کلی را افزایش می‌دهد.

راه حل های خلاقانه و استدلال شبیه به انسان

راه‌حل‌های AG2 اغلب خلاقیت فوق بشری از خود نشان می‌دهند و ساختارهای کمکی غیرمتعارف و راه‌حل‌های ظریف را کشف می‌کنند. مثال‌ها شامل مسئله IMO 2024 P4 است.

توکن‌سازها و زبان‌های خاص دامنه

عملکرد در توکن‌سازهای مختلف ثابت باقی می‌ماند. ترجمه داده‌های AG2 به زبان طبیعی نتایج قابل مقایسه‌ای به دست می‌دهد و نشان می‌دهد که توکن‌سازهای LLM مدرن به اندازه کافی برای وظایف ریاضی انعطاف‌پذیر هستند.

تولید اثبات کامل با LM

در حالی که AG2 برای تأیید صحت اثبات به موتور نمادین متکی است، LM آن می‌تواند راه‌حل‌های جزئی را به طور مستقل تولید کند و به این موضوع اشاره می‌کند که LMهای آینده در استدلال ریاضی خودکفاتر خواهند شد.

AlphaGeometry2 نقطه عطف مهمی در استدلال ریاضی مبتنی بر هوش مصنوعی است. معماری عصبی-نمادین، زبان دامنه پیشرفته، موتور نمادین بهینه شده و الگوریتم جستجوی جدید آن، همگی با هم عملکرد مدال‌آور طلا را در حل مسائل هندسه IMO امکان‌پذیر می‌سازند. با ادامه تحقیقات، انتظار می‌رود قابلیت‌های هوش مصنوعی در ریاضیات و سایر حوزه‌ها رشد کند و امکانات جدیدی را برای همکاری هوش مصنوعی و انسان باز کند.