شاهکاری دیگر از هوش مصنوعی؛ فرمولهکردن اثبات ۱۳ میلیون خطی یک قضیه ریاضی در ۱۱ روز !
هوش مصنوعی آنتروپیک تنها در ۱۱ روز موفق به فرموله کردن «قضیه آخر فرما» شد.
کلود یک اثبات ۱۳ میلیون خطی و بررسیشده توسط رایانه برای این قضیه مشهور تولید کرده است که دستاوردی مهم برای دنیای ریاضیات به شمار میرود.
به نقل از نیچر، قضیه آخر فرما، یکی از مشهورترین نتایج ریاضی نیمقرن اخیر، برای نخستین بار با استفاده از نسخهای پیشرفته و آزمایشی از چتبات هوش مصنوعی کلود به کدی تبدیل شده که توسط رایانه قابل راستیآزمایی است.
الکس کونتوروویچ، نظریهپرداز اعداد در دانشگاه راتگرز در نیوجرسی، میگوید اینکه یک ماشین توانسته کار ریاضیدانان انسانی را به یک اثبات ۱۳ میلیون خطی و کاملا قابل اعتماد تبدیل کند، واقعا مغزم را منفجر کرد.
شرکت آنتروپیک، سازنده کلود، که در سانفرانسیسکو مستقر است، این دستاورد را در روز چهارم سپتامبر اعلام کرد. این مدل پروژهای را که پیشبینی میشد تکمیل آن برای انسانها ۱۰ سال زمان ببرد، در تنها ۱۱ روز به پایان رساند.
این نتیجه نشان میدهد که هوش مصنوعی احتمالا نقش مهمتری در بررسی و راستیآزمایی کار ریاضیدانان و همچنین تولید استدلالهای جدید ریاضی ایفا خواهد کرد.
با سرعت فعلی پیشرفت، دیگر چندان دور از ذهن نیست که هوش مصنوعی به زودی بتواند تمام کتابخانه دانش ریاضی را بررسی کند و حتی شاید مشخص شود که برخی از نتایج شناخته شده ریاضی اشتباه هستند.
کوین بازارد، ریاضیدان امپریال کالج لندن، میگوید: دو سال پیش، چنین چیزی یک خیال بود.
ریاضیدانان شگفتزده شدهاند
ریاضیدانان به طور فزایندهای از سرعت پیشرفت تواناییهای هوش مصنوعی در ریاضیات شگفتزده شدهاند. یکی از این تواناییها، مشخص کردن اثباتها است؛ یعنی تبدیل استدلالهای ریاضی که به زبان طبیعی نوشته شدهاند به کدی رسمی که رایانه بتواند صحت آن را تایید کند. این کار معمولا با استفاده از زبان برنامهنویسی Lean انجام میشود.
در ماه فوریه نیز هوش مصنوعی در زمینه رسمیسازی به دستاورد مهم دیگری رسید؛ زمانی که توانست کار مارینا ویازوفسکا، برنده مدال فیلدز، درباره کارآمدترین روشهای چیدن کرهها در فضاهای هشتبعدی یا ۲۴بعدی را به صورت رسمی تایید کند.
اما بازارد میگوید پروژه مربوط به قضیه آخر فرما از نظر پیچیدگی در سطح کاملا متفاوتی قرار دارد. او میگوید: این کار شاید یک مرتبه دشوارتر بود.
دانیل لیت، نظریهپرداز اعداد در دانشگاه تورنتو در کانادا نیز با این دیدگاه موافق است. او میگوید: اگر آنها بتوانند قضیه آخر فرما را فرموله کنند (formalize)، احتمالا میتوانند تقریبا هر چیزی را فرموله کنند.
اثباتی که بیش از سه قرن طول کشید
اثبات اصلی قضیه آخر فرما که در سال ۱۹۹۴ توسط اندرو وایلز و ریچارد تیلور تکمیل شد، یکی از دستاوردهای مهم ریاضیات قرن بیستم بود.
ریاضیدان اندرو وایلز در سال ۱۹۹۴ اثبات «آخرین قضیه فرما» را تکمیل کرد؛ بیش از ۳۵۰ سال پس از آنکه پیر فرما این قضیه را مطرح کرده بود.ریاضیدان فرانسوی، پیر دو فرما، در سال ۱۶۳۷ این ادعا را مطرح کرده بود، اما اثباتی برای آن ارائه نکرد. این مسئله بعدها به «قضیه آخر فرما» مشهور شد؛ هرچند در ریاضیات، یک گزاره تنها زمانی عنوان «قضیه» را دریافت میکند که به طور دقیق و منطقی اثبات شده باشد.
خودِ حل این معادله یا اثبات اینکه هیچ پاسخی برای آن وجود ندارد، کاربرد عملی چندانی ندارد. اما تکنیکهایی که وایلز برای حل این مسئله توسعه داد، به برقراری ارتباط میان حوزههای به ظاهر دور از هم در ریاضیات کمک کرد.
این اثبات در نهایت در سال ۲۰۱۶ برای وایلز جایزه آبل را به همراه داشت؛ یکی از معتبرترین جوایز جهان در ریاضیات.
فرموله کردن اثبات با Lean
فرموله کردن یک اثبات ریاضی در Lean نیازمند آن است که برنامه کامپایلر Lean با تمام مفاهیم مقدماتی و حقایق ریاضی شناختهشدهای که اثبات بر آنها تکیه دارد، آشنا شود.
برای امکانپذیر کردن فرمولهسازی نتایج پیشرفتهتر، ریاضیدانان طی سالها با زحمت، کتابخانهای از کدهای Lean به نام Mathlib ایجاد کردهاند.
از سال ۲۰۲۴، بازارد پروژهای را به طور اختصاصی برای قضیه آخر فرما هدایت کرده است. هدف این پروژه، گسترش Mathlib با تمام نتایج مقدماتی و هزاران صفحه از مطالب ریاضی موردنیاز برای رسمیسازی اثبات وایلز و تیلور بوده است. او تخمین میزند که تکمیل این پروژه برای انسانها حدود ۱۰ سال زمان ببرد.
اما کلود توانسته نسخه رسمی و فرموله شده خود از این اثبات را در تنها ۱۱ روز تولید کند. با این حال، یک نکته مهم وجود دارد.
برخلاف Mathlib، کدی که کلود تولید کرده که طبق اعلام آنتروپیک شامل حدود ۲۹ هزار و ۵۰۰ قضیه میانی است، هنوز به شکلی نیست که سایر ریاضیدانان بتوانند بلافاصله از آن استفاده کنند.
بازارد میگوید ادغام دستکم بخشی از این کد با Mathlib امکانپذیر است، اما انجام این کار به حجم بسیار زیادی از کار نیاز خواهد داشت.
در نتیجه، حتی اگر هوش مصنوعی بتواند تقریبا هر اثبات ریاضی را بررسی کند، جامعه ریاضی ممکن است با یک سناریوی کابوسوار مواجه شود: رشد کتابخانههای متعدد و ناسازگار Lean.
در مورد کار وایلز و تیلور، اثبات قضیه طی سالها به طور گسترده بررسی و بارها بازنویسی شده بود.
اگرچه پروژه بازارد برخی شکافهای جزئی موجود در اثبات را برطرف کرده بود، هیچکس انتظار نداشت که فرموله کردن کامل این اثبات با Lean به این سرعت انجام شود.
بازارد میگوید: قبلا ۹۹.۹ درصد مطمئن بودم که این اثبات درست است. اما بعد از کار آنتروپیک، حالا ۱۰۰ درصد مطمئنم.
با این حال، مقالات ریاضی پر از نمونههایی است که در آنها اثباتهایی صدها صفحهای وجود دارند، اما هنوز وضعیت مشخصی ندارند؛ برخی از اعضای جامعه علمی صحت آنها را قطعی میدانند و برخی دیگر همچنان نسبت به آنها تردید دارند.
اغلب، انتشار یک مقاله در یک مجله معتبر تنها نخستین گام برای پذیرش گستردهتر صحت یک نتیجه ریاضی است.
این مسئله درباره بسیاری از مقالات کمتر شناخته شده حتی جدیتر است؛ چراکه ممکن است تنها تعداد محدودی از ریاضیدانان آنها را مطالعه کنند.
آیا هوش مصنوعی داوری مقالات ریاضی را متحول میکند؟
بسیاری از ریاضیدانان امیدوارند که ترکیب فرموله کردن با هوش مصنوعی و تایید توسط Lean بتواند فرایند داوری و بررسی کار دیگر ریاضیدانان را به شدت سادهتر کند؛ کاری که در این حوزه میتواند بسیار دشوار و طاقتفرسا باشد.
با افزایش تعداد مقالات و طولانیتر و پیچیدهتر شدن آنها، داوری همتا زمان بیشتری میبرد، اما عملکرد آن ضعیفتر شده است. ارائه یک عصای جادویی به ریاضیدانان که بتوانند یک مقاله arXiv را وارد کنند و در مقابل، گواهی دریافت کنند که نشان دهد مقاله درست است، یا خطای موجود در آن را مشخص کند، میتواند واقعا ارزشمند باشد.
به این ترتیب، دستاورد کلود در فرموله کردن قضیه آخر فرما فقط یک نمایش قدرت برای هوش مصنوعی نیست؛ بلکه میتواند نشانهای از تغییر بزرگتری در ریاضیات باشد: حرکت از اعتماد انسانی به اثباتها، به سمت اثباتهایی که ماشینها نیز بتوانند صحت آنها را به طور قطعی بررسی کنند.
نظر شما