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