ویژهنامه هوش مصنوعی ساینتیفیک امریکن
آغاز عصر نوین در اثباتهای ریاضی
سید محمدجواد فیاض- ۳ اسفند ۱۴۰۴
همکاری هوش مصنوعی و انسان احتمالاً میتواند به پیشرفتهای فرابشری در ریاضیات دست یابد.
ریاضیدانان ایدهها را با مطرحکردن حدسها و اثبات آنها با قضیهها کاوش میکنند. برای قرنها، ریاضیدانان این اثباتها را خطبهخط و با دقت مینوشتند و اکثر پژوهشگران ریاضی امروز نیز هنوز به همین روش کار میکنند. اما هوش مصنوعی آماده است تا این فرایند را به طور اساسی تغییر دهد. دستیارهای هوش مصنوعی در حال به کمک به ریاضیدانان در توسعه اثباتها کردهاند؛ با این احتمال واقعی که این ابزارها روزی به انسانها اجازه دهند به مسائلی پاسخ دهند که در حال حاضر فراتر از تصور ذهن ما هستند.
دستیار هوشمند کلتک؛ گامی نوی در تدوین اثباتها
یک دستیار هوش مصنوعی نویدبخش در Caltech درحالتوسعه است که میتواند به طور خودکار گامهای بعدی در یک اثبات را پیشنهاد دهد، در تکمیل اهداف ریاضیات سطح متوسط کمک کند و به ساخت بافت پیوندی منطقی بین گامهای بزرگتر کمک کند. «آنیماشری آناندکومار» (Animashree Anandkumar) استاد علوم کامپیوتر و ریاضی در Caltech میگوید: «اگر من درحالتوسعه یک اثبات باشم، این دستیار جدید پیشنهادها متعددی برای پیش رفتن به من میدهد.» آناندکومار همراه با تیمش، این دستیار هوش مصنوعی را در آوریل ۲۰۲۴ در یک مقاله پیشچاپ ارائه کرد که تا زمان انتشار نسخه اصلی این گزارش، هنوز مورد داوری همتا قرار نگرفته است. آناندکومار معتقد است نکته حیاتی این است که آن پیشنهادها «همگی درست خواهند بود.»
ترکیب مدلهای زبانی با دقت منطقی نرمافزار «لین»
این دستیار یک مدل زبانی بزرگ است، همان نوع سیستم یادگیری ماشین که پشت ChatGPT و Gemini قرار دارد. اگرچه آموزش آن متفاوت است؛ اما شبیه به فناوریای است که AlphaProof و AlphaGeometry 2 گوگل از آن استفاده میکنند که هر دو اثباتهای ریاضی پیچیدهای را در سطح استاندارد مدال نقره در المپیاد بینالمللی ریاضی (IMO) سال ۲۰۲۴ تولید کردند. LLMها میتوانند آنچه را که به معنای فنی «چرند» (Bullshit) است تولید کنند؛ اما پیشنهادها اشتباه یک دستیار بررسی و رد میشوند. در مورد دستیار Caltech، این غربالگری به کمک نرمافزاری مبتنی بر هوش مصنوعی به نام «لین» (Lean) که از منطق ریاضی دقیق برای غربالکردن گزارههای معتبر استفاده میکند، انجام میشود.
فرمالیزهسازی؛ پایانی بر خطاهای انسانی در داوری
در طول چند سال گذشته، Lean در میان یک پایگاه کاربری کوچک اما روبهرشد محبوب شده است. این نرمافزار متنباز به ریاضیدانان اجازه میدهد تا ریاضیات خود را با کدنویسی وارد کنند؛ فرایندی که بهعنوان «فرمولیسازی» (Formalizing) شناخته میشود. مزیت آن چیست؟ هرگز اشتباه نمیکند. در Lean و سایر برنامههای دستیار اثبات، نرمافزار به طور خودکار گزارههای ریاضی را از نظر صحت بررسی میکند. این دنیایی دور از ریاضیات سنتی و بهاصطلاح غیررسمی است، جایی که داوران و همکاران با زحمت صفحات چنین گزارههایی را ممیزی میکنند. آن فرایند مستعد خطای انسانی است و اشتباهات نادیده گرفته میشوند.
پیشنهادهای تاکتیکی؛ کدنویسی به سبک هوشمند
اگر با کمک دستیار Caltech در حال نوشتن یک اثبات هستید، میتوانید روی دکمهای کلیک کنید تا خطوط جدیدی از زبان برنامهنویسی Lean را برای نمایش ریاضیاتی که با آن کار میکنید درخواست کنید. چندین گزینه که آناندکومار آنها را «پیشنهادها تاکتیکی» مینامد، در سمت راست صفحه ظاهر میشوند؛ سپس شما بهسادگی هر گزینهای که مناسبترین به نظر میرسد را انتخاب میکنید. اگر اثبات شما در جهتی پیش میرود که نتایج متوسط بدیهی یا شناختهشدهای دارد، دستیار همچنین میتواند پیشنهاد دهد که چگونه آن مسیر را کامل کنید.
چالشهای پذیرش؛ از سختی کدنویسی تا حذف کارهای یدی
«مارتین هایرر» (Martin Hairer) استاد ریاضیات محض در مؤسسه فدرال فناوری سوئیس و کالج امپریال لندن میگوید: «هیچ عدم اعتمادی» نسبت به Lean وجود ندارد؛ زیرا نرمافزار کار را بررسی میکند. بااینحال، بسیاری از دانشگاهیان هنوز آن را نپذیرفتهاند. هایرر میگوید: «استفاده از آن سخت است؛ زیرا باید تمام عملیات ریاضی را بهصورت کد وارد کنید.» او خاطرنشان میکند که کدنویسی در Lean مستلزم واردکردن جزئیاتی است که هنگام نوشتن یک مقاله حذف میشود، بنابراین ممکن است چندین صفحه کد لازم باشد تا آنچه که خودبهخود درست یا بدیهی است را نشان دهد.
اما هایرر که در پروژه Caltech دخیل نیست، معتقد است که دستیارهای هوش مصنوعی در نهایت تمام آن کارهای یدی و خستهکننده را از بین خواهند برد و میگوید: «هنگامی که گزارهای را ارائه میدهید که برای اکثر ریاضیدانان بدیهی است، یک LLM باید بتواند کد آن را تولید کند» و میافزاید که این فرایند سریعتر، میتواند «احتمالاً نسل جدیدی از ریاضیدانان را به سمت Lean جذب کند.»
آناندکومار نیز پیشبینی میکند که پژوهشگران بیشتری ریاضیات رسمی به کمک هوش مصنوعی را خواهند پذیرفت. او میگوید: «امروز وقتی با ریاضیدانان جوان یا حتی دانشجویان کارشناسی صحبت میکنم، میبینم که آنها با این سیستمهای هوش مصنوعی آشنا هستند. آنها هر کاری لازم باشد انجام میدهند تا کار را سریعتر و آسانتر کنند تا مزیت رقابتی به دست آورند.»
از مدال المپیاد تا مرزهای پژوهشهای پیشرفته
قبل از اینکه جامعه بینالمللی ریاضی ابزارهای هوش مصنوعی را به روشی معنادار بپذیرد، این پلتفرمها باید بسیار قدرتمندتر شوند. AlphaProof و AlphaGeometry 2 گوگل با استاندارد مدال نقره خود در IMO سال ۲۰۲۴، نتایج قابلتوجهی را نشان دادهاند. اما آنها هنوز به سطحی نرسیدهاند که ریاضیدانان پژوهشی برای کمک در اثباتهای پیچیده نیاز دارند؛ انسانها در این زمینه هنوز ریاضیدانان تواناتری هستند.
بااینحال «دیوید سیلور» (David Silver)، معاون یادگیری تقویتی در گوگل DeepMind میگوید: «بهزودی سیستمهایی ساخته خواهند شد که به آن سطح نزدیک میشوند. من فکر میکنم چنین چیزی اساساً ریاضیدانان انسانی را به جایگاهی ارتقا میدهد که قادر باشند در سطح بسیار بالاتری به فعالیت بپردازند و به ایدهها بیندیشند.» او معتقد است ریاضیات در حال دگرگونی است، درست مثل زمانی که ماشینحساب الکترونیکی اختراع شد و میگوید: «در زمان قبل از ماشینحساب، طیف وسیعی از ریاضیات وجود داشت که بسیار پرزحمت بود و تلاش زیادی میطلبید. فکر میکنم ما اکنون در مرحله مشابهی برای مفهوم اثبات ریاضی هستیم و در آینده شاهد حل خودکار اثباتهای بسیار پیچیده توسط هوش مصنوعی خواهیم بود.»
تغییر الگوی همکاری؛ از انزوای فردی تا کار تیمی گسترده
پذیرش دستیارهای هوش مصنوعی نحوه کار ریاضیدانان با یکدیگر را نیز دگرگون خواهد کرد. به طور معمول آنها بهتنهایی یا در گروههای کوچک کار میکنند. همکاران مورداعتماد اثباتهای آنها را تکهتکه ارزیابی میکنند. اما دستیاران رسمی هوش مصنوعی میتوانند گروههای بزرگتری از همکاران انسانی را توانمند سازند تا با شکستن بزرگترین مسائل به زیرمسئلهها، با آنها روبهرو شوند. هر بخش دستهبندی میشود تا توسط تیمهای مختلفی از همکاران متخصص هوش مصنوعی-انسان حل شود. آناندکومار میگوید: «ریاضیات بهویژه در رسانههای عمومی بهعنوان حوزه بسیار تنها دیده میشود؛ اما اکنون به نظر میرسد هوش مصنوعی سبب تسهیل همکاری میان ریاضیدانان خواهد شد.»
ریاضیدانان بهطورکلی خوشبین هستند که دستیارهای هوش مصنوعی بهزودی متخصصان انسانی را توانمندتر کنند که به آنها اجازه میدهند زمان خود را در مسائل پیچیدهتر و دشوارتر صرف کنند. برای مثال، در سالهای آینده مشارکتهای هوش مصنوعی-انسان ممکن است شانس خود را در «مسائل جایزه هزاره» (Millennium Prize Problems) که بهدشواری معروف هستند، امتحان کنند؛ شاید حتی چیزی به چالشبرانگیزی «مسئلهP در برابر NP»، یک پرسش قدیمی در علوم کامپیوتر نظری که میپرسد آیا هر مسئلهای که راهحل آن میتواند بهسرعت تأیید شود، میتواند بهسرعت حل شود؟
سیلور درحالیکه مفهوم حل چنین پرسشهایی را در نظر میگیرد میگوید: «این جایی است که ما بهزودی خود را در حال رفتن به سمت آن خواهیم یافت. مسائلی به پیچیدگی «مسئلهP در برابر NP»، بسیار فراتر از جایی هستند که ما امروز حتی از نظر دانستن نحوه شروع در آن قرار داریم. اما میتوانم تصور کنم که شاید در حدود سه سال دیگر، ممکن است در مسیر چیزی شبیه به آن باشیم.»
