تصور کنید یک برنامهنویس ارشد در تلاش است تا مطمئن شود عامل هوش مصنوعی او هرگز در یک حلقهی تکراری گیر نمیکند یا دسترسیهای غیرمجاز ایجاد نمیکند. اگر فکر میکنید ابزارهای تأیید رسمی میتوانند این نگرانیها را بهطور کامل از بین ببرند، باید با یک حقیقت ریاضی تلخ روبرو شوید.
به نقل از بوریس چرنی (Boris Cherny)، ابداعکنندهی Claude Code، مدل Claude Opus میتواند از TLA+ برای شناسایی تداخلات یا همان Race Conditions استفاده کند. او این نکته را هفته گذشته اشاره کرد، اما مشاهدهی او موجی از خوشبینی خطرناک را ایجاد کرده است؛ گویی روشهای رسمی قرار است هرجومرج توسعهی عاملمحور (Agentic) را یکبار برای همیشه پایان دهد. من به عنوان کسی که سالها مدرس و حامی TLA+ بودهام، توانایی طراحی سیستمهای همزمان پیچیده و تضمین بدونخطا بودن آنها را هیجانانگیز میدانم؛ اما به عنوان کسی که طرفدار واقعبینی است، نگرانم که تأیید رسمی (Formal Verification) را به اشتباه به عنوان یک «گلولهی جادویی» برای حل آشفتگیهای نرمافزارهای عاملمحور بشناسند.
این هیجان، یک حقیقت بنیادی را نادیده میگیرد: یک سیستم تنها زمانی قابل تأیید است که ویژگی مورد نظر را بتوان به صورت یک فرمول منطقی بیان کرد. برای بسیاری از شکستهای بحرانی در عاملهای هوش مصنوعی (AI Agents)، چنین فرمولی وجود ندارد. بسیاری استدلال میکنند که روشهای رسمی توسعهی نرمافزارهای عاملمحور را برای همیشه حل میکند، اما این حرف بیمعنی است. ما پیش از این دربارهی نقاط ضعف TLA+ بحث کردهایم؛ اینکه چگونه طراحیهای درست لزوماً به کدهای درست ترجمه نمیشوند. اما محدودیت عمیقتر این است که برای تأیید یک ویژگی، ما ابتدا باید ویژگیای داشته باشیم که بتوانیم آن را تأیید کنیم.
تصور کنید میخواهید ثابت کنید یک عامل هوش مصنوعی «مفید» یا «ایمن» است. اگر نتوانید مفهوم انسانی «مفید بودن» یا تعریف یک «پرنده» را به یک عبارت ریاضی تبدیل کنید، TLA+ نمیتواند ثابت کند که عامل شما پرندهها را میشناسد یا دارای ویژگی مفید بودن است. این شکاف بین قصد انسان و مشخصات منطقی، سقف اصلی تأیید رسمی است. این چالش در ارزیابیهای سنتی نیز دیده میشود، به همین دلیل است که رویکردهایی مانند تستهای ساختاری انویدیا برای جایگزینی ارزیابیهای حسی در عاملها توسعه یافتهاند تا دقت سنجش را افزایش دهند.
منطق بررسی در TLA+
برای درک محدودیتها، ابتدا باید سازوکار این ابزار را بشناسیم. TLA+ سیستم را به مجموعهای از رفتارها تقسیم میکند. هر رفتار، توالیای از حالتهاست؛ برای مثال، یک توالی چراغ راهنمایی که در آن «چراغ اول سبز است، سپس زرد و سپس قرمز میشود». در هر حالت، میتوانیم عبارات بولی معمولی را بیان کنیم، مانند «چراغ چهارم سبز است» یا «تمام چراغها قرمز هستند».
این ابزار از عملگرهای منطقی زمانی خاصی برای بررسی این حالتها استفاده میکند:
- ناورداها (Invariants - []P): عملگر
[]P(به معنای «همیشه P») زمانی درست است که P در حالت فعلی و هر حالت آینده درست باشد. برای مثال،[](at_most_one_green)تضمین میکند که در هر حالتی در آینده، بیش از یک چراغ سبز وجود نداشته باشد. این پایه و اساس ویژگیهای ایمنی (Safety Properties) است، به این معنا که «اتفاق بد هرگز رخ نمیدهد». - ویژگیهای عملیاتی (Action Properties): اینها از «پرایمها» (P') برای بررسی انتقالها استفاده میکنند.
P'درست است اگر P در حالت بعدی درست باشد. یک مثال،light="green" && light'="red"است که اگر چراغ از سبز به قرمز تغییر کند، درست است. ما میتوانیم اینها را ترکیب کنیم تا تضمین کنیم یک مقدار فقط افزایش مییابد، مانند[](x' >= x)، یا تضمین کنیم که وقتی حالتی حاصل شد، هرگز به حالت قبلی برنگردد:[](P => P'). - ویژگیهای زنده بودن (Liveness Properties - <>P): عملگر
<>P(به معنای «در نهایت P») زمانی درست است که P در حالت فعلی یا حداقل در یکی از حالتهای آینده درست باشد. زنده بودن تضمین میکند که «اتفاق خوب همیشه رخ میدهد».
از آنجایی که <>P به تنهایی اغلب بسیار ضعیف است، TLA+ از ترکیبها برای ویژگیهای زنده بودن جالبتر استفاده میکند:
- تکرار بینهایت (Infinite Recurrence - []<>P): این عبارت زمانی درست است که در هر حالت، P در حداقل یک حالت آینده درست باشد. این برای مکانیسمهای بازیابی (Recovery) استفاده میشود؛ مثلاً ثابت میکند که اگر گرهها یک انتخابات لیدر جدید داشته باشند، در نهایت روی یک لیدر توافق میکنند.
- پایداری (Stability - <>[]P): این عبارت زمانی درست است که در نقطهای از زمان، P درست شود و برای همیشه درست باقی بماند. این برای نشان دادن اینکه الگوریتمها با نتایج درست متوقف میشوند، ایدهآل است.
- منجر شدن به (Leads-to - [](P => <>Q)): این عبارت زمانی درست است که برای هر حالتی که در آن P درست است، حالتی در آینده وجود داشته باشد که در آن Q درست باشد. این ثابت میکند که P در نهایت باعث Q میشود، یا اینکه «تمام پیامهایی که در صف قرار میگیرند، در نهایت در تاریخچهی خواننده قرار میگیرند». TLA+ برای این فرمول، علامت سادهی
P ~> Qرا ارائه میدهد.
در حالی که عملگرهایی مانند ENABLED و <<A>>_v ترفندهای بیشتری ارائه میدهند و «پالایش» (Refinement) ویژگیهای ایمنی و زنده بودن را ترکیب میکند، اکثریت بررسیها بر ناورداها، ویژگیهای عملیاتی و زنده بودن متمرکز هستند.
مرزهای سخت بیان منطقی
با وجود این قدرتها، چندین دسته از ویژگیها وجود دارند که TLA+ بهطور بومی قادر به بیان آنها نیست:
۱. جزئیات و زمان: ویژگیهای ایمنی TLA+ روی سطح حالتهای فردی (ناورداها) یا گامهای واحد (ویژگیهای عملیاتی) کار میکنند. شما نمیتوانید بهطور بومی ویژگیای را تعریف کنید که دو یا چند گام را در بر بگیرد؛ مثلاً «فشردن دکمه حذف و سپس لغو، حالت اولیه را بازیابی میکند» یا «پس از فشردن دکمه پاور، کامپیوتر ظرف ۱۰ گام روشن میشود». علاوه بر این، این ابزار نمیتواند عملیات اعداد اعشاری یا محدودیتهای زمانی واقعی (Real-time) را مدیریت کند، زیرا صرفاً بر اساس زمان منطقی عمل میکند.
۲. قابلیت دسترسی (Reachability): ویژگیهای TLA+ بهطور ضمنی روی تمام رفتارها کوانتیزه شدهاند. بررسی []P در واقع به این معناست که «برای تمام رفتارها، []P برای حالت اولیه آن رفتار درست است». در نتیجه، TLA+ نمیتواند بیان کند که «رفتاری وجود دارد که در آن P درست باشد». این یعنی نمیتوانید از آن برای ثابت کردن اینکه یک بازی قابل بُرد است یا یک حالت خاص از هر حالت اولیهای قابل دسترسی است، استفاده کنید. قابلیتهای دسترسی پیشرفتهتر، مانند «P از هر حالتی که در آن Q درست باشد قابل دسترسی است»، نیز بهطور بومی پشتیبانی نمیشوند.
۳. هایپر-ویژگیها (Hyperproperties): TLA+ نمیتواند «هایپر-ویژگیها» را تأیید کند؛ ویژگیهایی که روی مجموعهای از رفتارها تعریف میشوند، نه یک رفتار واحد. برای مثال، اگر سختافزار تلفن را مدلسازی میکنید، ممکن است بخواهید تأیید کنید که حالت ذخیره انرژی همیشه انرژی کمتری نسبت به حالت عادی مصرف میکند. این کار مستلزم مقایسه دو رفتار یکسان است—یکی در حالت ذخیره انرژی و یکی بدون آن. چون یک رفتار واحد برای رد کردن این ادعا کافی نیست، بررسی آن بهطور طبیعی در TLA+ غیرممکن است. هایپر-ویژگیها برای ویژگیهای امنیتی و آماری، مانند «زمان پاسخدهی در صدک ۹۵٪ برابر با ۵ میلیثانیه است»، حیاتی هستند.
۴. متا-ویژگیهای فضای حالت: در نهایت، TLA+ نمیتواند ویژگیهایی را روی کل فضای حالت تعریف کند. برای مثال، نمیتوانید ثابت کنید که تنها یک مسیر منحصربهفرد از حالت X به Y وجود دارد. اگرچه این «متا-ویژگیها» بیشتر جنبه آکادمیک دارند، اما مرز منطق این ابزار را نشان میدهند.
خطر تکیه بر «ترفندها»
مهندسان باسابقه اغلب از راهکارهای جایگزین (Workarounds) برای دور زدن این محدودیتها استفاده میکنند. شما میتوانید ویژگیهای چندگامی را با استفاده از متغیرهای کمکی (Auxiliary Variables) شبیهسازی کنید تا تمام تغییرات حالت را در یک توالی state_history ذخیره کرده و ویژگی را به عنوان یک ناوردا روی آن توالی تعریف کنید. همچنین میتوانید برخی هایپر-ویژگیها را با «خود-ترکیبی» (Self-composition) شبیهسازی کنید، جایی که هر رفتار از مشخصات خود-ترکیبشده، نماینده دو رفتار از سیستم واقعی است.
علاوه بر این، مدلچکر اصلی TLA+ (یعنی TLC) میتواند قابلیت دسترسی پایه را با کلمه کلیدی REACHABLE و برخی ویژگیهای فضای حالت را با TLCGet بررسی کند. برخی حتی از «انصاف» (Fairness) و «بستار ماشین» (Machine Closure) برای شبیهسازی ویژگیهای «همیشه قابل دسترسی» استفاده میکنند.
اما اینها ترفندهایی با هزینههای شدید هستند:
- مشکلات پالایش (Refinement): متغیرهای کمکی، فرآیند پالایش را تخریب میکنند.
- انفجار فضای حالت: خود-ترکیبی باعث میشود فضای حالت شما بهصورت نمایی رشد کند و مدلچکر را کند یا غیرقابلاستفاده کند.
- پیچیدگی: این روشها باعث میشوند مدلها عجیب و آشفته به نظر برسند و دیگر با سیستمهای واقعی که نمایندگی میکنند، مطابقت نداشته باشند.
برای کسانی که به تضمینهای متفاوتی نیاز دارند، ابزارهای دیگری وجود دارد. CTL قابلیت دسترسی را بهتر مدیریت میکند و PRISM برای ویژگیهای احتمالی طراحی شده است. اما هیچیک از این ابزارها مشکل اصلی را حل نمیکنند: ناتوانی در تبدیل منطقی نیازهای مبهم انسانی به فرمولهای ریاضی.
این بدان معناست که در حالی که TLA+ برای شکار «میوههایt پایین» (یعنی باگهای سادهی تداخل) در سیستمهای همزمان عالی است، هرگز نمیتواند جایگزین نیاز به تستهای سختگیرانه و نظارت انسانی در گردشکارهای عاملمحور شود. در واقع، حتی وقتی تستها پاس میشوند، ممکن است لایههای عمیقتری از نقص وجود داشته باشد؛ موضوعی که در تحلیل ما درباره تستهای توخالی و شکست عاملهای کدنویس با وجود چراغ سبز به تفصیل بررسی شده است. باور به اینکه میتوانیم صرفاً با «تأیید رسمی» به عاملهای هوش مصنوعی بینقص برسیم، یک محال ریاضی است.
گام بعدی شما
- اگر از TLA+ برای طراحی سیستم استفاده میکنید، روی ناورداهای ساده تمرکز کنید و برای ویژگیهای رفتاری به تستهای یکپارچگی (Integration Tests) تکیه کنید.
- در توسعه عاملها، بهجای جستوجوی یک «اثبات ریاضی» برای ایمنی، روی ایجاد حفاظهای (Guardrails) لایهای تمرکز کنید.
- ابزارهای مدلسازی احتمالی مانند PRISM را برای سیستمهایی که با عدم قطعیت سروکار دارند بررسی کنید.
اما داستان سختافزاری این تحول حتی شگفتانگیزتر است — به تحلیل ما دربارهی تراشههای Blackwell مراجعه کنید.
گفتگو