آنتروپیک می‌گوید کلود نیز فرضیه زمان نمایی را با استفاده از ۱۴ میلیون توکن رد کرده است
آنتروپیک مقاله‌ای به تاریخ ۲۶ اکتبر ۲۰۲۶ منتشر کرده است که در آن می‌گوید یک مدل پژوهشی داخلی کلود توانسته فرضیه زمان نمایی (ETH) را رد کند؛ همان فرضیه‌ای که اوپن‌ای‌آی نیز در ۲۶ اکتبر اعلام کرد مدل داخلی این شرکت آن را رد کرده است. در مقاله آنتروپیک آمده است که الگوریتم اصلی در ۱۶ اکتبر و «با تولید ۱۴ میلیون توکن خروجی و بدون دخالت انسان» کشف شده است.
این مقاله با عنوان A 2o(n) Time Algorithm for 3-SAT به کلود و آنتروپیک نسبت داده شده است. نسخه‌ای از آن همراه با صورت‌بندی رسمی در زبان Lean 4، در ۲۷ اکتبر به مخزن عمومی ریاضیات صوری آنتروپیک در گیت‌هاب افزوده شد. مقاله مستقیماً به کار اوپن‌ای‌آی اشاره می‌کند: «به‌طور مستقل و هم‌زمان، یک مدل داخلی در اوپن‌ای‌آی مدعی شده است که نتیجه‌ای مشابه را اثبات کرده است.»
ویدئوی توضیحی
این ویدئو به بررسی ادعاهای دو آزمایشگاه درباره فرضیه ETH و رشته رویدادهای مرتبط با آن می‌پردازد و روایتش بر پایه گزارش‌های منتشرشده ماست.
نکته اصلی: از نظر ما، اکنون دو آزمایشگاه مدعی‌اند که مدل‌های داخلی‌شان در یک روز واحد فرضیه مشابهی را رد کرده‌اند. این وضعیت دو گزارش مستقل و دو صورت‌بندی رسمی در Lean از یک ادعا در اختیار پژوهشگران بیرونی قرار می‌دهد تا بتوانند آن‌ها را با یکدیگر مقایسه و بررسی کنند.
مقاله آنتروپیک چه می‌گوید؟
در مقاله آمده است که یک الگوریتم قطعی ارائه شده که مسئله 3-SAT را برای n متغیر، در زمانی کمتر از هر تابع نمایی با نرخ رشد ثابت حل می‌کند؛ این زمان با نماد ۲ به توان o(n) نوشته می‌شود. به گفته مقاله، الگوریتم علاوه بر تشخیص امکان‌پذیری فرمول، تعداد انتساب‌های متغیرها را که آن را ارضا می‌کنند نیز محاسبه می‌کند؛ مسئله‌ای دشوارتر که با عنوان #3-SAT شناخته می‌شود.
مسئله 3-SAT می‌پرسد آیا می‌توان به متغیرهای یک فرمول منطقی، که هرکدام مقدار درست یا نادرست می‌گیرند، مقادیری اختصاص داد تا کل فرمول برقرار باشد. فرضیه زمان نمایی که ایمپالیاوتزو و پاتوری مطرح کرده‌اند، بیان می‌کند که حل 3-SAT به زمان نمایی نیاز دارد. مقاله، بهترین الگوریتم قطعی پیشین را الگوریتمی با زمان اجرای O(1.328n) و بهترین الگوریتم تصادفی را الگوریتمی با زمان اجرای O(1.308n) معرفی می‌کند.
مقاله می‌گوید این نتیجه فرضیه قوی‌تر SETH را نیز رد می‌کند، اما فرضیه بردارهای متعامد را رد نمی‌کند؛ فرضیه‌ای که بسیاری از کران‌های پایین در نظریه پیچیدگی ریزدانه بر آن متکی‌اند. طبق جست‌وجوی منابع علمی که کلود انجام داده است، بیش از ۸۰۰ مقاله وجود دارد که دست‌کم یکی از نتایج خود را فقط تحت فرضیه ETH یا فرضیه‌ای که آن را نتیجه می‌دهد، اثبات می‌کنند.
چه مطالبی در ایکس منتشر شد؟
«الگوریتم اصلی در ۱۶ اکتبر توسط یک مدل پژوهشی داخلی کلود، با تولید ۱۴ میلیون توکن خروجی و بدون دخالت انسان، کشف شد. پژوهشگران آنتروپیک همراه با کلود روی بهبود نحوه ارائه نتیجه کار کردند و این مقاله را تهیه کردند.»
مخزن رسمی ریاضیات صوری آنتروپیک در گیت‌هاب، پوشه eth— لِوِنت آلپوگه (@__alpoge)، ۲۷ اکتبر، ساعت ۰۴:۰۰
لِوِنت آلپوگه که در نمایه ایکس خود به آنتروپیک اشاره کرده است، در ۲۷ اکتبر ۲۰۲۶، ساعت ۰۴:۰۰ به وقت هماهنگ جهانی، بخشی از مقاله درباره منشأ این دستاورد را منتشر کرد. در این بخش آمده است که الگوریتم اصلی «در ۱۶ اکتبر توسط یک مدل پژوهشی داخلی کلود، با تولید ۱۴ میلیون توکن خروجی و بدون دخالت انسان» کشف شده است. او همچنین پیوند پوشه مربوط به ETH در مخزن ریاضیات صوری آنتروپیک را درج کرد. این گزارش نیز همین عبارت را مستقیماً از مقاله نقل می‌کند.
«یک مدل داخلی آنتروپیک نیز فرضیه ETH را رد کرده است؛ آن هم با تنها ۱۴ میلیون توکن خروجی و از همان ۱۶ اکتبر.
ناگهان همه‌چیز هم‌زمان اتفاق می‌افتد.»— چابی (@kimmonismus)، ۲۷ اکتبر، ساعت ۰۴:۲۹
چابی (@kimmonismus) این مطلب را ۲۹ دقیقه بعد منتشر کرد: «یک مدل داخلی آنتروپیک نیز فرضیه ETH را رد کرده است؛ آن هم با تنها ۱۴ میلیون توکن خروجی و از همان ۱۶ اکتبر.» جمله «ناگهان همه‌چیز هم‌زمان اتفاق می‌افتد» برداشت شخصی نویسنده پست است. تاریخ ۱۶ اکتبر همان تاریخی است که اوپن‌ای‌آی نیز برای رد این فرضیه اعلام کرده است.
«این موضوع واقعاً گیج‌کننده است، اما یک مدل پژوهشی داخلی کلود نیز در ۱۶ اکتبر، به‌طور مستقل و با تولید ۱۴ میلیون توکن خروجی و بدون دخالت انسان، فرضیه زمان نمایی را رد کرده است. آنتروپیک می‌گوید پژوهشگرانش همراه با کلود برای بهبود نحوه ارائه نتیجه همکاری کردند و مقاله حاصل این همکاری است.»
— اندرو کران (@AndrewCurran_)، ۲۷ اکتبر، ساعت ۰۴:۲۰
اندرو کران این پست را ساعت ۰۴:۲۰ به وقت هماهنگ جهانی منتشر کرد و نوشت که موضوع «واقعاً گیج‌کننده» است، اما یک مدل پژوهشی داخلی کلود نیز در ۱۶ اکتبر، با تولید ۱۴ میلیون توکن خروجی و بدون دخالت انسان، به‌طور مستقل فرضیه زمان نمایی را رد کرده است. او توضیح نداد که چرا این ماجرا را گیج‌کننده می‌داند.
«باورنکردنی است: تنها یک روز پس از آنکه اوپن‌ای‌آی اعلام کرد مدلش فرضیه زمان نمایی را رد کرده است، آنتروپیک می‌گوید یک مدل داخلی کلود به‌طور مستقل به نتیجه‌ای متفاوت برای رد همان فرضیه رسیده و تاریخ کشف نیز دقیقاً یکسان است: ۱۶ اکتبر.
یک مدل پژوهشی داخلی کلود برای کشف الگوریتمی با زمان اجرای زیرنمایی برای 3-SAT، بدون دخالت انسان ۱۴ میلیون توکن خروجی تولید کرده است.
آنتروپیک اکنون نتیجه را در ۱٬۰۵۰ ماژول Lean صورت‌بندی رسمی کرده است؛ ماژول‌هایی که هم هسته Lean و هم هسته مستقل nanoda آن‌ها را بررسی می‌کنند.
نکته شگفت‌انگیزتر این است که آنتروپیک می‌گوید کلود اوپوس ۵٫۵ می‌تواند این رد را تنها از روی یک طرح فنی کوتاه دوباره استخراج کند.
انتشار آنتروپیک شامل ۱۵۳٬۱۹۱ خط کد در ۱٬۰۶۳ فایل است.
مقاله می‌گوید هنوز کسی شناسایی نشده است که کل صورت‌بندی رسمی را بررسی کرده باشد.»— چابلین (@choblin29)، ۲۷ اکتبر، ساعت ۰۵:۵۴
حساب @choblin29 ساعت ۰۵:۵۴ به وقت هماهنگ جهانی، خلاصه‌ای از این انتشار را ارائه کرد. در این پست آمده است که صورت‌بندی رسمی شامل ۱٬۰۵۰ ماژول Lean است که هم Lean و هم هسته مستقل nanoda آن‌ها را بررسی می‌کنند؛ همچنین هنوز مشخص نیست کسی کل صورت‌بندی را بررسی کرده باشد. در پیوست E مقاله نیز آمده است که هر ۱٬۰۵۰ ماژول Lean با هم ساخته شده‌اند، اثبات‌ها از سوی هسته Lean و nanoda پذیرفته شده‌اند و «تا زمان نگارش مقاله، کسی شناسایی نشده است که آن را بررسی کرده باشد».
کلود چگونه به این نتیجه رسید؟ به روایت آنتروپیک
در مقاله آمده است: «الگوریتم اصلی در ۱۶ اکتبر توسط یک مدل پژوهشی داخلی کلود، با تولید ۱۴ میلیون توکن خروجی و بدون دخالت انسان، کشف شد.» در ادامه می‌گوید: «پژوهشگران آنتروپیک همراه با کلود برای بهبود نحوه ارائه نتیجه همکاری کردند و این مقاله را تهیه کردند.»
در فایل README مخزن آمده است که صورت‌بندی رسمی در Lean 4 «توسط مدل‌های هوش مصنوعی نوشته شده است». بر اساس این توضیح، Lean اثبات‌ها را با سه اصل موضوع استاندارد خود بررسی می‌کند. با این حال، README هشدار می‌دهد که «هیچ ماشینی بررسی نمی‌کند که محتوای این فایل با آنچه مقاله می‌گوید مطابقت داشته باشد». فایل حاوی گزاره اصلی عمداً کوتاه نگه داشته شده است تا خوانندگان بتوانند آن را بررسی کنند.
README همچنین می‌گوید کلود اوپوس ۵٫۵، در سطح تلاش محاسباتی بالا، می‌تواند رد فرضیه را از روی توضیحی فشرده از ایده اصلی دوباره به دست آورد؛ البته فقط کران ضعیف‌تر را، نه کران دقیق‌تری را که در ابتدای صفحه آمده است. لِوِنت آلپوگه که در نمایه ایکس خود به آنتروپیک اشاره کرده است، بخش مربوط به منشأ کشف را در ۲۷ اکتبر در این شبکه منتشر کرد.
این دستاورد در عمل چه چیزی را تغییر نمی‌دهد؟
مقاله درباره کاربرد عملی نتیجه صریح است: «بنابراین، نتیجه ما چیزی درباره حل عملی فرمول‌ها نمی‌گوید.» بر اساس مقاله، برای فرمول‌های 3-SAT که به‌ازای هر متغیر پنج بند دارند، کران زمانی الگوریتم پیشنهادی تا زمانی که تعداد متغیرها از ۱۰ به توان ۱۰٬۰۰۰ بیشتر نشود، از زمان اجرای ۲n در جست‌وجوی فراگیر بهتر نیست.
مقاله اضافه می‌کند که حتی جست‌وجوی فراگیر برای n برابر با ۱۰۰ نیز از نظر عملی امکان‌پذیر نیست. همچنین این نتیجه «مستقیماً به مسئله P در برابر NP ارتباطی ندارد و هیچ الگوریتم عملی برای مسائل NP-کامل ارائه نمی‌کند».
ارتباط با گزارش‌های پیشین
ما در ۲۶ اکتبر گزارش دادیم که اوپن‌ای‌آی می‌گوید هوش مصنوعی این شرکت فرضیه زمان نمایی را رد کرده است. اوپن‌ای‌آی تاریخ کشف نتیجه خود را ۱۶ اکتبر و تاریخ صورت‌بندی رسمی آن در Lean را ۱۷ اکتبر اعلام کرده بود. مقاله آنتروپیک نیز تاریخ کشف خود را همان روز، یعنی ۱۶ اکتبر، ذکر می‌کند. در سپتامبر، درباره صورت‌بندی رسمی آخرین قضیه فرما توسط کلود در Lean گزارش دادیم و در ۶ اکتبر نیز نوشتیم که یک مدل داخلی اوپن‌ای‌آی ۷۲۲ مقاله ریاضی تولید کرده است.
در پرونده S-1 که آنتروپیک همین ماه ارائه کرده است نیز آمده بود که کلود بیش از ۹۰ درصد کدهای جدید آنتروپیک را نوشته است. برای آشنایی با شیوه درآمدزایی این شرکت، می‌توانید تحلیل مدل کسب‌وکار آنتروپیک را بخوانید.
برداشت ساختاری از ماجرا
از نظر ما، رقم ۱۴ میلیون توکن خروجی به مقیاس این ادعا اشاره دارد: مقاله کشف الگوریتم اصلی را به اجرای یک مدل نسبت می‌دهد که میزان خروجی آن با توکن اندازه‌گیری شده است و پژوهشگران آنتروپیک در مرحله نگارش و ارائه نتیجه وارد کار شده‌اند.
به برداشت ما، README آنتروپیک محدودیت مهمی را از ابتدا روشن می‌کند: Lean درستی اثبات‌های رسمی را بررسی می‌کند، اما تطابق گزاره رسمی با محتوای مقاله همچنان بر عهده خوانندگان انسانی است. به همین دلیل، فایل حاوی گزاره اصلی کوتاه نگه داشته شده است.
از نظر ما، این محدودیت عملی برای مخاطبان کسب‌وکار نیز اهمیت دارد: مقاله می‌گوید برتری الگوریتم نسبت به جست‌وجوی فراگیر فقط در مورد فرمول‌هایی ظاهر می‌شود که بسیار بزرگ‌تر از نمونه‌های مورد استفاده در عمل هستند.
کلود (آنتروپیک)، A 2o(n) Time Algorithm for 3-SAT، مقاله مورخ ۲۶ اکتبر ۲۰۲۶
«الگوریتم اصلی در ۱۶ اکتبر توسط یک مدل پژوهشی داخلی کلود، با تولید ۱۴ میلیون توکن خروجی و بدون دخالت انسان، کشف شد.»
سه پیامد
برای پژوهشگران: مقاله آنتروپیک و فایل‌های Lean تحت مجوز Apache 2.0 به‌صورت عمومی منتشر شده‌اند. فایل README فرمان‌های لازم برای بازسازی و بررسی اثبات‌ها را ارائه می‌کند و می‌گوید این فرایند روی ۲۴ پردازنده مجازی حدود هشت دقیقه طول کشیده است.
برای نظریه پیچیدگی: مقاله به بیش از ۸۰۰ پژوهش اشاره می‌کند که دست‌کم یک نتیجه را فقط تحت فرضیه ETH یا فرضیه‌ای که آن را نتیجه می‌دهد اثبات کرده‌اند. همچنین می‌گوید قضیه ارائه‌شده، الگوریتم‌های سریع‌تری برای مسائلی مانند مجموعه مستقل، کلیک و پوشش رأس به دست می‌دهد.
برای رقابت آزمایشگاه‌های هوش مصنوعی: اوپن‌ای‌آی و آنتروپیک هر دو می‌گویند یک مدل داخلی آن‌ها در ۱۶ اکتبر به این نتیجه رسیده است. مقاله آنتروپیک این دو نتیجه را مستقل و هم‌زمان توصیف می‌کند.
ماجرا از نگاه چارچوب بیزنس انجینیر
این گزارش با چارچوب بیزنس انجینیر با عنوان دکترین فاصله میان توان فناوری و کاربرد محصول ارتباط پیدا می‌کند.
این چارچوب با این گزاره آغاز می‌شود: «در هر چرخه محصول، باید دو منحنی را دنبال کرد. منحنی نخست نشان می‌دهد فناوری زیربنایی چه کارهایی می‌تواند انجام دهد. منحنی دوم نشان می‌دهد کاربران در عمل چه کارهایی می‌توانند با آن انجام دهند.»
از نظر ما، این دستاورد در انتهای دورترین بخش این فاصله قرار می‌گیرد: طبق مقاله آنتروپیک، الگوریتم فقط برای فرمول‌هایی بسیار بزرگ‌تر از نمونه‌های مورد استفاده در عمل، نسبت به جست‌وجوی فراگیر سریع‌تر است. این چارچوب در ژوئن ۲۰۲۶ منتشر شده و به این نتیجه خاص نمی‌پردازد.
چه چیزهایی هنوز اثبات یا تأیید نشده‌اند؟
در مقاله یا فایل README نامی از یک نشریه داوری‌شده نیامده است؛ README می‌گوید پیوندی به Hexagon قرار است بعداً منتشر شود. اثبات‌های Lean گزاره‌های رسمی را بررسی می‌کنند، اما خود README تصریح می‌کند که هیچ ماشینی مطابقت این گزاره‌ها با متن مقاله را بررسی نمی‌کند. مقاله از «یک مدل پژوهشی داخلی کلود» نام می‌برد و نسخه دقیق مدل مورد استفاده برای این کشف را مشخص نمی‌کند. اوپن‌ای‌آی گفته است گروه‌های بیرونی ادعای این شرکت را بررسی خواهند کرد؛ اما در مقاله و README آنتروپیک، اشاره‌ای به بررسی بیرونی نتیجه این شرکت نشده است.
جمع‌بندی
مقاله آنتروپیک می‌گوید یک مدل داخلی کلود در ۱۶ اکتبر، با تولید ۱۴ میلیون توکن خروجی و بدون دخالت انسان، فرضیه زمان نمایی را رد کرده است؛ این همان تاریخی است که اوپن‌ای‌آی برای نتیجه مشابه خود اعلام کرده است. هر دو آزمایشگاه ادعای خود را با صورت‌بندی رسمی در Lean همراه کرده‌اند، اما مقاله آنتروپیک تأکید دارد که این نتیجه کاربرد عملی برای حل فرمول‌ها ندارد.
یادداشت درباره منابع: این گزارش بر مقاله آنتروپیک، شامل صفحه عنوان، چکیده و مقدمه تا بخش مربوط به منشأ کشف، فایل README مخزن ریاضیات صوری این شرکت در گیت‌هاب، پستی از لِوِنت آلپوگه در ایکس، اعلامیه اوپن‌ای‌آی در ۲۶ اکتبر ۲۰۲۶ و گزارش‌های پیشین ما استوار است. این منابع در ۲۷ اکتبر ۲۰۲۶ بررسی شده‌اند. ما خودمان اثبات‌ها را بررسی یا اجرا نکرده‌ایم و با آنتروپیک یا اوپن‌ای‌آی تماس نگرفته‌ایم.
منابع: مخزن ریاضیات صوری آنتروپیک، پوشه eth، شامل README و فایل‌های Lean، ۲۷ اکتبر ۲۰۲۶؛ کلود (آنتروپیک)، «A 2o(n) Time Algorithm for 3-SAT»، مقاله مورخ ۲۶ اکتبر ۲۰۲۶؛ لِوِنت آلپوگه در ایکس، ۲۷ اکتبر ۲۰۲۶؛ اعلامیه اوپن‌ای‌آی، ۲۶ اکتبر ۲۰۲۶.