هوش مصنوعی در المپیاد ریاضی بین‌المللی به مدال نقره دست پیدا کرد!
هوش مصنوعی، مدال نقره المپیاد جهانی ریاضی را از آن خود کرد
سیستم‌های هوش مصنوعی AlphaProof و AlphaGeometry 2 توانستند چهار سوال از شش سوال المپیاد جهانی ریاضی را حل کنند.
یک دستاورد بزرگ در زمینه هوش مصنوعی به ثبت رسید. سیستم‌های هوش مصنوعی AlphaProof و AlphaGeometry 2 موفق شدند چهار سوال از شش سوال پیچیده المپیاد جهانی ریاضی (IMO) را حل کنند. این دستاورد به معنای کسب مدال نقره در این رقابت معتبر جهانی است.
المپیاد جهانی ریاضی، چالشی بزرگ برای هوش مصنوعی
المپیاد جهانی ریاضی قدیمی‌ترین، بزرگ‌ترین و معتبرترین رقابت ریاضیات برای دانش‌آموزان است که از سال ۱۹۵۹ برگزار می‌شود. هر ساله، نخبگان ریاضیات سرتاسر جهان ساعت‌ها تمرین می‌کنند تا بتوانند شش سوال فوق‌العاده دشوار در زمینه جبر، ترکیبات، هندسه و نظریه اعداد را حل کنند. بسیاری از برندگان مدال فیلدز، یکی از بالاترین افتخارات در ریاضیات، سابقه حضور در المپیاد جهانی ریاضی را دارند.
در سال‌های اخیر، المپیاد جهانی ریاضی به یک چالش بزرگ در حوزه یادگیری ماشین تبدیل شده و به عنوان یک معیار مهم برای سنجش توانایی استدلال ریاضی پیشرفته سیستم‌های هوش مصنوعی شناخته می‌شود.
سیستم‌های هوش مصنوعی، هم‌تراز با نخبگان ریاضی
امسال، سیستم ترکیبی هوش مصنوعی تیم‌های AlphaProof و AlphaGeometry بر روی سوالات ارائه شده توسط برگزارکنندگان المپیاد جهانی ریاضی اعمال شد. پاسخ‌های این سیستم توسط پروفسور سر تیموتی گاورز، دارنده مدال فیلدز و مدال طلای المپیاد جهانی ریاضی، و دکتر جوزف مایرز، دو بار دارنده مدال طلای المپیاد جهانی و رئیس کمیته انتخاب سوالات المپیاد جهانی ریاضی ۲۰۲۴، بر اساس قوانین امتیازدهی المپیاد جهانی امتیازدهی شد.
پروفسور سر تیموتی گاورز در این باره می‌گوید: «این واقعیت که این برنامه می‌تواند یک ساختار غیر بدیهی مانند این را ارائه دهد بسیار چشمگیر است و فراتر از آنچه من فکر می‌کردم سطح پیشرفت است.»
ابتدا، سوالات به زبان رسمی ریاضی ترجمه شدند تا سیستم‌ها بتوانند آنها را درک کنند. در رقابت رسمی، دانش‌آموزان دو جلسه ۴.۵ ساعته برای پاسخگویی دارند. این سیستم‌ها یک سوال را در عرض چند دقیقه حل کردند و برای حل بقیه سوالات تا سه روز زمان صرف کردند.
AlphaProof دو سوال جبر و یک سوال نظریه اعداد را با تعیین پاسخ و اثبات صحت آن حل کرد که سخت‌ترین سوال مسابقه بود و تنها پنج شرکت‌کننده در المپیاد امسال توانستند آن را حل کنند. AlphaGeometry 2 نیز سوال هندسه را اثبات کرد، اما دو سوال ترکیبیات بدون پاسخ ماند.
هر یک از شش سوال می‌تواند هفت امتیاز کسب کند و حداکثر نمره ممکن ۴۲ است. سیستم ارائه شده به امتیاز نهایی ۲۸ دست یافت و در هر سوال حل شده امتیاز کامل کسب کرد که معادل بالاترین سطح دسته مدال نقره است. امسال، آستانه مدال طلا از ۲۹ امتیاز شروع می‌شود و توسط ۵۸ نفر از ۶۰۹ شرکت‌کننده در رقابت رسمی به دست آمد.
AlphaProof: رویکردی رسمی برای استدلال
AlphaProof سیستمی است که خود را برای اثبات مسائل ریاضی در زبان رسمی Lean آموزش می‌دهد. برای حل مسائل این سیستم یک مدل زبان از پیش آموزش دیده شده را با الگوریتم یادگیری تقویتی AlphaZero ترکیب نموده است.
مزیت زبان‌های رسمی این است که امکان ارائه اثبات همراه با استدلال های منطقی را دارند اما به دلیل کمبود داده ورودی محدودیت هایی دارند.
در مقابل، رویکردهای مبتنی بر زبان طبیعی علیرغم دسترسی به داده‌های بسیار بیشتر می‌توانند مراحل استدلال و راه‌حل‌های احتمالی اما نادرست را ایجاد کنند. تیم توسعه دهندگان با تنظیم دقیق یک مدل Gemini برای ترجمه خودکار بیانیه‌های مسائل زبان طبیعی به بیانیه‌های رسمی، یک پل بین این دو حوزه مکمل ایجاد کرد و در نهایت کتابخانه ای بزرگ از مسائل رسمی با سطوح دشواری متفاوت ایجاد شد.
هنگامی که با یک مسئله مواجه می‌شود، AlphaProof گزینه‌های حل را تولید می‌کند و سپس آنها را با جستجو بر روی مراحل اثبات احتمالی در Lean اثبات یا رد می‌کند. هر اثباتی که پیدا و تأیید شد برای تقویت مدل زبان AlphaProof استفاده می‌شود و توانایی آن را برای حل مسائل چالش‌برانگیز بعدی افزایش می‌دهد.
ما AlphaProof را برای المپیاد جهانی ریاضی با اثبات یا رد میلیون‌ها مسئله، پوشش طیف گسترده‌ای از دشواری‌ها و حوزه‌های موضوعی ریاضی در طول چند هفته منتهی به رقابت آموزش دادیم. حلقه آموزشی همچنین در طول مسابقه اعمال شد و اثبات‌های تغییرات خودساخته مسائل مسابقه را تا زمانی که یک راه حل کامل پیدا شود، تقویت کرد.
AlphaGeometry 2 رقابتی‌تر
AlphaGeometry 2 نسخه بهبود یافته قابل توجهی از AlphaGeometry است. این یک سیستم ترکیبی عصبی-سمبولی است که در آن مدل زبان بر اساس Gemini بوده و از ابتدا بر روی یک مرتبه بزرگتر از داده‌های مصنوعی نسبت به سلف خود آموزش دیده است. این به مدل کمک کرد تا با مشکلات هندسه بسیار چالش‌برانگیزتر، از جمله مشکلات مربوط به حرکت اشیاء و معادلات زاویه، نسبت یا فاصله مقابله کند.
AlphaGeometry 2 از یک موتور نمادین استفاده می‌کند که دو مرتبه سریع‌تر از سلف خود است. هنگام مواجهه با یک مشکل جدید، از یک مکانیسم به اشتراک‌گذاری دانش جدید برای فعال کردن ترکیبات پیشرفته درختان جستجوی مختلف برای مقابله با مشکلات پیچیده‌تر استفاده می‌شود.
قبل از رقابت امسال، AlphaGeometry 2 توانست ۸۳ درصد از تمام مسائل هندسه المپیاد جهانی ریاضی تاریخی از ۲۵ سال گذشته را حل کند، در مقایسه با نرخ ۵۳ درصدی که توسط سلف خود به دست آمده بود. برای المپیاد جهانی ریاضی ۲۰۲۴، AlphaGeometry 2 مسئله ۴ را در عرض ۱۹ ثانیه پس از دریافت رسمی‌سازی آن حل کرد.
مشخصات فنی سیستم‌های هوش مصنوعی AlphaProof و AlphaGeometry 2
Tech Specs
- مدل پایه: مدل زبان از پیش آموزش دیده
- داده‌های آموزشی: میلیون‌ها مسئله ریاضی به زبان رسمی
- الگوریتم یادگیری: AlphaZero
- وظیفه: اثبات قضایای ریاضی
افق‌های جدید در استدلال ریاضی
به عنوان بخشی از کار المپیاد جهانی ریاضی ما، ما همچنین با یک سیستم استدلال زبان طبیعی آزمایش کردیم که بر اساس Gemini و تحقیقات اخیر ما برای فعال کردن مهارت‌های حل مسئله پیشرفته ساخته شده است. این سیستم نیازی به ترجمه مسائل به یک زبان رسمی ندارد و می‌تواند با سایر سیستم‌های هوش مصنوعی ترکیب شود. ما همچنین این رویکرد را روی مسائل المپیاد جهانی ریاضی امسال آزمایش کردیم و نتایج نویدبخش بود.
تیم‌های ما به کاوش رویکردهای مختلف هوش مصنوعی برای پیشبرد استدلال ریاضی ادامه می‌دهند و قصد دارند جزئیات فنی بیشتری را در مورد AlphaProof منتشر کنند.
ما برای آینده‌ای هیجان‌زده هستیم که در آن ریاضیدانان با ابزارهای هوش مصنوعی برای کاوش فرضیه‌ها، امتحان کردن رویکردهای جدید جسورانه برای حل مسائل طولانی‌مدت و تکمیل سریع عناصر زمان‌بر اثبات‌ها همکاری می‌کنند – و جایی که سیستم‌های هوش مصنوعی مانند Gemini در ریاضیات و استدلال گسترده‌تر توانمندتر می‌شوند.