OpenAI میگوید یکی از مدلهایش برای مسئله هزاره ناویر–استوکس یک راهحل پیشنهادی تولید کرده و در کنار توضیح ریاضی، نسخهای رسمی از برهان را نیز در Lean ارائه داده است. اهمیت بالقوه این خبر فقط به دشواری مسئله برنمیگردد؛ برای یکی از مشهورترین مسائل باز ریاضی، اکنون علاوه بر متن معمول برهان، یک شیء رسمی و قابل بررسی با ابزار اثبات نیز وجود دارد.
در وضعیت فعلی نباید این خبر را به شکل «حل قطعی مسئله» منتشر کرد. Nature آن را ادعایی با اهمیت بسیار بالا توصیف کرده که هنوز باید زیر بررسی جامعه ریاضی قرار گیرد و خود OpenAI نیز از عبارت «راهحل پیشنهادی» استفاده میکند. این تفاوت مهم است: بررسی ماشینی میتواند نشان دهد یک برهان رسمی از تعریفها و لمهای ثبتشده پیروی میکند، اما بهتنهایی ثابت نمیکند که صورت رسمی دقیقاً با مسئله مورد نظر ریاضیدانان یکسان است یا همه فرضها و تعریفها مورد پذیرش متخصصان هستند.
Lean بخشی از فرایند را از متن به اثبات قابل بررسی منتقل میکند
در ریاضیات معمول، بررسی یک برهان به خواندن دقیق متن، بازسازی گامهای حذفشده و کنترل فرضها توسط متخصصان وابسته است. رسمیسازی در Lean بخش قابل توجهی از این کار را به محیطی منتقل میکند که هر گام منطقی را بر اساس قواعد مشخص بررسی میکند.
این به معنی حذف نقش انسان نیست. متخصصان هنوز باید ببینند قضیهای که در Lean نوشته شده همان مسئلهای است که ادعا میشود، تعریفها با صورت پذیرفتهشده مسئله سازگارند و میان بیان غیررسمی و صورت رسمی شکاف مهمی وجود ندارد. اما پس از روشنشدن این تطابق، بررسی ماشینی میتواند بسیاری از خطاهای منطقی پنهان را سختتر کند.
برای ریاضیات تولیدشده با هوش مصنوعی، این موضوع اهمیت بیشتری دارد. مدلهای زبانی میتوانند استدلالهایی بسیار قانعکننده بسازند که در یک نقطه ظریف نقص دارند. برهان رسمی یک نمایش دوم فراهم میکند که اعتبارش کمتر به روانبودن متن وابسته است.
«ماشین تأیید کرد» با «جامعه پذیرفت» یکی نیست
تحلیل Aipolix این است که این پرونده سه مرحله متفاوت را از هم جدا میکند: درستی منطقی، تطابق دقیق با مسئله، و پذیرش علمی.
Lean میتواند بخشی از مرحله اول را پوشش دهد. مرحله دوم همچنان به بررسی متخصصان نیاز دارد تا روشن شود صورت رسمی دقیقاً همان ادعای مورد نظر مسئله هزاره است. مرحله سوم نیز به بازبینی مستقل، بازتولید استدلال و بررسی ارتباط آن با کارهای پیشین نیاز دارد.
این تفکیک فقط برای ناویر–استوکس مهم نیست. هرچه عاملها و مدلهای هوش مصنوعی بیشتر وارد پژوهش شوند، سازمانها باید زنجیرهای از شواهد نگه دارند که نشان دهد کدام بخش ماشینی بررسی شده، کدام بخش به قضاوت انسانی وابسته است و چه چیزهایی هنوز نامطمئناند.
منشأ و مسیر شکلگیری پژوهش به بخشی از کنترل کیفیت تبدیل میشود
در نتیجهای با این سطح از اهمیت، منشأ پژوهش هم اهمیت عملی پیدا میکند. برای بررسی درست باید مشخص باشد کدام بخشها توسط مدل ساخته شده، چه تعریفها یا لمهایی از کتابخانههای قبلی آمده، انسانها چه راهنماییهایی دادهاند و صورت نهایی قضیه در طول کار چگونه تغییر کرده است.
برهان رسمی مزیت مهمی دارد: یک شیء نسخهپذیر و قابل بازرسی ایجاد میکند. اما خودش به پرسشهایی درباره اولویت فکری، منابع ورودی یا سهم انسان پاسخ نمیدهد. برای این موضوع به ثبت جداگانه منابع، نشستهای مدل، نسخههای میانی و مداخلات انسانی نیاز است.
برای تیمهایی که هوش مصنوعی را وارد پژوهش میکنند، نتیجه روشن است: فایل اثبات، اطلاعات اجرای مدل، منابع و تغییرات انسانی باید کنار هم نگه داشته شوند. هرچه ادعا مهمتر باشد، نگهداشتن فقط نسخه نهایی مقاله قابل دفاع نیست.
این خبر شبیه یک رکورد بنچمارک نیست
بسیاری از خبرهای «هوش مصنوعی در ریاضی» با تعداد مسائل حلشده یا امتیاز یک مجموعه آزمون سنجیده میشوند. مسئله هزاره چنین ماهیتی ندارد. هیچ رتبهبندی کوتاهی نمیتواند جای بازبینی مستقل را بگیرد. ارزش ادعا به این بستگی دارد که استدلال جدید در برابر بررسی طولانی و تخصصی دوام بیاورد.
به همین دلیل، فرایند تأیید خودش بخشی از خبر است. نکته مهم فقط این نیست که مدل متنی تولید کرده که شبیه ریاضیات پیشرفته است؛ OpenAI اثری ارائه کرده که قرار است هم توسط ریاضیدانان و هم توسط یک سامانه اثبات رسمی بررسی شود.
اگر برهان پذیرفته شود، اهمیت آن بسیار فراتر از یک رشد امتیاز خواهد بود و نمونهای از مشارکت مستقیم هوش مصنوعی در پژوهش مرزی به شمار میرود. اگر ایرادی پیدا شود، همین پرونده میتواند نشان دهد رسمیسازی ماشینی دقیقاً کدام نوع خطاها را میگیرد و کجا هنوز به تفسیر انسان نیاز داریم.
در ادامه باید چه شواهدی را دنبال کرد
مهمترین مرحله بعدی، بازبینی مستقل ریاضی است. بررسی عمومی فایلهای Lean، تلاش دیگران برای بازتولید یا سادهکردن برهان، نظر متخصصان درباره انطباق صورت رسمی با مسئله اصلی و هر اصلاحیهای که منتشر شود، از نشانههای اصلی خواهند بود.
همچنین باید دید OpenAI مرز میان کار مدل و کار انسان را تا چه حد شفاف ثبت میکند. در پژوهش مبتنی بر هوش مصنوعی، این مرز در حال تبدیلشدن به بخشی از حاکمیت پژوهش است.
فعلاً جمعبندی دقیق این است: OpenAI یک راهحل پیشنهادی برای ناویر–استوکس همراه با برهان رسمی Lean ارائه کرده و این قالب، امکان بررسی قویتری از متن عادی فراهم میکند. پذیرفتهشدن آن بهعنوان پاسخ نهایی هنوز نیازمند بررسی مستقل جامعه ریاضی است.