پژوهشگران سه معنای متفاوت برای «کد تأییدشده» با مدل‌های زبانی تفکیک کردند

پیش‌چاپی در arXiv با بررسی دو خط لولهٔ تولید کدِ مبتنی بر مدل زبانی استدلال می‌کند که ارزیابی «کد تأییدشده» نباید به یک عدد خلاصه شود. نویسندگان سه سطح را از هم جدا می‌کنند: پذیرش کد از سوی ابزار تأیید (A)، پیوند صوری تعهد اثبات با مشخصات (B)، و این‌که خود مشخصات واقعاً نیاز غیررسمی را بیان کند (C).

در آزمایش نخست، بازتولید خط لولهٔ Li@Opus با Claude Opus 4.7 و Dafny روی سه معیار Python، نرخ پذیرش verifier در HumanEval به ۹۹٫۱ درصد رسید؛ اما فقط ۱٫۹ درصد نمونه‌ها گواهی‌ای داشتند که به محمول یا تابع تعریف‌شده در مشخصات پیوند بخورد. این نتیجه، از دید نویسندگان، نشان می‌دهد پذیرش verifier به‌تنهایی تضمین نمی‌کند که اثبات واقعاً به مشخصات متصل باشد.

آزمایش دوم با خط لولهٔ داخلی VCG روی دو معیار Rust انجام شد. در این روش، هر مؤلفه گواهی Dafny دارد و شرط پیوند به مشخصات از ابتدا برقرار است؛ بااین‌حال، ۱۱٫۴۸ درصد نمونه‌های ساختاراً تأییدشده در MBPP-Rust و ۱۴٫۸۲ درصد در بخش LC از VeriContest در آزمون‌های پنهان شکست خوردند. بنابراین، حتی پیوند صوری اثبات با مشخصات تضمین نمی‌کند که مشخصات نیاز واقعی را درست بازتاب دهد.

نرخ End2End گزارش‌شدهٔ VCG در بخش LC از VeriContest برابر ۷٫۷۹ درصد، یا ۵۳۵ مورد از ۶۸۷۰، بود. مقاله نرخ‌های بیرونی ۵٫۵۱ درصد برای GPT-5.5 و ۱٫۸۸ درصد برای اجرای تک‌مرحله‌ای Opus 4.7 را نیز ذکر می‌کند، اما تأکید دارد تفاوت در بودجهٔ وظایف، فرایند تعمیر و محیط آزمون اجازهٔ مقایسهٔ عملکرد هم‌شرایط را نمی‌دهد. این مقاله نسخهٔ پیش‌چاپ است.