آیا میتوان به کدهای نوشته شده توسط هوش مصنوعی اعتماد کرد؟ این پرسش بزرگی است که این پروژه جدید سعی دارد با «تأیید رسمی» (Formal Verification) به آن پاسخ دهد.
در این روش، به جای بررسی هزاران خط کد تولید شده توسط هوش مصنوعی، تنها با تکیه بر ۹۳ خط کدِ مشخصات فنی (Spec) و استفاده از زبان Lean 4، صحت عملکرد سیستمهای هندسی (CSG) تضمین میشود. هوش مصنوعی ۶۰ هزار خط اثبات ریاضی تولید کرده که سیستم به صورت خودکار آنها را بررسی میکند تا از دقت کامل کدها اطمینان حاصل شود. این یک گام مهم برای استفاده از هوش مصنوعی در پروژههای حساس و دقیق است که نیاز به تضمینهای ریاضی دارند.
تجربه کار با این متد، مرز جدیدی در تقابل میان هوش مصنوعی و امنیت نرمافزار ایجاد کرده است.
منبع: Hacker News AI
