ارزیابی نمادین مشخصه های تولید شده توسط LLMها برای زبان های آگاه از تایید

ظهور مدل های زبانی بزرگ (LLM) تحولی شگرف در حوزه تست تولید خودکار کد ایجاد کرده است. با این حال، تولید مشخصات صوری (Formal Specifications) دقیق برای زبان های آگاه از تایید (Verification-Aware Languages) همچنان چالشی دشوار باقی مانده است. این مقاله ضمن مروری بر سیر تکاملی از روش های تست سنتی به سمت متدولوژی های نوین ارزیابی نمادین (Symbolic Evaluation) – با تمرکز ویژه بر دستاوردهای لاهیری و همکاران - به بررسی شکاف های موجود در قابلیت اطمینان کدهای تولید شده توسط هوش مصنوعی می پردازد. یافته های ما نشان می دهد که محدودیت اصلی نه در ابزارهای تایید بلکه در ناتوانی مدل ها در استخراج مشخصات کامل (Complete Specifications) از ورودی های مبهم و غیر ساختاریافته است. در این راستا ما رویکردی نوآورانه مبتنی بر دخیل سازی مستندات تحلیل و طراحی نرم افزار (Document-Driven Specification Formalization) را پیشنهاد می دهیم که با استفاده از دانش زمینه ای موجود در مستندات مهندسی دقت و کامل بودن مشخصات صوری تولید شده توسط LLMها را به طرز چشمگیری ارتقا می دهد. این پژوهش مسیر جدیدی برای حرکت به سوی تولید نرم افزارهای پیچیده و بدون خطا (Correct-by-construction) با کمک هوش مصنوعی هموار می کند.

کلیدواژه ها:

هوش مصنوعی (LMS) ، تایید صوری (Formal Verification) ، زبان های آگاه از تایید ، رسمی سازی نیت کاربر (Intent Formalization) ، ارزیابی نمادین (Symbolic Evaluation) ، مستندات طراحی نرم افزار (Software Design Documentation)