کامپیوترها برای گرفتن مدال طلا در المپیاد ریاضی آماده می‌شوند

منتشر‌شده در: مجله quanta به تاریخ ۲۱ سپتامبر ۲۰۲۰
لینک منبع: At the Math Olympiad, Computers Prepare to Go for the Gold

شصت و یکمین المپیاد بین‌المللی ریاضی، یا IMO، امروز تمام می‌شود. این رویداد ممکن است حداقل به دو دلیل در تاریخ ثبت شود: با توجه به شیوع ویروس کرونا، این اولین باری است که این رویداد از راه دور برگزار می‌شود، و همچنین ممکن است آخرین باری باشد که هوش مصنوعی در این رقابت حضور ندارد.

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

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

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

مسائل IMO ساده هستند، اما تنها به این معنا که به هیچ ریاضی پیشرفته‌ای نیاز ندارند-حتی حساب دیفرانسیل و انتگرال فراتر از حوزه رقابت در نظر گرفته می‌شود. آن‌ها همچنین شدیدا سخت هستند. برای مثال، این پنجمین مسئله از رقابت ۱۹۸۷ در کوبا است:

فرض کنید n عددی بزرگ‌تر یا مساوی با ۳ باشد. اثبات کنید که مجموعه‌ای از n نقطه در صفحه وجود دارد به طوری که فاصله بین هر دو نقطه غیر منطقی است و هر مجموعه از سه نقطه یک مثلث غیر تبهگن با مساحت منطقی را تعیین می‌کند.

مانند بسیاری از IMO مسائل، این مورد ممکن است در ابتدا غیر ممکن به نظر برسد.

کوین بازارد از کالج سلطنتی لندن، یکی از اعضای تیم گراند چلنج IMO و برنده مدال طلا در ۱۹۸۷ IMO گفت: «شما پرسش‌ها را می‌خوانید و فکر می‌کنید: من نمی‌توانم این را حل کنم. آن‌ها سوالات بسیار سختی هستند که در دسترس دانش‌آموزان قرار می‌گیرند؛ اگر آن‌ها تمام ایده‌هایی که می‌دانند را به شکل هوشمندانه‌ای کنار هم بگذارند.»

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

به عنوان مثال، یکی از قدیمی‌ترین نتایج در ریاضیات، اثبات اقلیدس از ۳۰۰ سال پیش از میلاد است که تعداد بی‌نهایت عدد اول وجود دارد. با این تشخیص شروع می‌شود که همیشه می‌توانید با ضرب کردن تمام اعداد اول شناخته‌شده و اضافه کردن ۱. دلیل پشت آن ساده است، اما رسیدن به ایده اولیه یک عمل هنری بود.

بازارد می‌گوید: «شما نمی‌توانید کاری کنید که کامپیوتر به این ایده برسد. حداقل هنوز نمی‌توانید.»

گرند چلنج IMO از یک برنامه نرم‌افزاری به نام Lean استفاده می‌کند که اولین بار در سال ۲۰۱۳ توسط یک محقق مایکروسافت به نام لئوناردو دومورا راه‌اندازی شد. Lean یک «دستیار اثبات» است که کار ریاضی دانان را بررسی می‌کند و برخی از بخش‌های خسته‌کننده نوشتن اثبات را خودکار می‌کند.

دومورا و همکارانش می‌خواهند از Lean به عنوان «حل‌کننده»ای استفاده کنند که قادر به ابداع اثبات‌های خود از مسائل IMO است. اما در حال حاضر، حتی نمی‌تواند مفاهیم درگیر در برخی از مسائل را درک کند. اگر قرار است بهتر عمل کند، دو چیز باید تغییر کنند.

ابتدا، Lean باید ریاضی بیشتری یاد بگیرد. این برنامه از کتابخانه‌ای از ریاضیات به نام مت‌لیب استفاده می‌کند که همیشه در حال رشد است. امروزه این کتابخانه تقریبا هر چیزی که یک دانشجوی رشته ریاضی ممکن است تا پایان سال دوم کالج خود بداند را در بر می‌گیرد، اما با برخی شکاف‌های ابتدایی که برای IMO مهم هستند.

