OpenAI می‌گوید یکی از مدل‌های داخلی‌اش برهانی پیدا کرده که فرضیهٔ زمان نمایی (ETH) را رد می‌کند؛ فرضیه‌ای دربارهٔ محدودیت سرعت حل بعضی مسائل محاسباتی. شرکت می‌گوید مدل برهان را ۱۶ اکتبر ۲۰۲۶ پیدا کرد و روز بعد استدلال آن در Lean، سامانه‌ای که گام‌های یک برهان را با قواعد ریاضی بررسی می‌کند، بازنویسی و به‌صورت ماشینی وارسی شد. OpenAI این نتیجه را ۲۶ اکتبر اعلام کرد.
ETH به مسئلهٔ 3-SAT مربوط است: آیا می‌توان برای مجموعه‌ای از شرط‌های منطقی، به هر متغیر یکی از دو حالت را داد تا همهٔ شرط‌ها برقرار شوند؟ هرچه متغیرها بیشتر شوند، تعداد حالت‌های ممکن می‌تواند به‌شدت افزایش یابد. فرضیه می‌گفت هیچ الگوریتمی نمی‌تواند این مسئله را در همهٔ موارد با زمانی کمتر از رشد نمایی حل کند. رد آن به معنای حل فوری مسئله‌های بزرگ نیست؛ الگوریتم اعلام‌شده زمان را به شکلی زیرنمایی کاهش می‌دهد، اما ممکن است برای مسائل بزرگ همچنان بسیار طولانی باشد.
برهان چه چیزی را تغییر می‌دهد؟
به گفتهٔ OpenAI، روش جدید فقط وجود یک پاسخ را بررسی نمی‌کند؛ تعداد دقیق پاسخ‌های معتبر را هم می‌شمارد. این مسئله با نام #SAT شناخته می‌شود. اگر شمار پاسخ‌ها صفر باشد، مسئله راه‌حلی ندارد؛ اگر بیشتر از صفر باشد، دست‌کم یک پاسخ وجود دارد. مقالهٔ ۶۷صفحه‌ای شرکت از تقسیم مسئله به بخش‌های کوچک‌تر و رابطه‌های ریاضی برای محاسبهٔ تعداد پاسخ‌ها استفاده می‌کند. الگوریتم قطعی است و به انتخاب تصادفی متکی نیست.
به گفتهٔ رایان ویلیامز، یکی از داوران، زمان اجرای الگوریتم حدود ۲ به توانِ n تقسیم بر لگاریتم n به توانِ اندکی بیشتر از یک‌دوم است؛ n شمار متغیرهاست. این نتیجه برای نوع مشخصی از مسئله‌های SAT با تعداد ثابتی متغیر در هر شرط مطرح شده است. بنابراین، نمی‌توان آن را به همهٔ مسئله‌های دشوار یا همهٔ کاربردهای روزمره تعمیم داد. تبدیل یک مسئله به مسئله‌ای دیگر ممکن است اندازهٔ آن را آن‌قدر بزرگ کند که این بهبود از بین برود.
نتیجه هنوز در دست بررسی است
اگر برهان تأیید شود، صدها نتیجهٔ پژوهشی که از ETH برای تعیین حد سرعت الگوریتم‌ها استفاده کرده‌اند نیازمند بازبینی می‌شوند. این به معنی باطل‌شدن خودکار مقاله‌های پیشین نیست؛ نتیجه‌های شرطی آن‌ها از نظر منطقی باقی می‌مانند، اما ممکن است فرضی که بر آن تکیه کرده‌اند درست نباشد. مقالهٔ OpenAI همچنین می‌گوید برهان، نسخهٔ قوی‌تر ETH یعنی SETH را هم رد می‌کند.
ایمپالیاجو و پاتوری، دو پژوهشگری که در طرح ETH نقش داشتند، همراه ویلیامز نتیجه را بررسی می‌کنند. آن‌ها گفته‌اند مشارکتشان تأیید درستی ادعا نیست و بررسی مستقل لازم است. Lean می‌تواند خطاهای گام‌های صوری را پیدا کند، اما متخصصان باید بررسی کنند که تعریف‌های واردشده به سامانه واقعاً همان مسئله و ادعای مورد بحث را بیان می‌کنند. OpenAI در ۷ اکتبر نیز سه مقالهٔ تولیدشده با مدل‌هایش را به‌دلیل خطای علامت پس گرفت و ۱۴ مقاله را اصلاح کرد.
چرا مهم است
برای پژوهشگران علوم کامپیوتر، تأیید این برهان می‌تواند فرض‌هایی را که صدها مقاله برای سنجش دشواری الگوریتم‌ها به کار برده‌اند زیر سؤال ببرد. اما هنوز معلوم نیست بررسی مستقل ادعا را تأیید کند؛ و حتی در صورت تأیید، این نتیجه به‌تنهایی به معنی سریع‌ترشدن رایانه‌های معمولی یا شکسته‌شدن رمزنگاری نیست.
