مقاله‌ای که 5 نوامبر در arXiv منتشر شد، بررسی می‌کند که «تأییدشده» بودن کد تولیدشده با مدل‌های زبانی بزرگ چه معنایی دارد. نویسندگان سه معیار را از هم تفکیک می‌کنند: آیا راستی‌آزما کد را می‌پذیرد، آیا اثبات به یک مشخصات متصل است و آیا آن مشخصات بازتاب‌دهندهٔ نیاز اولیه است.
نویسندگان در یکی از آزمون‌ها می‌گویند راستی‌آزما 99.1% از کدها را در HumanEval پذیرفت، اما فقط 1.9% نمونه‌ها گواهی‌ای داشتند که به یک گزاره یا تابع تعریف‌شده در مشخصات متصل باشد. در یک خط لولهٔ جداگانهٔ Rust که برای اطمینان از این پیوند طراحی شده بود، 11.48% از نمونه‌های MBPP-Rust که از نظر ساختاری راستی‌آزمایی شده بودند و 14.82% از نمونه‌های یک بخش از VeriContest همچنان در آزمون‌های پنهان رد شدند.
چرا مهم است
برای تیم‌هایی که از بررسی اثبات‌ها برای ارزیابی کدهای تولیدشده استفاده می‌کنند، نتایج نشان می‌دهد که پذیرش کد از سوی راستی‌آزما به‌تنهایی لزوماً نه پیوند معنادار کد با نیازمندی‌ها را ثابت می‌کند و نه درستی آن را در آزمون‌های پنهان.