چالش بزرگ‌تر این است که به Lean آموزش دهیم با دانش خود چه کار کند. تیم گرند چلنج IMO می‌خواهد Lean را آموزش دهد تا به روشی که با آن سایر سیستم‌های هوش مصنوعی با موفقیت بازی‌های پیچیده مانند شطرنج را-با دنبال کردن یک درخت تصمیم‌گیری تا زمانی که بهترین حرکت را پیدا کند- به اتمام می‌رسانند، به یک اثبات ریاضی برسد.

بازارد گفت: «اگر ما بتوانیم کاری کنیم که یک کامپیوتر، با داشتن هزاران و هزاران ایده و رد کردن همه آن‌ها تا زمانی که به ایده درست برسد، به هوشمندانه‌ترین و بدیع‌ترین ایده دست پیدا کند، شاید بتوانیم چالش بزرگ IMO را حل کنیم.»

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

سلسام گفت: « یک گام کلیدی در بسیاری از مسائل IMO بازی کردن با آن و جستجوی الگوها است.» البته واضح نیست که چطور باید به یک کامپیوتر بگویید با یک مسئله «بازی کند».

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

سلسام گفت: « هیچ چیزی وجود ندارد که برای مسئله بعدی نیز کارساز باشد.»

برای کمک به این مساله، تیم گرند چلنج IMO به ریاضی دانانی نیاز دارد تا اثبات رسمی دقیق مسائل قبلی IMO را بنویسند. سپس تیم این شواهد را برمی دارد و سعی می‌کند تا تکنیک‌ها، یا استراتژی‌هایی را که آن‌ها را به کار می‌اندازد، از آن پیدا کند. سپس آن‌ها یک سیستم هوش مصنوعی را آموزش می‌دهند تا در میان آن استراتژی‌ها یک ترکیب «برنده» را پیدا کند که مسائلی در IMO که هرگز قبلا دیده نشده‌اند را حل کند. سلسام می‌گوید که نکته مهم این است که برد در ریاضی حتی از برد در بازی‌های رومیزی بسیار دشوارتر است. در این بازی‌ها، حداقل شما قوانین را می‌دانید.

او گفت: «شاید در بعضی از بازی‌ها هدف پیدا کردن بهترین حرکت باشد، در حالی که در ریاضی هدف پیدا کردن بهترین بازی و سپس پیدا کردن بهترین حرکت در آن بازی است.»

گرند چلنج IMO در حال حاضر یک هدف دور از دسترس است. دومورا گفت اگر Lean در رقابت امسال شرکت می‌کرد، «ما احتمالا به نمره صفر می‌رسیدیم».

اما محققان معیارهای متعددی دارند که سعی دارند قبل از رویداد سال آینده به آن‌ها برسند. آن‌ها قصد دارند تا شکاف‌های مت‌لیب را از بین ببرند تا Lean بتواند همه سوالات را بفهمد. آن‌ها همچنین امیدوارند که اثبات‌های رسمی دقیقی از ده‌ها مسئله IMO قبلی داشته باشند، که فرآیند تهیه یک کتاب بازی پایه برای Lean را آغاز خواهد کرد.

در آن زمان ممکن است یک مدال طلا هنوز دور از دسترس باشد، اما حداقل Lean می‌تواند برای شرکت در مسابقه صف بکشد.

سلسام گفت: « در حال حاضر بسیاری از چیزها در حال رخ دادن هستند، اما هیچ چیز مشخصی برای اشاره به آن وجود ندارد.» [ سال آینده ] این کار به یک تلاش واقعی تبدیل می‌شود.»

این متن با استفاده از ربات ترجمه مقالات ترجمه شده و به صورت محدود مورد بازبینی انسانی قرار گرفته است.در نتیجه می‌تواند دارای برخی اشکالات ترجمه باشد.