OpenAI ریاضیات را برای اثبات Navier-Stokes خود به اشتباه به کد تبدیل کرد

اثبات های تولید شده توسط هوش مصنوعی اغلب با استفاده از فرآیندی به نام رسمی سازی بررسی می شوند

تیمی از ریاضیدانان ادعا کرده اند که OpenAI هنگام انتشار شواهد خود در مورد مسئله Navier-Stokes یک خطای ظریف مرتکب شده است. این خطا به این معنی نیست که اثبات ها نادرست هستند یا OpenAI مشکل را به درستی حل نکرده است، اما این سوال را زیر سوال می برد که آیا می توان همیشه به نتایج ریاضی تولید شده توسط مدل های هوش مصنوعی اعتماد کرد.

آندرس هنسن از دانشگاه کمبریج می‌گوید: «آنچه باید با همه این شواهد بزرگ تولید شده توسط مدل‌های زبانی انجام شود این است که انسان‌ها باید آن‌ها را بخوانند، و این بار اضافی زیادی بر دوش ریاضیدانان ایجاد می‌کند.

در 8 سپتامبر، OpenAI اعلام کرد که راه حلی برای مسئله Navier-Stokes، یکی از مشهورترین مسائل باز در ریاضیات، پیدا کرده است. این اثبات را در دو نسخه منتشر کرد - یکی به زبان طبیعی نوشته شده بود، به معنای ترکیبی از نمادهای انگلیسی و ریاضی، همانطور که یک ریاضیدان انسانی می‌نویسد، و دیگری با کد کامپیوتری Lean. منظور از اثبات ناب، رسمی‌سازی نسخه زبان طبیعی است که به رایانه اجازه می‌دهد تا به صورت مکانیکی صحت تمام عبارات منطقی آن را تأیید کند. مشکل این است که هانسن و تیمش با هم مطابقت ندارند.

فابیان سیرچلی، عضو تیم، همچنین از دانشگاه کمبریج، می‌گوید: «این فرآیند رسمی‌سازی در تلاش است جایگزین بررسی همتا شود». "بررسی همتا به این معنی است که چشم انسان به شواهد نگاه می کند. اما آنچه در این مقاله نشان داده ایم این است که استفاده از این نوع رسمی سازی خودکار هوش مصنوعی نمی تواند همان هدف را دنبال کند."

برای روشن بودن، محققان نمی گویند که OpenAI در حل مشکل Navier-Stokes شکست خورده است. کاملا ممکن است که هم اثبات زبان طبیعی و هم اثبات ناب راه حلی ارائه دهند، همانطور که صدها اثبات معتبر برای قضیه فیثاغورث وجود دارد. در عوض، منظور آنها نکته ظریف تری است: اینکه مدل OpenAI هنگام تبدیل به Lean "به اشتباه ترجمه شده است".

هانسن می گوید: «ما نمی گوییم که اثبات زبان طبیعی اشتباه است. ما نمی گوییم که درست است.» مسئله این است که OpenAI این دو اثبات را یکسان ارائه می‌کند و در Github بیان می‌کند که «این مخزن حاوی 4 فرمول‌بندی ناب از نتایج ارائه‌شده در [مقاله] «فشار زمان محدود برای Navier-Stokes» است.

هانسن می‌گوید: این ترجمه اشتباه به این دلیل رخ می‌دهد که هوش مصنوعی باید یک اثبات ناب تولید کند که «کامپایل» می‌کند، به این معنی که کد رایانه کاملا سازگار است و خطایی ایجاد نمی‌کند. اگر در فرآیند رسمی‌سازی خودکار، هوش مصنوعی بخشی از اثبات را بیابد که کامپایل نمی‌شود، سعی می‌کند راه‌حلی پیدا کند، حتی اگر به معنای انحراف از اثبات نوشته شده به زبان طبیعی باشد.

ادعای خاص تیم به بخشی از شواهد به نام Lemma 8.6 بستگی دارد. در اثبات زبان طبیعی، یک معادله در این بخش مستلزم آن است که مقدار معینی زیر m + 4 باشد، جایی که m یک عدد کامل است. در اثبات ناب، مقدار معادل باید زیر m + 5 باشد، که از نظر ریاضی ضعیف‌تر است.

برای درک چرایی، تصور کنید که از شما خواسته می شود معادله x + 3 = 6 را حل کنید، که پاسخ آن x = 3 است. می توان اثباتی نوشت که x باید کمتر از 4 باشد و همچنین x باید کمتر از 5 باشد. اثبات دوم پاسخ‌های احتمالی بیشتری را برای x امکان‌پذیر می‌کند و آن را از نظر ریاضی ضعیف‌تر می‌کند.

