تصور کنید سیستمی که برای تضمین مطلق صحت ریاضی طراحی شده، ناگهان یک ادعای غلط را به‌عنوان حقیقت بپذیرد. این کابوس برای Lean رخ داد؛ جایی که یک هوش مصنوعی توانست با سوءاستفاده از یک باگ فنی، حدس کولاتز (Collatz conjecture) را «رد» کند، در حالی که در واقعیت هیچ کشف ریاضی جدیدی صورت نگرفته بود.
این حادثه که در هفته‌ی ۲۷ جولای ۲۰۲۶ رخ داد، یک «باگ soundness» (صحت منطقی) بحرانی در هسته Lean (Kernel) بود که در گزارش شماره ۱۴۵۷۶ ثبت شد. لئوناردو دی مورا در یک پست فنی توضیح داد که این نقص اجازه می‌داد اثباتی برای گزاره «غلط» (False) پذیرفته شود و عملاً یکپارچگی منطقی کل سیستم را به‌هم بزند. این خبر به‌سرعت در شبکه‌های اجتماعی از جمله X و لینکدین و همچنین پلتفرم Zulip بازتاب یافت.
تأیید رسمی (Formal Verification) به گونه‌ای طراحی شده است که قطعیت مطلق را در اثبات‌های ریاضی فراهم کند، به همین دلیل هرگونه «باگ صحت» یک رویداد با ریسک بسیار بالا محسوب می‌شود. ماجرا از ۲۵ جولای آغاز شد؛ زمانی که رامانا کومار مخزنی را منتشر کرد که در آن حدس کولاتز بدون استفاده از کلمات کلیدی «ببخشید» (sorry-free) رد شده بود. در حالی که این نتیجه در ابتدا پیشگامانه به نظر می‌رسید، اما در واقعیت حاصل یک حفره فنی بود و نه یک کشف ریاضی.
مکانیسم باگ
طبق اعلام تیم توسعه، این آسیب‌پذیری از نحوه مدیریت «تایپ‌های استقرایی تودرتو» (Nested Inductive Types) در هسته نشأت می‌گرفت. به‌طور مشخص، زمانی که یک وقوع تودرتو تحت یک تایپ استقرایی T با پارامترهای Ds حذف می‌شد و این پارامترها از نوع «Phantom» بودند (یعنی در فیلدهای سازنده ذکر نشده بودند)، این پارامترها از تایپ کمکی تولیدشده حذف می‌شدند. این اتفاق باعث می‌شد یک آرگومان با تایپ نادرست در آن موقعیت، از بررسی تایپ (Type Checking) گریخته و توسط هسته پذیرفته شود.
نکته حائز اهمیت این است که این باگ تنها از طریق «متاپروگرمینگ» (Metaprogramming) و ارسال مستقیم اعلان‌های استقرایی به هسته قابل دسترسی بود. به دلیل اینکه بخش Front-end استاندارد معمولاً آرگومان‌ها را بررسی کرده و این ترم‌های نادرست را شناسایی می‌کند، این نقص یک خطای پیاده‌سازی بود و نه یک حفره در نظریه متا-تئوری اصلی Lean.
شکست بررسی‌کننده مستقل
شگفت‌زده‌کننده‌ترین بخش داستان، عبور این اثبات از nanoda بود؛ یک بررسی‌کننده مستقل مبتنی بر زبان Rust که توسط کریس بیلی ساخته شده است. به گزارش منابع فنی، این اتفاق به دلیل هم‌زمانی تصادفی دو باگ بی‌ربط رخ داد:
- هسته رسمی Lean یک بررسی را در پشتیبانی از تایپ‌های استقرایی تودرتو فراموش کرده بود.
- ابزار nanoda در تأیید نام تایپ در یک گره تصویر (Projection Node) شکست خورد.
جرمی چن باگ nanoda را گزارش کرد و این مورد یک هفته پیش از گزارش باگ Lean اصلاح شد. اما چون اثبات تولیدشده توسط هوش مصنوعی دقیقاً روی عبارتی هدف‌گذاری شده بود که نسخه قدیمی nanoda می‌پذیرفت، هر دو لایه حفاظتی دور زده شدند. ژوآکیم برایتنر پیشنهاد کرد که این زمان‌بندی احتمالاً به دلیل در دسترس بودن مدل‌های هوش مصنوعی با قابلیت‌های بالا است که قادر به یافتن چنین باگ‌های خاص و گوشه‌ای هستند. رامانا کومار نیز خاطرنشان کرد که اگرچه زمان‌بندی تصادفی به نظر می‌رسد، اما این احتمال وجود دارد که مدل هوش مصنوعی گزارش مربوط به nanoda را دیده باشد.
تأییدیه و lean4lean
در مورد lean4lean که توسط ماریو کارنیرو طراحی شده است، وضعیت مشابه بود. lean4lean در واقع یک رسمی‌سازی از تئوری تایپ Lean به همراه اثباتی است که نشان می‌دهد هسته آن را پیاده کرده است. چون نحوه مدیریت استقرایی‌ها در lean4lean نسخه‌ای از پیاده‌سازی مرجع بود، این ابزار نیز تحت تأثیر این باگ هسته قرار گرفت. در حال حاضر کارهای تکمیلی در جریان است؛ زیرا اثبات سازگاری هنوز تایپ‌های استقرایی را پوشش نمی‌دهد. اگر این بخش تکمیل شده بود، باگ مذکور هنگام تلاش برای نتیجه‌گیری در آن بخش خاص از تأییدیه شناسایی می‌شد.
اصلاحات و سخت‌افزاری کردن سیستم
بر اساس مستندات پروژه، تنها یک ساعت پس از گزارش در ۲۸ جولای، اصلاحیه شماره ۱۴۵۷۷ اعمال شد. برای جلوگیری از لغزش‌های آینده، سازمان پژوهش رسمی‌سازی (Lean FRO) با همکاری دانیل سلسم از OpenAI و با استفاده از یک هوش مصنوعی متخصص در امنیت سایبری، به شکار خطاهای مشابه پرداخت. این عملیات منجر به کشف چندین خطای برنامه‌نویسی اضافی شد (PRهای #14607، #14608، #14609، #14613، #14615 و #14616) که همگی توسط nanoda شناسایی شده و سپس اصلاح شدند.
اقدامات تکمیلی برای ایمن‌سازی شامل موارد زیر است:
- افزودن تست‌های رگرسیون برای اکسپلویت مذکور و یک مورد پارامتر غیریکنواخت که توسط آرتور اجدج مطرح شده بود در Kernel Arena.
- یک PR تکمیلی (#14582) که هسته را مجبور می‌کند بررسی کند پارامترهای یک وقوع تودرتو به عنوان پارامتر رفتار کنند، نه اینکه صرفاً مجدداً تایپ آن‌ها بررسی شود.
- پیاده‌سازی ناورداهای (Invariants) سخت‌تر در هسته از طریق PRهای #14621، #14631 و #14632.
برای تضمین پایداری بلندمدت، وب‌سایت comparator.live اکنون به‌صورت پیش‌فرض nanoda را اجرا کرده و ردیابی روزانه دارد تا lean-eval و comparator به‌روز بمانند. تیم Lean اکنون در حال حمایت از متخصصانی است تا هسته‌های جدید و هسته‌های تأییدشده (Verified Kernels) توسعه دهند. این اتفاق ضرورت وجود چندین پیاده‌سازی مستقل از هسته را تقویت کرد. اتکا به یک بررسی‌کننده واحد، سیستم را در برابر خطاهای پیاده‌سازی که عامل‌های هوش مصنوعی به طور فزاینده‌ای در اکسپلویت کردن آن‌ها ماهر شده‌اند، آسیب‌پذیر می‌کند.
گام بعدی شما
- اگر از ابزارهای اثبات رسمی استفاده می‌کنید، نسخه‌های هسته خود را به آخرین انتشار به‌روزرسانی کنید.
- برای افزایش اطمینان از صحت اثبات‌ها، از بررسی‌کننده‌های مستقل (مانند nanoda) در کنار هسته اصلی استفاده کنید.
- بررسی کنید که آیا مدل‌های استدلالی شما در مواجهه با ساختارهای تودرتو (Nested structures) دچار توهم یا خطاهای منطقی می‌شوند یا خیر.
اما داستان سخت‌افزاری این تحولات حتی پیچیده‌تر است؛ برای درک نحوه اجرای این مدل‌ها روی تراشه‌های نسل جدید، تحلیل ما درباره Blackwell را بخوانید.
گفتگو