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

هوش مصنوعی اثبات‌های دقیق و مرحله به مرحله‌ای را ارائه کرد که توسط دو ریاضیدان برجسته به نام‌های جوزف مایرز و تیم گاورز ارزیابی شد و نمره ۲۸ از ۴۲ را به دست آورد؛ بدین معنی که فقط یک نمره تا محدوده‌ی مدال طلا فاصله داشت.

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

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

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

به‌گزارش نیچر، اولین هوش مصنوعی که در کل آزمون (شامل سؤالات جبر، ترکیبیات و نظریه اعداد که عمدتاً چالش‌برانگیزتر از هندسه درنظر گرفته می‌شود) بتواند در سطح مدال طلا عمل کند، واجد شرایط دریافت جایزه ۵ میلیون دلاری المپیاد ریاضی هوش مصنوعی (AIMO) خواهد بود.

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

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

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

آموزش هر مدل زبانی به حجم عظیمی از داده‌ها نیاز دارد، اما در لین تعداد معدودی اثبات ریاضی وجود داشت. توماس هوبرت که در توسعه آلفاپروف نقش داشته است، می‌گوید، برای غلبه بر این مشکل، تیم شبکه دیگری را طراحی کرد که تلاش کرد سوابق موجود از یک میلیون مسئله نوشته‌شده به زبان طبیعی را به لین ترجمه کند (اما بدون گنجاندن راه‌حل‌های نوشته‌شده توسط انسان). او می‌گوید: «رویکرد ما این بود که ببینیم اگر سیستم را با اثبات‌های نوشته‌شده به‌وسیله‌ی‌ انسان آموزش ندهیم، می‌تواند اثبات کردن را یاد بگیرد؟» (این شرکت رویکرد جدیدی در رابطه با گو داشت که در آن هوش مصنوعی آن یاد گرفت با بازی دربرابر خودش این بازی را یاد بگیرد).

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

گاورز در نشست مطبوعاتی گفت نتایج بهتر از انتظارات آن‌ها بود. او گفت: «بسیاری از مسائل موجود در IMO دارای ویژگی کلید جادویی هستند. مسئله در نگاه اول سخت به‌نظر می‌رسد تا زمانی که کلید جادویی را پیدا کنید که قفل آن را باز کند.»

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