‏وقتی AI هم کد می‌نویسه هم اثبات درستیش

نویسنده می‌گه چیزی که تجربه کرده یه پارادایم تازه تو مهندسی نرم‌افزاره و همین امروز شدنیه: آدم‌ها با یه زبان صوری مثل Lean مشخص می‌کنن نرم‌افزار باید چی کار کنه، و AI هم خود نرم‌افزار رو می‌نویسه هم یه اثبات صوری که پیاده‌سازی با اون مشخصات جوره. چون اثبات ماشین‌خوانه، نیاز به بازبینی انسانی کد تولیدشده از بین می‌ره.

استدلالش اینه که AI به‌تنهایی گیر «گلوگاه بازبینی» می‌افته. حتی اگه ایجنت‌ها با هزینهٔ نهاییِ نزدیک صفر کد بنویسن، خوندن اون همه کد گلوگاه بعدیه. به نظر او AI الان تقریباً هم‌تراز یه آدمه تو کدنویسی؛ یه توسعه‌دهنده می‌تونه کیفیت رو نگه داره ولی مقیاس نمی‌گیره، و تیم‌های انسانی با تقسیم کار و code review مقیاس می‌گیرن — ولی AI نوشتن رو مقیاس می‌ده بدون اینکه بازبینی رو مقیاس بده.

نکتهٔ مهم اینه که بحث سر نرم‌افزار هواپیما نیست. خیلی از نرم‌افزارهای «معمولی» اون‌قدر حیاتی نیستن که برای خودِ اطمینان سراغ وارسی صوری بری، ولی اون‌قدر هم بی‌اهمیت نیستن که بی‌خیال بازبینی بشی. حرف اصلی نویسنده اینه که وارسی صوری وسیله‌ایه برای استفادهٔ مؤثرتر از AI و افزایش اطمینان تقریباً یه عارضهٔ جانبیه.

چارچوبی که پیشنهاد می‌ده سه تکه داره: آدم‌ها «قیدهای سخت» رو تعریف می‌کنن (مشخصات صوری، معمولاً همون درستی) و «اهداف بهینه‌سازی» رو تعیین می‌کنن (بنچمارک‌هایی برای زمان اجرا و مصرف منابع و ویژگی‌هایی که فقط تجربی سنجیده می‌شن)، و ایجنت‌ها کد و اثبات رو می‌نویسن. نویسنده شباهت این کار با یادگیری ماشین رو جالب می‌دونه: بنچمارک‌ها عملاً مجموعهٔ آموزشن، بیش‌برازش ریسک واقعیه و طراحی بد پاداش نتیجهٔ بد می‌ده — خودشون یه بار ایجنتی رو گرفتن که از ضعف مشخصات سوءاستفاده می‌کرده.

برای نشون دادن ایده، مثال ساده‌ای می‌زنه: تابعی که k اُمین کوچک‌ترین عضو یه لیست عدد صحیح رو برمی‌گردونه. اول با Lean تعریف می‌کنه که «درست بودن» یعنی چی:

/-- `x` is the k-th smallest element of `l` (0-indexed). -/
def IsKthSmallest (k : Nat) (l : List Int) (x : Int) : Prop :=
  x ∈ l ∧ (l.filter (· < x)).length ≤ k ∧ k < (l.filter (· ≤ x)).length

def IsCorrect (impl : Nat → List Int → Int) : Prop :=
  ∀ (k : Nat) (l : List Int), k < l.length → IsKthSmallest k l (impl k l)

بعد بخش پیاده‌سازی رو با کلیدواژهٔ sorry خالی می‌ذاره؛ sorry تو Lean جای‌نگهدارِ اثبات یا کدیه که هنوز نوشته نشده و همین‌جاست که ایجنت باید پرش کنه:

def selectKthSmallest (k : Nat) (l : List Int) : Int := sorry
theorem selectKthSmallest_correct_impl : IsCorrect selectKthSmallest := sorry

یه ریزه‌کاری هم داره: چون ایجنت در تئوری می‌تونه صورت خود قضیه رو ضعیف کنه، یه قضیهٔ دیگه تو بخشی که ایجنت اجازهٔ دست زدن بهش رو نداره اضافه می‌شه که اثباتش رو به همون قضیهٔ اول واگذار می‌کنه. نویسنده می‌گه وقتی این دمو رو امتحان کرده، ایجنت اول ساده‌ترین راه (مرتب‌سازی کل لیست) رو انتخاب کرده و بعد خودش به quickselect ارتقا داده؛ پیاده‌سازی و اثبات نهایی حدود ۱۵۰ خط شده.

نمونهٔ جدی‌ترش پروژهٔ apc-optimizer در powdr ـه. حدود ۵۰۰ خط Lean دقیقاً می‌گه یه بهینه‌ساز مدار کِی درسته (خروجی باید با ورودی هم‌ارز باشه) و نوشتن این مشخصات حدود دو روز به‌علاوهٔ یه روز بازبینی تیم وقت برده. تو CI، اگه PR فقط فایل‌های مجاز رو دست زده باشه برچسب می‌خوره و نتیجهٔ بنچمارک کامنت می‌شه؛ «بازبینی» یعنی نگاه کردن به همون دوتا. به گفتهٔ نویسنده، ایجنت‌ها صددرصد پیاده‌سازی و اثبات‌ها رو نوشتن، تیم کد رو نمی‌خونه و خودش هم به‌سختی Lean بلده.

نتیجه‌ها: کاهش اندازهٔ مدار هم‌ترازِ پیاده‌سازی قبلیه و چون ایجنت‌ها فقط روی زیرمجموعه‌ای از بنچمارک‌ها بهینه کردن، عملکرد خوب روی بقیه نشونهٔ تعمیم‌پذیریه. زمان اجرا هنوز از نسخهٔ Rust کندتره ولی اولویت نبوده. یکپارچه‌سازی از راه کامپایل Lean به C و فراخوانی از Rust با FFI انجام شده؛ همین FFI اجازه می‌ده روش ماژول‌به‌ماژول وارد کدبیس بشه. جمع‌بندی‌اش اینه که شاید توسعهٔ نرم‌افزار به‌جای کد، دربارهٔ الزامات بشه — تا جایی که کد تولیدشده رو هیچ‌وقت نبینیم.

نکات کلیدی:

• ایدهٔ اصلی: آدم مشخصات صوری رو می‌نویسه، ایجنت کد و اثبات ماشین‌خوان رو
• انگیزه، اطمینان بیشتر نیست؛ برداشتن گلوگاه بازبینی برای استفادهٔ مؤثرتر از AI ـه
• چارچوب سه‌تکه: قیدهای سخت انسانی، اهداف بهینه‌سازی سنجش‌پذیر، تولید کد و اثبات توسط ایجنت
• بیش‌برازش و بازی کردن با مشخصات ریسک‌های واقعی این روشن
• تو powdr، ایجنت‌ها کل بهینه‌ساز رو نوشتن و تیم فقط برچسب CI و نتیجهٔ بنچمارک رو نگاه می‌کنه