ابزارهای یادگیری ماشینی در حال حاضر به ریاضیدانان کمک می‌کنند تا نظریه‌های جدید را فرموله و مسائل سخت را حل کنند. اما آنها قرار است این حوزه را بیشتر از این دگرگون کنند.
در حالی که علاقه به چت بات‌ها در حال گسترش است، ریاضیدانان به کشف اینکه چگونه هوش مصنوعی می‌تواند به آنها در انجام فعالیت‌هایشان کمک کند، می‌پردازند. به گفته محققان، فرقی نمی‌کند که هوش مصنوعی به تایید دست نوشته‌های انسان کمک کند یا راه‌هایی جدید برای حل مسائل دشوار پیشنهاد دهد، تغییر در این زمینه آغاز شده و این فراتر از محاسبات است.
اندرو گرانویل (Andrew Granville)، نظریه پرداز اعداد در دانشگاه مونترال کانادا می‌گوید: ما به یک سوال بسیار خاص توجه داریم: آیا ماشین‌ها ریاضیات را تغییر می‌دهند؟
یک کارگاه آموزشی در دانشگاه کالیفرنیا، لس آنجلس (UCLA)، این هفته این سوال را با هدف ایجاد پل‌هایی میان ریاضیدانان و دانشمندان رایانه بررسی کرد. یکی از سازمان دهندگان این رویداد، مارین هیول (Marijn Heule)، دانشمند رایانه در دانشگاه کارنگی ملون در پیتسبورگ، پنسیلوانیا، می‌گوید: بیشتر ریاضیدانان کاملا از این فرصت‌ها بی اطلاع هستند.
هوش مصنوعی نزدیک می‌شود
بخشی از بحث به این موضوع مربوط می‌شود که چه نوع ابزارهای خودکاری مفیدتر خواهند بود. هوش مصنوعی دو نوع اصلی دارد. در هوش مصنوعی نمادین، برنامه نویسان قوانین منطقی یا محاسباتی را در کدهایی که می‌نویسند تعبیه می‌کنند. لئوناردو دی مورا(Leonardo de Moura)، دانشمند رایانه در تحقیقات مایکروسافت در ردموند، واشنگتن، می‌گوید: این چیزی است که مردم به آن «هوش مصنوعی قدیمی خوب» می‌گویند.
رویکرد دیگر، که در یک دهه گذشته بسیار موفق بوده است، مبتنی بر شبکه عصبی مصنوعی است. در این نوع هوش مصنوعی، رایانه کم و بیش از یک لوح خالی شروع به کار می‌کند و با هضم مقادیر زیادی داده، الگوها را یاد می‌گیرد. این مورد یادگیری ماشینی نامیده می‌شود و اساس «مدل‌های زبانی بزرگ» مانند چت‌بات‌هایی همچون «ChatGPT» و سیستم‌هایی که می‌توانند کاربران انسانی را در بازی‌های پیچیده شکست دهند یا چگونگی تا شدن پروتئین‌ها را پیش‌بینی کنند، از این دست است. در حالی که هوش مصنوعی نمادین ذاتا دقیق است، شبکه‌های عصبی فقط می‌توانند حدس‌های آماری داشته باشند و عملیات آنها اغلب مرموز است.
دی مورا با ایجاد سیستمی به نام «لین»(Lean) به این هوش مصنوعی نمادین کمک کرد تا به موفقیت‌های اولیه ریاضی دست یابد. این نرم افزار تعاملی محققان را وادار می‌کند تا هر مرحله منطقی از یک مسئله را تا ابتدایی‌ترین جزئیات بنویسند و از درستی ریاضیات آن اطمینان حاصل کنند. دو سال پیش، تیمی از ریاضیدانان موفق شدند صحت یک برهان مهم اما غیرقابل نفوذ که به قدری پیچیده بود که حتی نویسنده‌اش هم از آن مطمئن نبود را با کمک لین تایید کنند.
محققان می‌گویند، این فرآیند به آنها کمک کرد تا این برهان را درک کنند و حتی راه‌هایی برای ساده‌سازی آن بیابند. دی مورا می‌گوید: من فکر می‌کنم این حتی هیجان‌انگیزتر از صحت‌یابی است.
علاوه بر آسان‌تر کردن کار انفرادی، این نوع «دستیار اثبات‌کننده» می‌تواند نحوه همکاری ریاضیدانان را با حذف آنچه که دی مورا «گلوگاه اعتماد» می‌نامد، تغییر دهد. وقتی ما با هم همکاری می‌کنیم، ممکن است به کاری که شما انجام می‌دهید اعتماد نداشته باشم. اما یک دستیار اثبات به همکاران شما نشان می‌دهد که می‌توانند به بخشی از کار شما اعتماد کنند.
تکمیل خودکار پیچیده
در سوی دیگر، مدل‌های زبانی بزرگ مبتنی بر شبکه عصبی قرار دارند. در شرکت گوگل در کالیفرنیا، فیزیکدان سابق ایتان دایر(Ethan Dyer) و تیمش یک چت‌بات به نام مینروا(Minerva) ساخته‌اند که در حل مسائل ریاضی تخصص دارد. مینروا نسخه بسیار پیچیده‌ای از عملکرد تکمیل خودکار در پیام‌رسان‌ها است. این هوش مصنوعی که با استفاده از مقالات ریاضی پایگاه arXiv، آموزش دیده است با روشی مشابه کاری که برخی از اپلیکیشن‌ها بوسیله آن می‌توانند کلمات و عبارات را پیش‌بینی کنند، می‌تواند گام به گام راه حل‌هایی برای مسائل ارائه کند. برخلاف لین که با استفاده از چیزی شبیه به کد رایانه‌ای ارتباط برقرار می‌کند، مینروا سوالات را می‌پذیرد و پاسخ‌ها را به زبان انگلیسی و به شکل مکالمه ارائه می‌دهد. دی مورا می‌گوید: حل کردن برخی از این مسائل به صورت خودکار یک دستاورد است.
مینروا هم قدرت و هم محدودیت‌های احتمالی این رویکرد را نشان می‌دهد. به عنوان مثال، می‌تواند اعداد صحیح را به طور دقیق به اعداد اول تبدیل کند اما زمانی که اعداد از اندازه معینی فراتر رفت اشتباهات آن شروع شد و این نشان می‌دهد که این هوش مصنوعی روند کلی را «درک» نکرده است.
با این وجود، به نظر می‌رسد که شبکه عصبی مینروا می‌تواند برخی از روش‌های کلی را برخلاف الگوهای آماری به دست آورد و تیم گوگل در تلاشند تا بفهمند چگونه این کار را انجام می‌دهد. دایر می‌گوید: در نهایت، ما مدلی را می‌خواهیم که بتوان با آن طوفان فکری کرد. او می‌گوید، این می‌تواند برای غیرریاضی‌دانانی که نیاز به استخراج اطلاعات از متون تخصصی دارند نیز مفید باشد. افزونه‌های بیشتر، مهارت‌های مینروا را با مطالعه کتاب‌های درسی و ارتباط با نرم‌افزارهای اختصاصی ریاضی گسترش می‌دهد.
دایر می گوید، انگیزه پشت پروژه مینروا این بود که ببینیم رویکرد یادگیری ماشینی تا کجا می‌تواند پیش برود. یک ابزار خودکار قدرتمند برای کمک به ریاضیدانان ممکن است در نهایت روش‌های هوش مصنوعی نمادین را با شبکه‌های عصبی ترکیب کند.
ریاضیات در مقابل ماشین‌ها
در درازمدت، آیا این برنامه‌ها به عنوان یک حامی باقی می‌مانند یا می‌توانند به طور مستقل تحقیقات ریاضی را انجام دهند؟
هوش مصنوعی ممکن است در تولید گزاره‌ها و برهان‌های صحیح ریاضی بهتر شود، اما برخی از محققان نگرانند که بیشتر آنها غیرجالب یا غیرقابل درک باشند. تیموتی گوورز(Timothy Gowers) برنده مدال فیلدز می‌گوید که ممکن است راه‌هایی برای آموزش برخی از شاخص‌های عینی برای ارتباط ریاضی به یک رایانه وجود داشته باشد، مانند اینکه آیا یک عبارت کوچک می‌تواند موارد خاص زیادی را در برگیرد یا حتی می‌توان پلی بین زیرشاخه‌های مختلف ریاضیات ایجاد کرد. او افزود: برای اینکه در اثبات قضایا بهتر شویم، رایانه‌ها باید قضاوت کنند که چه چیزی جالب است و ارزش اثبات دارد. اگر آنها بتوانند این کار را انجام دهند، آینده انسان‌ها در این زمینه نامشخص خواهد بود.
یک سیستم هوش مصنوعی به همان اندازه هوشمند است که ما آن را برنامه‌ریزی می‌کنیم. هوش درون رایانه وجود ندارد. هوش درون برنامه‌نویس یا مربی آن یافت می‌شود.
اریکا آبراهام (Erika Abraham)، دانشمند رایانه در آلمان، نسبت به آینده ریاضیدانان خوش‌بینانه‌تر فکر می‌کند. او می‌گوید: یک سیستم هوش مصنوعی به همان اندازه هوشمند است که ما برنامه‌ریزی می‌کنیم. هوش درون رایانه وجود ندارد. هوش درون برنامه‌نویس یا مربی آن یافت می‌شود.
ملانی میچل (Melanie Mitchell)، دانشمند علوم رایانه و دانشمند علوم شناختی در موسسه سانتافه در نیومکزیکو، می‌گوید که شغل ریاضیدانان تا زمانی که کاستی‌های عمده هوش مصنوعی برطرف نشود، ایمن خواهد بود.
ناتوانی هوش مصنوعی در استخراج مفاهیم انتزاعی از اطلاعات واقعی جزو این کاستی‌ها است. در حالی که سیستمهای هوش مصنوعی می‌توانند قضایا را اثبات کنند، ارائه انتزاعات ریاضی جالبی که در وهله اول باعث پیدایش قضایا می‌شوند، بسیار سخت‌تر است.