زبان برنامه‌نویسی جدید بوترین برای عصر هوش مصنوعی

ویتالیک بوترین، بنیان‌گذار اتریوم، ایده ساخت یک زبان برنامه‌نویسی جدید را معرفی کرده است. این زبان طوری طراحی شده که بررسی و اعتبارسنجی خروجی‌های هوش مصنوعی را ساده‌تر کند و بتواند به‌طور مستقیم به ابزارهای اثبات رسمی مانند Lean یا HOL کامپایل شود.

بوترین معتقد است که با گسترش استفاده از هوش مصنوعی در توسعه نرم‌افزار، این مدل‌ها می‌توانند اثبات‌های ریاضی و فنی بسیار پیچیده‌ای را در مدت کوتاهی تولید کنند، اما بررسی و تأیید آن‌ها برای انسان همچنان دشوار باقی می‌ماند. به همین دلیل پیشنهاد کرده است که بخش‌هایی از خروجی که انسان باید مطالعه کند، از جزئیات فنی اثبات‌ها جدا شود.

هدف؛ خواناتر شدن خروجی‌های هوش مصنوعی

Lean یکی از ابزارهای «اثبات رسمی» است که پژوهشگران و مهندسان از آن برای نوشتن و تأیید ریاضی کدها استفاده می‌کنند. محققان اتریوم نیز سال‌هاست از این ابزار برای بررسی صحت کدهای رمزنگاری و سازوکار اجماع شبکه بهره می‌برند.

بوترین در توضیح ایده خود می‌گوید مراحل داخلی یک اثبات تنها باید از نظر ریاضی صحیح باشند و نیازی نیست انسان همه آن‌ها را بخواند. در مقابل، تعریف مفاهیم، مشخصات فنی و قضایا باید به زبانی ساده و قابل فهم نوشته شوند تا توسعه‌دهندگان بتوانند به‌راحتی تشخیص دهند یک نرم‌افزار دقیقاً چه تضمین‌هایی ارائه می‌دهد.

به گفته بوترین، مدل‌های زبانی بزرگ اکنون می‌توانند اثبات‌های قابل استفاده برای Lean تولید کنند. او از مدل‌هایی مانند Claude، DeepSeek 4 Pro و Leanstral به‌عنوان نمونه‌هایی یاد کرده که در این زمینه عملکرد مناسبی دارند.

از نگاه او، ایجاد یک زبان استاندارد برای توصیف مشخصات نرم‌افزار می‌تواند فرآیند بررسی ادعاهای هوش مصنوعی را بسیار ساده‌تر کند. در این صورت، توسعه‌دهندگان به‌جای مطالعه هزاران خط اثبات ریاضی، تنها مشخصات قابل فهم پروژه را بررسی می‌کنند و ابزارهای اثبات رسمی صحت آن را تضمین خواهند کرد.

امنیت بیشتر برای اکوسیستم اتریوم

این پیشنهاد همزمان با تلاش پژوهشگران اتریوم برای توسعه نسخه‌ای از ماشین مجازی اتریوم (EVM) با قابلیت اثبات رسمی و مبتنی بر دانش صفر (Zero-Knowledge) مطرح شده است.

بوترین معتقد است با افزایش حملات سایبری مبتنی بر هوش مصنوعی، استفاده از کدهای دارای اثبات رسمی می‌تواند به یکی از مهم‌ترین ابزارهای افزایش امنیت نرم‌افزارهای بلاکچینی تبدیل شود. به همین دلیل، ساده‌تر شدن فرآیند بررسی این کدها اهمیت زیادی خواهد داشت.

با این حال، او تأکید کرده این ایده هنوز در مرحله مفهومی قرار دارد و هیچ نمونه اولیه‌ای از این زبان برنامه‌نویسی منتشر نشده است. همچنین هنوز مشخص نیست جامعه توسعه‌دهندگان روی یک استاندارد مشترک به توافق می‌رسند یا هر گروه مسیر مستقلی را دنبال خواهد کرد.

منابع:

• beincrypto