ویتالیک بوترین زبان برنامهنویسی جدیدی برای عصر هوش مصنوعی پیشنهاد داد
۳۱ تیر ۱۴۰۵
ویتالیک بوترین (Vitalik Buterin)، همبنیانگذار اتریوم، از ایده توسعه یک زبان برنامهنویسی جدید رونمایی کرده است؛ زبانی که با هدف سادهتر کردن بررسی خروجیهای هوش مصنوعی طراحی میشود و میتواند مستقیماً به ابزارهای اثبات رسمی مانند Lean یا HOL کامپایل شود. به گزارش ، بوترین معتقد است با گسترش استفاده از مدلهای هوش مصنوعی
ویتالیک بوترین (Vitalik Buterin)، همبنیانگذار اتریوم، از ایده توسعه یک زبان برنامهنویسی جدید رونمایی کرده است؛ زبانی که با هدف سادهتر کردن بررسی خروجیهای هوش مصنوعی طراحی میشود و میتواند مستقیماً به ابزارهای اثبات رسمی مانند Lean یا HOL کامپایل شود.
بوترین معتقد است با گسترش استفاده از مدلهای هوش مصنوعی در توسعه نرمافزار، این ابزارها قادرند در مدت کوتاهی اثباتهای ریاضی و فنی بسیار پیچیدهای تولید کنند؛ اما درک و راستیآزمایی این خروجیها برای انسان همچنان دشوار است. به همین دلیل، او پیشنهاد کرده بخشهایی که انسان باید آنها را مطالعه و بررسی کند، از جزئیات فنی اثباتها جدا شود.
Lean یکی از ابزارهای «اثبات رسمی» است که پژوهشگران و مهندسان از آن برای نوشتن و تأیید ریاضی کدها استفاده میکنند. محققان اتریوم نیز سالهاست از این ابزار برای بررسی صحت کدهای رمزنگاری و سازوکار اجماع شبکه بهره میبرند.
بوترین در توضیح ایده خود میگوید مراحل داخلی یک اثبات تنها باید از نظر ریاضی صحیح باشند و نیازی نیست انسان همه آنها را بخواند. در مقابل، تعریف مفاهیم، مشخصات فنی و قضایا باید به زبانی ساده و قابل فهم نوشته شوند تا توسعهدهندگان بتوانند بهراحتی تشخیص دهند یک نرمافزار دقیقاً چه تضمینهایی ارائه میدهد.
به گفته بوترین، مدلهای زبانی بزرگ اکنون میتوانند اثباتهای قابل استفاده برای Lean تولید کنند. او از مدلهایی مانند Claude، DeepSeek 4 Pro و Leanstral بهعنوان نمونههایی یاد کرده که در این زمینه عملکرد مناسبی دارند.
از نگاه او، ایجاد یک زبان استاندارد برای توصیف مشخصات نرمافزار میتواند فرآیند بررسی ادعاهای هوش مصنوعی را بسیار سادهتر کند. در این صورت، توسعهدهندگان بهجای مطالعه هزاران خط اثبات ریاضی، تنها مشخصات قابل فهم پروژه را بررسی میکنند و ابزارهای اثبات رسمی صحت آن را تضمین خواهند کرد.
این پیشنهاد همزمان با تلاش پژوهشگران اتریوم برای توسعه نسخهای از ماشین مجازی اتریوم (EVM) با قابلیت اثبات رسمی و مبتنی بر دانش صفر (Zero-Knowledge) مطرح شده است.
بوترین معتقد است با افزایش حملات سایبری مبتنی بر هوش مصنوعی، استفاده از کدهای دارای اثبات رسمی میتواند به یکی از مهمترین ابزارهای افزایش امنیت نرمافزارهای بلاکچینی تبدیل شود. به همین دلیل، سادهتر شدن فرآیند بررسی این کدها اهمیت زیادی خواهد داشت.
با این حال، او تأکید کرده این ایده هنوز در مرحله مفهومی قرار دارد و هیچ نمونه اولیهای از این زبان برنامهنویسی منتشر نشده است. همچنین هنوز مشخص نیست جامعه توسعهدهندگان روی یک استاندارد مشترک به توافق میرسند یا هر گروه مسیر مستقلی را دنبال خواهد کرد.