حمایت ۱۵ میلیون دلاری سیمونز، اوپن‌ای‌آی و آنتروپیک از کاربرد هوش مصنوعی در ریاضیات
هوش مصنوعی می‌تواند به ریاضی‌دانان کمک کند مسائل و پرسش‌هایی را بررسی کنند که حل آن‌ها در گذشته سال‌ها زمان می‌برد. اما وقتی یک ماشین راه‌حلی برای یک مسئله یا یک اثبات ریاضی پیشنهاد می‌کند، پژوهشگران چگونه می‌توانند مطمئن شوند که نتیجه واقعاً درست است؟
بنیاد سیمونز با همکاری اوپن‌ای‌آی و آنتروپیک، طرحی ۱۵ میلیون دلاری را برای کمک به ریاضی‌دانان در ارزیابی و استفاده از ابزارهای هوش مصنوعی راه‌اندازی کرده است؛ طرحی که در عین بهره‌گیری از این فناوری، بر حفظ دقت و سخت‌گیری علمیِ زیربنای ریاضیات تأکید دارد.
این برنامه که ۱۵ اکتبر ۲۰۲۶ اعلام شد، از طرح‌های جامعه پژوهشی، کارگاه‌ها و دسترسی به ابزارهای هوش مصنوعی و منابع محاسباتی حمایت خواهد کرد. هدف برنامه صرفاً قرار دادن ابزارهای بیشتر هوش مصنوعی در اختیار ریاضی‌دانان نیست، بلکه کمک به پژوهشگران برای تصمیم‌گیری درباره نحوه آزمودن، اعتماد کردن و استفاده از این سامانه‌هاست.
کمک به ریاضی‌دانان برای تعیین قواعد
بنیاد سیمونز، اوپن‌ای‌آی و آنتروپیک در مجموع ۱۵ میلیون دلار بودجه و منابع اختصاص خواهند داد. این بنیاد بر نحوه تخصیص حمایت‌ها نظارت می‌کند و از پژوهشگران می‌خواهد از طریق یک فراخوان عمومی، پیشنهادهای خود را ارائه کنند.
این حمایت‌ها به کارگاه‌ها و طرح‌های تحت رهبری جامعه پژوهشی اختصاص خواهد یافت؛ طرح‌هایی که به پژوهشگران کمک می‌کنند نتایج حاصل از همکاری با هوش مصنوعی را ارزیابی کنند، نحوه استفاده از ابزارهای نوظهور را بیاموزند و درباره استانداردهای مشترک تبادل نظر کنند. اوپن‌ای‌آی و آنتروپیک نیز ابزارهای هوش مصنوعی و منابع محاسباتی را در اختیار پژوهشگرانی قرار خواهند داد که تحت حمایت بنیاد هستند.
این حمایت فراتر از ریاضیات خواهد بود و علوم پایه را نیز دربر می‌گیرد. تأکید بر مشارکت جامعه پژوهشی در این طرح اهمیت زیادی دارد، زیرا پژوهش ریاضی بر استدلال دقیق و اثبات‌های قابل راستی‌آزمایی استوار است.
سامانه‌های هوش مصنوعی ممکن است به شناسایی الگوها، پیشنهاد راه‌حل‌ها یا رسمی‌سازی استدلال‌ها کمک کنند، اما پژوهشگران همچنان به روش‌های قابل اتکا برای بررسی درستی نتایج نیاز دارند.
تکیه بر ابزارهای بررسی اثبات
دیوید اسپرگل، رئیس بنیاد سیمونز، گفت هدف این طرح گرد هم آوردن جامعه ریاضی در شرایطی است که هوش مصنوعی در حال تغییر شکل پژوهش است. او تأکید کرد که ریاضیات صرفاً مجموعه‌ای از اثبات‌ها و قضیه‌ها نیست، بلکه تلاشی مشترک است که کنجکاوی انسان آن را پیش می‌برد.
این بنیاد بر حمایت‌های پیشین خود از ریاضیات، یادگیری ماشین برای علوم و Lean تکیه می‌کند؛ Lean یک دستیار اثبات است که به پژوهشگران کمک می‌کند استدلال‌های ریاضی را به‌صورت رسمی و گام‌به‌گام راستی‌آزمایی کنند.
ابزارهایی مانند Lean راهی برای بررسی این موضوع فراهم می‌کنند که آیا استدلال‌های ریاضی الزامات سخت‌گیرانه رسمی را برآورده می‌کنند یا خیر. این بنیاد همچنین کارگاه‌ها، سخنرانی‌ها و همکاری‌هایی را برگزار کرده است تا پژوهشگران بتوانند نقش هوش مصنوعی در این حوزه را بررسی کنند.
حفظ نقش محوری قضاوت انسانی
با افزایش توانایی سامانه‌های هوش مصنوعی در کمک به فعالیت‌های ریاضی، پژوهشگران با پرسش‌هایی فراتر از این موضوع روبه‌رو هستند که آیا یک مدل می‌تواند پاسخی ارائه کند یا نه. آن‌ها همچنین باید مشخص کنند نتایج چگونه باید راستی‌آزمایی و بررسی شوند و چگونه می‌توان آن‌ها را در شیوه‌های تثبیت‌شده پژوهش علمی وارد کرد.
این طرح ۱۵ میلیون دلاری به ریاضی‌دانان امکان می‌دهد در توسعه این رویکردها نقش داشته باشند و تصمیم‌گیری‌ها صرفاً در اختیار شرکت‌های هوش مصنوعی باقی نماند.
هوش مصنوعی می‌تواند مسیرهای تازه‌ای برای کشف‌های ریاضی باز کند. تعیین اینکه چگونه می‌توان به دستاوردهای این فناوری اعتماد کرد، به همان اندازه گسترش توانایی‌های خود فناوری اهمیت خواهد داشت.