ایایها دیگه ریاضیدان نمیشن، اثباتگر میشن؛ اثبات صوری با LLM
نویسنده: آرش لطیفی
آنتروپیک با Claude ویژگیهای امنیتی ۱۲۳ کتابخانه متنباز را در سطح اسمبلی RISC-V اثبات کرد؛ اثبات صوری چطور از یک تخصص ۲۰ ساله به یک مرحله CI تبدیل میشود.
TL;DR — آنتروپیک با Claude برای بیش از ۱۰۰ کتابخانه متنباز واقعی، در سطح کد اسمبلی (RISC-V) اثبات صوری ارائه کرد؛ LLMها دارند کاری را که قبلاً ۲۰ نفر-سال میخواست، خودکار میکنند.
اثبات صوری چرا تا حالا کسی انجامش نمیداد؟
بیشتر نرمافزارها پر از باگاند و تست فقط «بعضی ورودیها» را چک میکند. اثبات صوری (formal verification) برعکس است: کد را به یک مدل ریاضی تبدیل میکنید و ثابت میکنید کد همیشه قوانین امنیتی مشخصی را رعایت میکند — برای همه ورودیها. اگر اثبات شکست بخورد، خود شکست نشان میدهد باگ کجاست.
مشکل: هزینه. اثباتها معمولاً چند برابر خود کد طولانیترند. مثال معروف خودِ مقاله: پیادهسازی کرنل seL4 دو نفر-سال طول کشید، اما اثبات رسمیاش ۲۰ نفر-سال. برای همین اثبات صوری فقط در کدهای حیاتی مثل سیستم پروازی ایربس استفاده میشد.
آنتروپیک چه کاری کرد؟
با همکاری شرکت Theorem، از Claude برای اثبات ویژگیهای امنیتی روی ۱۲۳ کتابخانه متنباز واقعی استفاده کردند. نکتههای کلیدی از خود پژوهش:
- اثبات در سطح کد اسمبلی (RISC-V) است، نه فقط سورس بالا-سطح. به ادعای خودشان اولین تلاش بزرگ AI برای اثبات صوری کد پروداکشن در این سطح است.
- ویژگی اثباتشده: برنامهها برای هر ورودی کمتر از ۶۴ مگابایت و هر پاسخ مدلشدهی لینوکس، بدون خطای memory-safety و assertion خروج میدهند — با فرض باینری استاتیک تک-نخی روی RISC-V.
- در حین اثبات، Claude باگهایی پیدا کرد که با وجود تریلیونها اجرای تست سالها مخفی مانده بودند.
- زیرمجموعهای از اثباتها منتشر شده تا هرکس بتواند خودش verify کند.
در مقدمه مقاله هم اشاره شده که کرنل لینوکس — تستشدهترین نرمافزار دنیا — اخیراً بیش از ۱٬۰۰۰ آسیبپذیری داشتهاست؛ یعنی تست صرف کافی نیست.
| روش | چه چیزی تضمین میکند | هزینه سنتی | با LLM | | --- | --- | --- | --- | | تست (unit/E2E) | فقط ورودیهای تستشده | پایین | بدون تغییر | | Fuzzing | ورودیهای اتفاقی بیشتر | متوسط | بدون تغییر | | اثبات صوری | همه ورودیها، ریاضی | ۱۰ برابر کد (۲۰ نفر-سال برای seL4) | خودکار در مقیاس |
برای توسعهدهنده روزمره یعنی چه؟
شما هنوز قرار نیست برای سایت فروشگاهیتان Lean بنویسید. اما سه پیامد عملی نزدیک است:
- ثبت اثبات به CI. وقتی مدل میتواند اثبات تولید کند، میتواند در PR هم regenerate و چک کند. آیندهی احتمالی: «این PR تست دارد و اثبات امنیتیاش هم رد شد».
- وابستگیها قابل حسابرسی میشوند. اگر کتابخانههایی که
npm installمیکنید اثبات memory-safety داشته باشند، ریسک زنجیره تأمین (supply chain) واقعاً کاهش پیدا میکند — نه فقط روی کاغذ. - نقش مهندس عوض میشود. اثبات بهجای مهارت انحصاری، خروجی مدل + بازبینی انسانی میشود؛ مثل code review.
چکلیست آمادگی
- [ ] ماژولهای بحرانی پروژه (احراز هویت، پرداخت، رمزنگاری) را مشخص کنید
- [ ] پوشش تست این ماژولها را اول به ۱۰۰٪ خط برسانید
- [ ] ابزارهای تحلیل استاتیک (مثل type-checker سختگیرانه، linters) را در CI فعال کنید
- [ ] نسخه و lockfile وابستگیها را قفل کنید تا حسابرسی ممکن باشد
- [ ] مقاله آنتروپیک و اثباتهای منتشرشده را مطالعه کنید تا خروجی قابل قبول را بشناسید
سوالات پرتکرار
Q: یعنی دیگر باگ امنیتی نخواهیم داشت؟
نه. اثباتها تحت فرضهایی هستند (تک-نخی بودن، محدودیت حافظه، معماری RISC-V). خارج از آن فرضها تضمینی نیست. اثبات صوری یک لایه قویتر اضافه میکند، نه ضمانت مطلق.
Q: با از یادگیری رسمی (Lean، Coq) شروع کنم؟
اگر روی سیستمهای بحرانی کار میکنید بله، درک مفاهیم ارزشمند است. اما پیام اصلی مقاله این است که LLMها بار نوشتن اثبات را برداشتهاند؛ ارزش شما بیشتر در تعریف دقیق ویژگیهای امنیتی و بازبینی اثباتهاست.
Q: برای پروژه Next.js/وب من الان کاربرد دارد؟
بهصورت مستقیم نه — اثباتها در سطح اسمبلی و برای کتابخانههای سیستمی بود. کاربرد نزدیک شما تحلیل استاتیک قویتر و انتظار از ابزارهای AI آینده است که خروجی قابل verify میدهند.