مرزهای کاری که TLA+ می‌تونه ثابت کنه
تست
هوش مصنوعیخلاصهٔ کامل‌تر
تو این مقاله اومده که هیجان این روزها دربارهٔ خوب شدن مدل‌های هوش مصنوعی تو نوشتن TLA+ (یه زبان مشخصه‌نویسی رسمی که باهاش رفتار سیستم رو ریاضی‌وار توصیف می‌کنی) بیش از اندازه‌ست. نویسنده که خودش کتاب TLA+ نوشته می‌گه گیر کار مدل نیست، خود ابزاره: یه سری خاصیت اصلاً تو این زبان قابل نوشتن نیستن.
TLA+ سیستم رو مجموعه‌ای از behavior می‌بینه، یعنی همهٔ دنباله‌های ممکنِ حالت‌ها. دو جور خاصیت می‌نویسی: []P یعنی P تو همهٔ حالت‌های همهٔ دنباله‌ها برقراره، همون invariant آشنا مثل «داده هیچ‌وقت خراب نمی‌شه». P یعنی P دست‌کم تو یه حالت از هر دنباله اتفاق می‌افته. ترکیب این دوتا چیزهای قوی‌تری می‌ده، مثل «اگه پیامی رفت تو صف، آخرش یه worker پردازشش می‌کنه».
چیزی که نمی‌شه نوشت هم کم نیست. خاصیت‌های امکان‌پذیری مثل «کاربر همیشه بتونه رمزش رو عوض کنه» با P درنمیان، چون P می‌گه تو همهٔ مسیرها حتماً اتفاق می‌افته، نه اینکه از هر نقطه دست‌کم یه مسیر هست که توش شدنیه. hyperpropertyها هم بیرونن، یعنی خاصیت‌هایی که روی دو یا چند اجرا با هم تعریف می‌شن، مثل «کاربر از دادهٔ عمومی نتونه رازها رو حدس بزنه». خاصیت‌های آماری مثل تأخیر صدک ۹۵ و مقاومت سیستم در برابر تغییر کد هم همین‌طور.
بعضی از اینا تو فرمالیزم‌های دیگه جواب می‌دن، CTL برای reachability (یعنی «اصلاً میشه به این حالت رسید یا نه») و PRISM برای خاصیت‌های آماری، ولی اونا هم محدودیت خودشون رو دارن و هیچ ابزاری همه‌کاره نیست. به گفتهٔ نویسنده ریشهٔ ماجرا اینه که خاصیت باید فرمول منطقی باشه، و ۹۹ درصد چیزهایی که برامون مهمه، مثل «اطلاعات سایت راحت پیدا میشه» یا «اپ ما نمی‌تونه برای قانون‌شکنی استفاده بشه»، اصلاً فرمول‌پذیر نیستن. TLA+ تو شکار باگ‌های همزمانی عالیه، فقط قرار نیست همهٔ نگرانی‌مون رو تموم کنه.
نکات کلیدی:
- []P یعنی P تو همهٔ حالت‌های هر اجرا برقراره؛ P یعنی دست‌کم تو یه حالت از هر اجرا
- خاصیت‌های امکان‌پذیری مثل «کاربر همیشه می‌تونه رمزش رو عوض کنه» تو TLA+ بیان‌شدنی نیستن
- hyperpropertyها چون روی دو یا چند اجرا تعریف می‌شن از دست TLA+ خارجن
- CTL خاصیت reachability و PRISM خاصیت آماری رو پوشش می‌ده، ولی هر کدوم محدودیت خودشون رو دارن
- نویسنده می‌گه ۹۹ درصد خاصیت‌هایی که واقعاً برامون مهمن اصلاً به فرمول منطقی درنمیان