OpenAI به New Scientist گفت که از عدم تطابق بین اثبات زبان طبیعی و کد ناب آگاه است و این بدان معنا نیست که هر یک از این اثبات‌ها نامعتبر هستند. این شرکت می‌گوید هر گونه خطا در اثبات زبان طبیعی را به محض یافتن تصحیح می‌کند، و همچنین به روند رسمی کردن 722 مقاله ریاضی که شرکت در این هفته منتشر کرد، ادامه می‌دهد، که فقط برخی از آنها با اثبات ناب همراه هستند، که خودشان با دست بررسی نشده‌اند.

سوزن در پشته اثبات

یافتن این واگرایی شامل یک فرآیند کمی سورئال از ChatGPT می‌شود تا به دنبال اختلافات احتمالی بین اثبات‌های زبان طبیعی و ناب بگردد، سپس آنها را با دست بررسی کند. بسیاری از اختلافات پیشنهاد شده توسط ChatGPT، پس از بررسی، ثابت شد. هانسن می‌گوید: «گذراندن تمام این موارد به صورت دستی یک کابوس بود.

در مجموع، شناسایی یک مغایرت واقعی، در مقایسه با ۸۸ ساعتی که OpenAI گفته است مامورانش برای ایجاد شواهد صرف کرده‌اند، حدود دو هفته طول کشید. الکساندر باستونیس عضو تیم در کینگز کالج لندن می گوید: "OpenAI به سرعت توانسته است این نتیجه را ایجاد کند، به خود می بالد، اما این تنها بخشی از فرآیند است."

اگر ریاضیدانان بخواهند به این نتایج اعتماد کنند، پاسخ به این سوال که آیا مدل‌های هوش مصنوعی می‌توانند ریاضیات را به‌طور خودکار رسمی‌سازی کنند، ضروری است. آندرس و تیمش نشان داده‌اند که ChatGPT می‌تواند یک نسخه ناب از اثباتی را تولید کند که با زبان طبیعی اصلی مطابقت ندارد، با هوش مصنوعی بی‌صدا استدلال منطقی را در این فرآیند تغییر می‌دهد تا هرگونه خطا را بپوشاند. هانسن می‌گوید: «این می‌خواهد به من کمک کند، اما با انجام این کار، کمکی نمی‌کند».

اگر قرار بود این برای یک اثبات طولانی و پیچیده اتفاق بیفتد، برای کسی بسیار دشوار خواهد بود که بدون بررسی دقیق هر دو نسخه متوجه شود. این موضوع فقط به دلیل دسته ای از 722 مقاله OpenAI که به تازگی منتشر شده است، شدیدتر است. هانسن می‌گوید: «اگر فکر کنیم همه این‌ها اکنون درست است، تنها کاری که اکنون باید انجام دهیم خواندن مقاله است»، پس این خطرناک است.» هدف از انجام علم این است که بشر باید درک کند که جهان چگونه کار می‌کند تا بتوانیم تصمیم‌های آموزش‌دیده بگیریم. اگر این درک را از دست بدهیم، چه کار می‌کنیم؟»

کوین بازارد از امپریال کالج لندن اشاره می کند که در بحث هایی مانند این، تمایز بین بیان یک قضیه و اثبات آن مهم است. برای مثال، بیان آخرین قضیه معروف فرما این است که برای عدد صحیح a، b، c و n، aⁿ + bⁿ = cⁿ فقط در صورتی که n 1 یا 2 باشد. تبدیل این قضیه به Lean آسان است و به راحتی قابل بررسی است. هنگامی که از درستی یک عبارت در Lean خوشحال هستید، اگر اثبات آن عبارت جمع‌آوری شود، می‌توانید مطمئن باشید که اثبات درست است.

مسئله، همانطور که هانسن و تیمش اشاره کرده اند، این است که این به شما چیزی در مورد نسخه به زبان طبیعی یک مدرک منتشر شده به عنوان یک سند PDF نمی گوید. بازارد می گوید: «من مطمئن هستم که مشکل ناویر-استوکس به درستی حل شده است. "من بسیار کمتر مطمئن هستم که مدرک توضیح داده شده در PDF درست است."

هانسن می‌گوید امیدوار است که OpenAI کار تیم را «بسیار جدی» بگیرد و باید کار بیشتری روی توسعه تکنیک‌های رسمی‌سازی خودکار قوی انجام شود. "آیا راه حلی داریم؟ هنوز نه. آیا می توان این کار را به صورت کنترل شده انجام داد؟ بله، خواهد بود، اما راه بهینه و نهایی انجام این کار کاملا ناشناخته است."