هوش مصنوعی و معمای اثباتهای ریاضی: وقتی ماشینها با اعتماد به نفس بالا استدلال میکنند
- ریاضیدانان از توانایی مدلهای هوش مصنوعی مانند o4-mini در ارائه استدلالهای پیچیده و متقاعدکننده شگفتزده شدهاند.
- نگرانی اصلی، پذیرش اثباتهای تولیدشده توسط هوش مصنوعی است که ممکن است ظاهری قوی اما حاوی اشتباهات پنهان داشته باشند.
- استفاده از زبانهای تأیید صوری مانند Lean میتواند راهحلی برای اعتبارسنجی دقیق استدلالهای هوش مصنوعی باشد.
- آیندهای محتمل است که در آن هوش مصنوعی اثباتهایی کاملاً صحیح اما برای انسان غیرقابل درک تولید کند.
- این تحول، پرسشهای فلسفی عمیقی درباره ماهیت و هدف ریاضیات به عنوان یک رشته انسانی مطرح میکند.
شگفتی و نگرانی در مواجهه با استدلالهای هوش مصنوعی
در یک گردهمایی محرمانه در سال ۲۰۲۵، گروهی از برجستهترین ریاضیدانان جهان گرد هم آمدند تا آخرین مدل زبان بزرگ OpenAI با نام o4-mini را بیازمایند. آنچه آنها مشاهده کردند، حیرتآور بود. پاسخهای مدل به حدی شبیه به استدلال یک ریاضیدان واقعی در حین ارائه یک اثبات پیچیده بود که کارشناسان را مبهوت کرد.
کن اونو، استاد نظریه اعداد در دانشگاه ویرجینیا، در این باره گفت: «من قبلاً هرگز چنین نوعی از استدلال را در مدلها ندیده بودم. این دقیقاً کاری است که یک دانشمند انجام میدهد.» اما این ستایش، همراه با یک هشدار بود. آیا به این مدل هوش مصنوعی بیش از حد اعتبار داده میشود؟ آیا ما در خطر پذیرش اثباتهای مشتقشده از هوش مصنوعی بدون درک کامل آنها قرار داریم؟
اونو خود اذعان کرد که این مدل ممکن است پاسخهای متقاعدکنندهای ارائه دهد که بالقوه نادرست هستند. او گفت: «اگر چیزی را با اعتماد به نفس کافی بیان کنید، مردم میترسند. به نظر من o4-mini بر "اثبات از طریق ارعاب" مسلط شده است؛ همه چیز را با اطمینان بسیار زیادی بیان میکند.»
شکستن ارتباط سنتی بین مهارت و بیان
در گذشته، اعتماد به نفس و ظاهر یک استدلال خوب، نشانههای مثبتی محسوب میشدند، زیرا تنها بهترین ریاضیدانان میتوانستند arguments متقاعدکننده ارائه دهند و استدلال آنان معمولاً صحیح بود. اما اکنون این قاعده شکسته شده است.
تری تائو، ریاضیدان دانشگاه UCLA و برنده مدال فیلدز سال ۲۰۰۶، توضیح میدهد: «اگر شما یک ریاضیدان ضعیف بودید، احتمالاً یک نویسنده ریاضی ضعیف نیز بودید و بر نکات اشتباه تأکید میکردید. اما هوش مصنوعی این سیگنال را شکسته است.» به عبارت دیگر، هوش مصنوعی میتواند ساختار و لحن یک استدلال قوی را تقلید کند، بدون اینکه لزوماً محتوای درستی داشته باشد.
طبیعتاً، ریاضیدانان شروع به نگرانی کردهاند که مبادا هوش مصنوعی آنها را با انبوهی از اثباتهای به ظاهر متقاعدکننده بمباران کند که در واقع حاوی اشکالاتی هستند که تشخیص آنها برای انسان دشوار است. تائو هشدار میدهد که استدلالهای تولیدشده توسط هوش مصنوعی ممکن است به اشتباه پذیرفته شوند، صرفاً به این دلیل که دقیق و سختگیرانه به نظر میرسند.
ضرورت احتیاط و استفاده از ابزارهای تأیید صوری
تری تائو بر احتیاط در پذیرش «اثباتهای» هوش مصنوعی تأکید میکند. او میگوید: «یک چیز که از استفاده از هوشهای مصنوعی آموختهایم این است که اگر به آنها یک هدف بدهید، برای رسیدن به آن هدف مانند دیوانهها تقلب خواهند کرد.» این هشدار نشان میدهد که خروجی هوش مصنوعی ممکن است برای رسیدن به یک نتیجه از پیش تعیینشده طراحی شده باشد، نه لزوماً برای کشف حقیقت ریاضی.
برای جلوگیری از چنین مشکلاتی، جنبشی در حال شکلگیری است تا اثباتها با چیزی که ریاضیدانان «زبانهای تأیید صوری» مینامند، تقویت شوند. معروفترین نمونه این برنامههای کامپیوتری، Lean نام دارد. در این روش، ریاضیدانان باید اثباتهای خود را به قالبی بسیار دقیق ترجمه کنند. سپس کامپیوتر هر گام را با اعمال منطق ریاضی دقیق بررسی میکند تا تأیید کند که استدلال ۱۰۰٪ صحیح است.
کوین بازارد، ریاضیدان کالج سلطنتی لندن، از طرفداران پیشرو این روش صوری است. او میگوید: «من به این دلیل وارد این کار شدم که نگران بودم اثباتهای انسانی ناقص و نادرست هستند و ما انسانها کار ضعیفی در مستندسازی استدلالهایمان انجام میدهیم.»
همکاری هوش مصنوعی و سیستمهای تأیید: آیندهای متحولکننده
ریاضیدانان بر این باورند که هوش مصنوعی، در همکاری با برنامههایی مانند Lean، میتواند بازی را به کلی تغییر دهد. تائو معتقد است: «اگر ما خروجی هوش مصنوعی را مجبور کنیم تا چیزها را به یک زبان تأییدشده صوری تولید کند، در اصل، این کار بیشتر مشکل تولید اثباتهای متقاعدکننده اما نهایتاً نادرست توسط هوش مصنوعی را حل میکند.»
بازارد با این دیدگاه موافق است. او تصور میکند که یک تعامل رفت و برگشتی بین Lean و هوش مصنوعی شکل بگیرد، جایی که Lean خطاها را نشان میدهد و هوش مصنوعی سعی در تصحیح آنها میکند. اگر مدلهای هوش مصنوعی بتوانند به گونهای ساخته شوند که با این زبانهای صوری کار کنند، آنگاه میتوانند برخی از دشوارترین مسائل ریاضی را با یافتن ارتباطاتی فراتر از محدوده خلاقیت انسان حل کنند.
مارک لکنبی، ریاضیدان دانشگاه آکسفورد، در این باره میگوید: «هوش مصنوعی در یافتن ارتباط بین حوزههای مختلف ریاضی که لزوماً به ذهن ما نمیرسد، بسیار خوب عمل میکند.»
اثباتی که هیچ کس نمیفهمد: یک آینده واقعی؟
اگر ایده اثباتهای تأییدشده صوری توسط هوش مصنوعی را تا نهایت منطقی آن پیش ببریم، آیندهای واقعبینانه در انتظار است: آیندهای که در آن هوش مصنوعی اثباتهایی «عینیاً صحیح» توسعه میدهد که آنقدر پیچیده هستند که هیچ انسانی قادر به درک آنها نیست.
این چشمانداز، ریاضیدانان را به روشی کاملاً متفاوت نگران میکند. این امر پرسشهای بنیادینی درباره هدف انجام ریاضیات به عنوان یک رشته علمی مطرح میکند. نهایتاً اثبات چیزی که هیچ کس نمیفهمد چه فایدهای دارد؟ و اگر چنین کنیم، آیا میتوان گفت که به مجموعه دانش بشری افزودهایم؟
با این حال، بازارد خاطرنشان میکند که مفهوم اثباتی آنقدر طولانی و پیچیده که هیچ کس روی زمین آن را نفهمد، برای ریاضیات جدید نیست. او مثال میزند: «مقالههایی در ریاضیات وجود دارند که هیچ کس کل مقاله را نمیفهمد. میدانید، مقالهای با ۲۰ نویسنده وجود دارد و هر نویسنده بخش خودش را میفهمد. هیچ کس کل مطلب را نمیفهمد. و این اشکالی ندارد. روش کار همین است.»
پیشینه اثباتهای کامپیوتری و ورود به قلمروی ناشناخته
بازارد همچنین اشاره میکند که اثباتهایی که برای پر کردن شکافها به کامپیوتر متکی هستند، چیز جدیدی نیستند. او میگوید: «ما دههها است که اثباتهای کمککامپیوتری داشتهایم.» یک مثال کلاسیک، قضیه چهاررنگ است که میگوید برای رنگآمیزی هر نقشهای حداکثر به چهار رنگ نیاز است تا هیچ دو منطقه همسایه همرنگ نباشند.
تقریباً ۵۰ سال پیش، در سال ۱۹۷۶، ریاضیدانان مسئله را به هزاران مورد کوچک و قابل بررسی تقسیم کردند و برنامههای کامپیوتری برای تأیید هر یک نوشتند. اولین اثبات کمککامپیوتری این قضیه در سال ۱۹۷۷ منتشر شد. اعتماد به این اثبات به تدریج در طول سالها افزایش یافت و با ارائه یک اثبات سادهتر اما همچنان کمککامپیوتری در سال ۱۹۹۷ و یک اثبات صوری تأییدشده توسط ماشین در سال ۲۰۰۵ تقویت شد.
اما این مثالها از اثباتهای کمککامپیوتری و کار تیمی ریاضی، با سناریوی پیشنهاد، تطبیق و تأیید یک اثبات به طور کامل توسط هوش مصنوعی — اثباتی که شاید هیچ انسان یا تیمی از انسانها هرگز امید درک آن را نداشته باشد — اساساً متفاوت احساس میشود.
تحول ماهیت اثبات و پرسشهای فلسفی بنیادین
صرف نظر از اینکه ریاضیدانان آن را بپذیرند یا نه، هوش مصنوعی در حال تغییر ماهیت خود اثباتها است. برای قرنها، عمل تولید و تأیید اثبات، تلاشی انسانی بوده است — استدلالهایی که برای متقاعد کردن دیگر ریاضیدانان انسانی ساخته شدهاند. ما در حال نزدیک شدن به وضعیتی هستیم که در آن ماشینها ممکن است منطقی بینقص تولید کنند، منطقی که توسط سیستمهای صوری تأیید شده است، اما حتی بهترین ریاضیدانان نیز از دنبال کردن آن عاجز خواهند بود.
در آن سناریوی آینده — اگر محقق شود — هوش مصنوعی هر مرحله، از پیشنهاد گرفته تا آزمایش و تأیید اثباتها را انجام خواهد داد و همانطور که لکنبی میگوید: «و بعد شما برنده شدهاید. شما چیزی را اثبات کردهاید.» با این حال، این رویکرد یک سؤال فلسفی عمیق را برمیانگیزد: اگر یک اثبات به چیزی تبدیل شود که فقط یک کامپیوتر میتواند آن را درک کند، آیا ریاضیات همچنان یک تلاش انسانی باقی میماند، یا به چیزی کاملاً متفاوت تکامل مییابد؟ و این باعث میشود که یکی به این فکر کند که هدف نهایی چیست.
منبع: Livescience
اخبار علم و فناوری