پروتکل NEAR در بیانیه‌ای اعلام کرد که تحقیقاتش به دنبال کاهش کار تخصصی و هزینه‌های محاسباتی مربوط به اثبات پیروی نرم‌افزار از قوانین تعریف‌شده است. این پروتکل قصد دارد از «تأیید رسمی به کمک هوش مصنوعی» (AI-assisted formal verification) برای پروتکل و قراردادهای هوشمند اصلی خود و همچنین ابزارهای توسعه‌دهندگان اکوسیستم استفاده کند.
این برنامه پس از آن اعلام شد که هوش مصنوعی NEAR موفق شد ۶۷۲ مسئله ریاضی از بنچمارک PutnamBench را با هزینه مدل ۱۱۱.۸۵ دلار در زمان ثبت، حل کند. NEAR این دستاورد را گامی در جهت تولید خودکار اثبات‌های ریاضی توصیف کرده و هدف نهایی را تأیید نرم‌افزارهای در حال اجرا می‌داند.
مراحل و چالش‌های پیش رو
به گفته NEAR، پیاده‌سازی این تحقیق روی نرم‌افزارهای واقعی شامل سه مرحله است: ابتدا توسعه‌دهندگان باید برنامه را به صورت ریاضی مدل‌سازی کنند، سپس ویژگی‌هایی که باید برآورده شوند را تعریف کرده و در نهایت، اثبات‌هایی برای نشان دادن صحت آن ویژگی‌ها ایجاد کنند.
نتایج اخیر بنچمارک NEAR پیشرفت در مرحله سوم را نشان می‌دهد. با این حال، این تیم تأکید می‌کند که کار در سطح تولید همچنان نیازمند مدل‌های دقیق از رفتار نرم‌افزار و ارتباط شفاف بین اثبات‌ها و پیاده‌سازی نهایی است که کاربران به آن تکیه می‌کنند.
برای مثال، یک اثبات ممکن است تضمین کند که موجودی حساب‌ها در حین انتقال حفظ می‌شود، اما برای اطمینان از اینکه فقط حساب‌های مجاز می‌توانند انتقال را آغاز کنند، به یک اثبات جداگانه نیاز است.
ایلیا پولوسوکین (Illia Polosukhin)، هم‌بنیان‌گذار NEAR، این تحقیق را به خطرات ناشی از نرم‌افزارهای تولیدشده توسط هوش مصنوعی و ابزارهایی که به مهاجمان در شناسایی ضعف‌ها کمک می‌کنند، مرتبط دانسته است.
آینده هوش مصنوعی و کدهای تولیدشده توسط آن هیجان‌انگیز است - اما تنها زمانی که به تضمین‌های قابل تأیید و ریاضیاتی از رفتار آن دست یابیم.
Illia Polosukhin
NEAR تأکید می‌کند که تأیید رسمی باید مکمل روش‌های امنیتی دیگر مانند تست، بازبینی کد و شیوه‌های امنیت عملیاتی باشد.
جزئیات هزینه و عملکرد
نتیجه ۱۱۱.۸۵ دلاری مربوط به حل ۶۷۲ مسئله از بنچمارک PutnamBench است که بر اساس رقابت ریاضیات دانشگاهی پاتنم طراحی شده است. هزینه متوسط گزارش‌شده برای هر مسئله حدود ۰.۱۷ دلار بوده است. این هزینه شامل کل هزینه توسعه سیستم نمی‌شود و برآوردی از قیمت تأیید یک قرارداد هوشمند در محیط واقعی نیست.
تیم پروژه اشاره کرده که اجرای مجدد همین فرآیند با قیمت‌های جدیدتر سرویس DeepSeek حدود ۳۳۱ دلار هزینه خواهد داشت. همچنین طولانی‌ترین اجرای این فرآیند بیش از سه روز به طول انجامیده است.
تأیید رسمی در اکوسیستم بلاکچین
تأیید رسمی پیش از این نیز در اکوسیستم NEAR کاربرد داشته است. برای مثال، شرکت Certora در ارزیابی خود از پروتکل وام‌دهی Templar، از بازبینی دستی و تأیید رسمی برای قراردادهای آن استفاده کرده بود.
سایر تیم‌های بلاکچینی نیز به دنبال تأیید به کمک هوش مصنوعی هستند. در ماه می، Aptos Labs پشتیبانی از این فناوری را برای قراردادهای Move اعلام کرد. ویتالیک بوترین، هم‌بنیان‌گذار اتریوم، نیز درباره ترکیب ابزارهای هوش مصنوعی و اثبات‌های ماشین‌خوان برای افزایش امنیت در بخش‌های مختلف نقشه راه اتریوم صحبت کرده است.
این تلاش‌ها در کنار سایر تحقیقات امنیتی NEAR، مانند کار بر روی امضاهای مقاوم در برابر کوانتوم با استفاده از استاندارد ML-DSA، نشان‌دهنده تمرکز جدی این پروتکل بر افزایش امنیت در بلندمدت است.
