هوش مصنوعی دیپ مایند موفق به حل سوالات المپیاد ریاضی شد
هوش مصنوعی گوگل با اثبات توانایی خود در حل سؤالات المپیاد ریاضی، گامی مثبت در رقابت برای ایجاد اثبات‌های ریاضی برداشت.
دیپ مایند گوگل پس از شکست‌دادن انسان‌ها در زمینه‌های مختلف از بازی گو گرفته تا بازی‌های رومیزی استراتژیک، اکنون در آستانه پیشی‌گرفتن از دانش‌آموزان برتر جهان در حل مسائل ریاضی است. این شرکت یادگیری ماشین مستقر در لندن اعلام کرده است سیستم هوش مصنوعی آن‌ها چهار مسئله از شش مسئله المپیاد بین‌المللی ریاضی (IMO) سال ۲۰۲۴ را که ماه جاری در شهر باث بریتانیا به دانش‌آموزان داده شده بود، حل کرده است.
هوش مصنوعی اثبات‌های دقیق و مرحله به مرحله‌ای را ارائه کرد که توسط دو ریاضیدان برجسته به نام‌های جوزف مایرز و تیم گاورز ارزیابی شد و نمره ۲۸ از ۴۲ را به دست آورد؛ بدین معنی که فقط یک نمره تا محدوده‌ی مدال طلا فاصله داشت.
دیپ مایند و سایر شرکت‌ها در رقابت برای ساخت ماشین‌هایی هستند که بتوانند مسائل تحقیقاتی اساسی را در ریاضی حل کنند. این شرکت می‌گوید مسائل مطرح‌شده در المپیاد ریاضی امسال به معیاری برای پیشرفت برای دستیابی به این هدف تبدیل شده‌اند و به‌عنوان چالشی بزرگ برای یادگیری ماشین درنظر گرفته می‌شوند.
پوشمیت کوهلی، معاون علمی دیپ‌مایند در نشست خبری گفت: «اولین بار است که یک سیستم هوش مصنوعی توانسته است به عملکردی در سطح مدال دست پیدا کند. این نقطه عطف کلیدی در مسیر ایجاد اثبات‌کننده‌های پیشرفته قضایای ریاضی است.»
مسائل طر‌ح‌شده در المپیاد بین‌المللی ریاضی از چندین حوزه‌ی ریاضی است.
در ماه ژانویه، آلفاجئومتری دیپ‌مایند به عملکردی در سطح برنده‌شدن مدال در حل مسائل المپیاد ریاضی حوزه هندسه اقلیدسی دست پیدا کرد.
به‌گزارش نیچر، اولین هوش مصنوعی که در کل آزمون (شامل سؤالات جبر، ترکیبیات و نظریه اعداد که عمدتاً چالش‌برانگیزتر از هندسه درنظر گرفته میشود) بتواند در سطح مدال طلا عمل کند، واجد شرایط دریافت جایزه ۵ میلیون دلاری المپیاد ریاضی هوش مصنوعی (AIMO) خواهد بود.
پژوهشگران در آخرین تلاش خود، از آلفاجئومتری ۲ برای حل مسئله هندسه در کمتر از ۲۰ ثانیه استفاده کردند. آن‌ها برای انواع دیگر سؤالات، سیستم کاملاً جدیدی به نام آلفاپروف را ایجاد کردند. آلفاپروف دو مسئله جبر و همچنین یک مسئله در حوزه نظریه اعداد را حل کرد (حل آن سه روز طول کشید. به شرکت‌کنندگان در المپیاد ریاضی واقعی دو جلسه فرصت داده میشود که هر جلسه ۴٫۵ ساعت است). سیستم نتوانست دو مسئله دیگری را که در زمینه‌ی ترکیبیات بود، حل کند.
پژوهشگران در تلاش برای پاسخگویی به سؤالات ریاضی با مدل‌های زبانی (سیستمی که چت‌بات‌هایی مانند چت جی‌پی‌تی با آن عمل می‌کنند) به نتایج مختلفی دست پیدا کردند. این مدل‌ها گاهی پاسخ صحیح می‌دهند، اما قادر به توضیح منطقی استدلال خود نیستند و گاهی نیز پاسخ اشتباه می‌دهند.
چندی پیش، گروهی از پژوهشگران از شرکت‌های نرم‌افزاری نومینا و هاگینگ‌فیس از مدل زبانی برای برنده شدن در رقابتی استفاده کردند که مبتنی بر نسخه‌های ساد‌ه‌ای از مسائل المپیاد ریاضی بود. این شرکت‌ها کل سیستم‌های خود را به‌صورت متن‌باز در دسترس سایر پژوهشگران قرار دادند تا در صورت نیاز آن‌ها را دانلود کنند. اما برندگان این رقابت گفتند مدل‌های زبانی به‌تنهایی برای حل مسائل سخت‌تر کافی نیستند.
آلفاپروف مدل زبانی را با تکنیک یادگیری تقویتی ترکیب می‌کند و از موتور آلفازیرو استفاده می‌کند. در یادگیری تقویتی، شبکه عصبی با آزمون و خطا یاد می‌گیرد. این سیستم زمانی به خوبی جواب می‌دهد که بتوان پاسخ‌های آن را با معیارهای عینی ارزیابی کرد. برای این منظور، آلفاپروف برای خواندن و نوشتن اثبات‌ها به زبان رسمی به نام لین (Lean) آموزش داده شد که در بسته نرم‌افزاری «دستیار اثبات» استفاده میشود.
آموزش هر مدل زبانی به حجم عظیمی از داده‌ها نیاز دارد، اما در لین تعداد معدودی اثبات ریاضی وجود داشت. توماس هوبرت که در توسعه آلفاپروف نقش داشته است، می‌گوید، برای غلبه بر این مشکل، تیم شبکه دیگری را طراحی کرد که تلاش کرد سوابق موجود از یک میلیون مسئله نوشته‌شده به زبان طبیعی را به لین ترجمه کند (اما بدون گنجاندن راه‌حل‌های نوشته‌شده توسط انسان). او می‌گوید: «رویکرد ما این بود که ببینیم اگر سیستم را با اثبات‌های نوشته‌شده به‌وسیله‌ی انسان آموزش ندهیم، می‌تواند اثبات کردن را یاد بگیرد؟» (این شرکت رویکرد جدیدی در رابطه با گو داشت که در آن هوش مصنوعی آن یاد گرفت با بازی دربرابر خودش این بازی را یاد بگیرد).
کلیدهای جادویی
بسیاری از ترجمه‌های لین بی‌معنا اما به اندازه کافی خوب بودند که آلفاپروف را به نقطه‌ای برسانند که بتواند چرخه‌های یادگیری تقویتی خود را شروع کند.
گاورز در نشست مطبوعاتی گفت نتایج بهتر از انتظارات آن‌ها بود. او گفت: «بسیاری از مسائل موجود در IMO دارای ویژگی کلید جادویی هستند. مسئله در نگاه اول سخت به‌نظر می‌رسد تا زمانی که کلید جادویی را پیدا کنید که قفل آن را باز کند.»
موفقیت هوش مصنوعی گوگل نقطه عطف مهمی در توسعه اثبات‌کننده‌های قضایای ریاضی با استفاده از هوش مصنوعی محسوب میشود
در برخی موارد، به‌نظر می‌رسید آلفاپروف در حل مسائل ریاضی می‌تواند حتی خلاقیت به خرج دهد اما به‌گفته‌ی گاورز برای تعیین این موضوع که آیا هوش مصنوعی واقعاً می‌تواند در حل مسائل ریاضی خلاقیت داشته باشد، به تجزیه‌وتحلیل بیشتری نیاز است. بحث مشابهی پس از «حرکت ۳۷» ربات آلفاگو دیپ‌مایند در شکست معروف سال ۲۰۱۶ برترین بازیکن گو جهان اتفاق افتاد که نقطه عطفی برای هوش مصنوعی بود.
مایرز در کنفرانس مطبوعاتی گفت مطالعات آینده می‌توانند نشان دهند که آیا می‌توان این تکنیک‌ها را تا حد انجام کارهای تحقیقاتی در ریاضی کامل کرد و آیا می‌توان آن را به انواع دیگر مسائل ریاضی که برایشان یک میلیون مسئله مشابه برای آموزش سیستم نداریم، گسترش داد یا خیر.