TLA+ و ایجنتهای کدنویسی: شکار باگهای پنهان
هوش مصنوعیخلاصهٔ کاملتر
یکی از بهترین تکنیکها برای کار با ایجنتهای هوش مصنوعی اینه که یه «تپه» قابلسنجش بهشون بدی تا بالا برن — مثلاً یه مجموعه تست که باید همهشون پاس بشن. نویسنده این ایده رو یه قدم جلوتر برده و از TLA+ استفاده کرده: یه زبان مدلسازی رسمی که همه حالتهای ممکن یه سیستم رو بهصورت جامع بررسی میکنه. وقتی ایجنت هم مدل رو مینویسه و هم چکر رو اجرا میکنه، در واقع داره روی یه تپه کاملاً قابلتأیید بالا میره.
TLA+ برای سیستمهای توزیعشده و همزمان (concurrent) طراحی شده. مثلاً میتونی نحوه تقسیم یه شارد دیتابیس رو مدل کنی و از چکر بخوای ثابت کنه که هیچوقت دادهای از دست نمیره. چیزی که با تست معمولی شاید سالها پنهان بمونه، اینجا بهصورت خودکار کشف میشه — چکر مسیر دقیق رسیدن به اون حالت مشکلدار رو هم نشون میده.
جریان کاری که نویسنده به اون رسیده اینشکلیه: اول با ایجنت مشخص میکنه دقیقاً چه بخشی از کدبیس زیر ذرهبینه و فرضیههای اولیه رو مینویسه. بعد ایجنت مدل TLA+ رو مینویسه و چکر رو اجرا میکنه. اگه باگی پیدا شد، ایجنت یه تست فایل مینویسه که وجود باگ رو ثابت کنه، بعد باگ رو فیکس میکنه. خروجی نهایی خیلی سادهست: یه تست کوچیک که باگ رو نشون میده، و یه فیکس مختصر.
یه نکته مهم در مرحله مدلسازیه: باید صریحاً مشخص کنی چی خارج از مدله. وابستگیهای third-party، رفتار سیستمعامل، و هر چیزی که چکر رو با تعداد نجومی حالت روبرو میکنه باید کنار گذاشته بشه. وگرنه چکر ممکنه دهها گیگابایت trace بنویسه و عملاً قفل کنه.
برای اینکه مطمئن بشه نتایج واقعیه و نه noise، نویسنده این روش رو روی یه باگ شناختهشده توی ریپوی Pebble (یه key/value store) آزمایش کرد — کامیتی که احتمالاً توی دیتای آموزشی Claude نبود. ایجنت نهتنها اون باگ رو پیدا کرد، بلکه یه باگ دیگه هم کشف کرد که بعداً توی یه PR دیگه فیکس شده بود.
نکات کلیدی:
- TLA+ یه زبان مدلسازی رسمیه که همه حالتهای ممکن سیستم رو چک میکنه، مناسب race condition و باگهای توزیعشده
- ایجنتهای هوش مصنوعی میتونن مدل TLA+ رو بنویسن و چکر رو اجرا کنن بدون اینکه توسعهدهنده زبان رو بلد باشه
- خروجی مفید فقط یه تست + یه فیکس کوچیکه؛ بقیه کدهای تولیدشده رو میشه دور انداخت
- مرزبندی دقیق مدل (چی داخله، چی خارج) برای جلوگیری از انفجار حالتها ضروریه
- این رویکرد کد رو نهفقط سریعتر، بلکه واقعاً بهتر میکنه
