آیا Lean برنده‌ی بلندمدت کدنویسی با LLM ـه؟
هوش مصنوعیخلاصهٔ کامل‌تر
گورن با یه نگرانی امنیتی شروع می‌کنه: مدل‌های کدنویس دارن بخش بزرگی از نرم‌افزار آینده رو می‌نویسن، ولی کیفیتشون معمولاً متوسط یا ناامنه. راه فرار احتمالی، نوشتن نرم‌افزار به زبان‌های اثبات‌پذیر مثل Lean ـه — منتها چقدر از این هدف عقبیم؟ پیشنهاد او اینه که به‌جای بحث ذوقی، مسئله رو با قوانین مقیاس‌پذیری اندازه بگیریم.
استدلال رایج اینه که LLMها تو زبان‌های پرطرفدار بهترن چون داده‌ی بیشتری دارن، پس زبان‌های بهتر مثل Rust یا Lean تو یه قفل‌شدگیِ ابدی گیر می‌کنن. نویسنده می‌گه این نتیجه‌گیری غلطه: داده‌ی زیاد فقط یعنی مدل «به‌طور پیش‌فرض» خوب شروع می‌کنه. مهارت‌ها بین زبان‌ها تا حدی منتقل می‌شن، پس بهتر شدن مدل‌ها ممکنه اتفاقاً رنسانسی برای زبان‌های گمنام بسازه.
نکته‌ی دوم اینه که خوب بودن تو مقیاس کوچیک، تضمینی برای مقیاس بزرگ نیست. نوشتن یه اسکریپت کوتاه پایتون آسونه و کلش تو پنجره‌ی زمینه جا میشه؛ ولی وقتی کدبیس بزرگ و کهنه شد و دیگه تو زمینه جا نشد، مدل باید تایپ‌های پویا، استثناها، monkey-patchهای گوشه‌وکنار و رفتار عوض‌شده‌ی یه وابستگی رو هم‌زمان تو ذهنش نگه داره. یه خطای کوچیک هم می‌تونه هفته‌ها دیباگ ببره.
مشکل Lean هم صریحه: کد Lean زیادی تو دنیا وجود نداره، پس مدل‌ها توش خیلی خوب نیستن — یه دور باطل مرغ و تخم‌مرغ. برای این‌که کدبیس بزرگ Lean داشته باشیم به مدلی نیاز داریم که Lean خوب بنویسه، و برای اون مدل به کدبیس بزرگ Lean نیاز داریم.
راه پیشنهادی نویسنده برای شکستن این حلقه، یه شاخص جانشینه: پیش‌بینی‌پذیری. کد بد از دید یه LLM «سخت‌خوان» ـه — باید ده فایل دیگه رو بخونی تا بفهمی یه تابع واقعاً چی‌کار می‌کنه. کد خوب برعکس، هرچی بیشتر ازش می‌بینی پیش‌بینی‌پذیرتر میشه. پس perplexity (یا بیت بر کاراکتر) یه سنجه‌ی تقریبی برای کیفیت طراحی در مقیاسه.
طرح آزمایش هم عملیه و به گفته‌ی خودش در حد یه پروژه‌ی دانشجویی: کدبیس‌ها رو به تفکیک زبان به یه فایل بزرگ تبدیل کن، با یه مدل منجمد perplexity رو در هر موقعیت از پنجره‌ی زمینه اندازه بگیر، بر حسب زبان نرمال‌سازی کن، منحنی مقیاس‌پذیری رو برازش بده و بعد اکستراپوله کن تا نقطه‌ی تقاطع زبان‌ها پیدا بشه.
چند آزمون جانبی هم پیشنهاد می‌ده: تزریق باگ‌های ظریف (هرچی مدل بیشتر جا بخوره، بهتر)، حذف/افزودن type signatureها برای سنجش فایده‌ی واقعی‌شون، و این‌که آیا مدل می‌تونه یه ماژول Lean رو فقط از روی امضای تایپ‌هاش بازتولید کنه.
پیش‌بینی خودش اینه که زبان‌های «ضعیف» با تایپ پویا و حالت سراسری تو مقیاس چند هزار خط راحت‌تر پیش‌بینی می‌شن ولی نمای مقیاس‌پذیری بدتری دارن و جایی حوالی صدها هزار تا میلیون خط، از زبان‌های «قوی» عقب می‌افتن. Lean هم به‌خاطر ثابت اولیه‌ی بسیار بد، شاید تو طول‌های متعارف تو خطای مطلق جلو نزنه، ولی بهترین نما رو داره — و همین توجیه اقتصادیِ خرید داده‌ی آموزشی Lean و بازنویسی کدهاست.
نویسنده خودش هم حالت شکست رو می‌بینه: ممکنه اثر بلوغ اکوسیستم و اندازه‌ی پیکره، بر ویژگی‌های ذاتی زبان غلبه کنه — مثلاً کد Lean رو آدم‌های غیرعادی (آکادمیک‌ها) و درباره‌ی ریاضی می‌نویسن، ولی جاوااسکریپت رو برنامه‌نویس‌های معمولی برای وب. حتی همین نتیجه هم مفیده: یعنی ابزار و قرارداد و مستندات، دست‌کم فعلاً، از ویژگی‌های صوریِ زبان مهم‌ترن.
نکات کلیدی:
- پیشنهاد: به‌جای بحث سلیقه‌ای، قوانین مقیاس‌پذیریِ perplexity به تفکیک زبان رو اندازه بگیریم
- پیش‌بینی‌پذیری در مقیاس، جانشینِ کیفیت طراحیه: کد خوب هرچی بیشتر ببینی، پیش‌بینی‌پذیرتر میشه
- حدس نویسنده: پایتون ثابت بهتر ولی نمای بدتر؛ Lean ثابت بد ولی بهترین نما
- آزمون‌های جانبی: تزریق باگ ظریف، حذف type signature، بازتولید ماژول از روی امضای تایپ
- دور باطل Lean: مدل خوب می‌خواد کد زیاد، کد زیاد می‌خواد مدل خوب
- حالت شکست محتمل: بلوغ اکوسیستم و اندازه‌ی پیکره بر ویژگی‌های زبان غلبه کنه
