آژانس پروژه های تحقیقاتی پیشرفته دفاعی ایالات متحده (DARPA) بر این باور است که ریاضیات به اندازه کافی سریع پیشرفت نمی کند.
بنابراین، برای تسریع - یا "نمایی کردن" - نرخ تحقیقات ریاضی، دارپا این هفته یک رویداد "روز پیشنهاد دهندگان" برگزار کرد تا با جامعه فنی تعامل کند، به این امید که شرکت کنندگان پیشنهادات خود را برای ارسال پس از انتشار درخواست گسترده آژانس (BAA) واقعی آماده کنند.
پروژه دارپا با نام expMath، قصد دارد با کمک هوش مصنوعی یا یادگیری ماشین، نوآوری در ریاضیات را آغاز کند.
این آژانس در وب سایت خود توضیح می دهد: «هدف از نمایی کردن ریاضیات (expMath) تسریع اساسی نرخ پیشرفت در ریاضیات محض از طریق توسعه یک نویسنده همکار هوش مصنوعی است که قادر به پیشنهاد و اثبات انتزاعات مفید باشد.»
پاتریک شفتو، مدیر برنامه دارپا، در این رویداد که در مرکز کنفرانس دارپا در آرلینگتون، ویرجینیا برگزار شد، با نشان دادن اینکه چگونه ریاضیات بین سالهای 1878 و 2018 به آرامی پیشرفت کرده است، استدلال کرد که تحقیقات ریاضی باید تسریع شود.
این زمینه ها تغییراتی را تجربه کرده اند، اما ریاضیات اینطور نبوده است، و کاری که ما می خواهیم انجام دهیم این است که این تغییر را در ریاضیات ایجاد کنیم.
در طول این مدت، پیشرفت ریاضیات - که با لگاریتم تعداد سالانه انتشارات علمی اندازه گیری می شود - با نرخی کمتر از 1 درصد رشد کرد.
این بر اساس تحقیقاتی است که در سال 2021 توسط لوتز بورنمان، رابین هاونشیلد و رودیگر موتز انجام شد، که نرخ کلی رشد علمی را در رشته های مختلف 4.10 درصد محاسبه کردند.
تحقیقات علمی همچنین موجی از نوآوری را به همراه دارد. به عنوان مثال، در علوم زیستی، دوران ژان باتیست لامارک (1744-1829) و چارلز داروین (1809-1882)، دوره بین سالهای 1806 و 1848 شاهد نرخ رشد انتشار 8.18 درصد بود. و در علوم فیزیکی و فنی، رشد 25.41 درصدی بین سالهای 1793 و 1810 ثبت شد، دورهای که مصادف با کار مهم ژوزف-لویی لاگرانژ (1736-1813) بود.
شفتو در طول سخنرانی خود گفت: «بنابراین این زمینهها تغییراتی را تجربه کردهاند، اما ریاضیات اینطور نبوده است، و کاری که ما میخواهیم انجام دهیم این است که این تغییر را در ریاضیات ایجاد کنیم.»
شتاب دهنده نوآوری پیشنهادی دارپا، هوش مصنوعی است. اما مشکل این است که هوش مصنوعی آنقدرها هم هوشمند نیست. می تواند ریاضیات سطح دبیرستان را انجام دهد اما نه ریاضیات سطح بالا.
همانطور که در یکی از اسلایدهای شفتو اشاره شده است، "OpenAI o1 (توت فرنگی) علیرغم ادعاهای قابلیت های استدلال، همچنان در ریاضیات پایه به طرز اسفناکی شکست می خورد."
با این وجود، هدف expMath این است که مدل های هوش مصنوعی را قادر سازد تا:
- تجزیه خودکار - به طور خودکار عبارات زبان طبیعی را به لم های زبان طبیعی قابل استفاده مجدد تجزیه کند (یک گزاره اثبات شده برای اثبات گزاره های دیگر استفاده می شود). و
- خودکار (در) فرموله کردن - لم زبان طبیعی را به یک اثبات رسمی ترجمه کند و سپس اثبات را به زبان طبیعی برگرداند.
رابین رو، بنیانگذار و مدیر عامل موسسه تحقیقات هوش مصنوعی Fountain Abode، در این رویداد شرکت کرد. همانطور که او به The Register توضیح داد، او در کالج در رشته ریاضیات تحصیل کرد، اما آن را کسل کننده یافت، بنابراین به علوم کامپیوتر رفت.
با این وجود، او گفت، برایش جالب بود که به نظر می رسد هدف این است که یک ریاضیدان هوش مصنوعی ایجاد شود که بتواند به عنوان یک همکار خدمت کند، کسی که معادل یک دانشجوی فارغ التحصیل باشد که قادر به کمک به اثبات است.
او گفت، این سطح بالاتری از شایستگی است که در حال حاضر در مدل های هوش مصنوعی نشان داده می شود.
رو گفت: «اکنون ما زنجیره تفکر داریم. بنابراین این مانند زنجیره تفکر روی استروئیدها است.»
- از آنجایی که ChatGPT در مهندسی نمره B- می گیرد، اساتید برای به روز رسانی دوره ها تلاش می کنند
- آخرین مدل های Google DeepMind تا حدودی در المپیاد ریاضی مدال نقره می گیرند
- علی بابا در مسابقات سالانه ریاضیات خود، مردم را در برابر هوش مصنوعی قرار می دهد
- بالاخره! راه حلی برای 42 - پاسخ به سوال نهایی زندگی، جهان و همه چیز
برای رو، سوال این است که چگونه می توان هوش مصنوعی را در ریاضیات پیشرفته بهتر کرد.
رو گفت: «پاتریک شفتو، که مدیر پروژه این کار است، مقاله [PDF] در مورد استقرای بیزی را نوشته است، که ایده این است که شما می توانید این را با استفاده از یک مدل زبان بزرگ بفهمید.
«این روشی نیست که من به آن تمایل دارم، اما روشی است که بسیاری از افراد در اتاق به آن تمایل دارند، زیرا این تا حدودی واضح ترین گام بعدی است اگر قرار است از فناوری موجود استفاده کنید.
به نظر من ما به استدلال ریاضی نیاز داریم.
«برای افرادی که در اتاق هستند، می گویند، «اوه، می دانید، LLM ها در سال گذشته بسیار بهتر شده اند. ما به همین منوال ادامه خواهیم داد.» این نشان دهنده نگرانی دارپا در مورد اینکه این چقدر سخت است، این است که این یک برنامه سه ساله است. این برای دارپا عادی نیست.»
«اما برای خودم، چیزی که فکر میکنم به آن نیاز داریم استدلال ریاضی است. پیشنهادات هنوز ارائه نشده اند، اما این جهتی است که ما قصد داریم در پیش بگیریم. اما افراد دیگری نیز در آنجا بودند که دیدگاه متفاوتی داشتند، مانند انجام استدلال ریاضی هندسی و چیزهایی از این دست. احتمالاً ده ها روش مختلف برای انجام این کار وجود دارد.»
به عبارت دیگر، رو مطمئن نیست که تمرکز بر زبان طبیعی مسیر درستی است. او پیشنهاد می کند مدل های مبتنی بر ورودی بصری یا صوتی در ریاضیات پیشرفته ماهرتر خواهند بود.
رو پرسید: «آیا ما استقرای بیزی را در LLM ها انتخاب می کنیم، که به نظر می رسد اگر این رشته شما بود، اولین چیزی است که به آن فکر می کنید، یا به چیزی رادیکال تر مانند مدل سازی هندسی روی می آوریم و آن را به صورت بصری انجام می دهیم، به عنوان مثال، به جای استفاده از کلمات؟
«و در اتاق مورد بحث قرار نگرفت، اما ریاضیدانانی هستند که در سر خود محاسبات صوتی انجام می دهند - آنها اعداد را به عنوان تن های موسیقی احساس می کنند. بنابراین چیزهای عجیب و غریب زیادی وجود دارد که مردم می توانند پیشنهاد دهند اگر ما آن را بر اساس نحوه انجام اثبات توسط ریاضیدانان در زندگی واقعی مدل سازی کنیم، زیرا روش های مختلفی وجود دارد. اکثر مردم فقط در مورد روش های رایج می دانند، زیرا این چیزهای دیگر مستلزم آن است که شما نوعی توانایی نبوغ داشته باشید که عادی نیست.»
با این حال، رو خوشبین است. من فکر می کنم ما آن را از بین خواهیم برد، صادقانه بگویم. فکر نمی کنم سه سال طول بکشد. اما فکر می کنم انجام آن با LLM ها ممکن است سه سال طول بکشد. بنابراین سوال این است که همه چقدر مایل به رادیکال بودن هستند؟»