سیستم‌های کامپیوتری امروزی به‌طور فزاینده‌ای در محیط‌هایی به کار گرفته می‌شوند که در آن‌ها نمی‌توانند وضعیت واقعی محیط را مستقیماً تشخیص دهند و تنها اطلاعات ناقصی از طریق مشاهدات دریافت می‌کنند. در چنین شرایطی، نرم‌افزار ممکن است باور نادرستی درباره وضعیت واقعی محیط پیدا کند و همین امر می‌تواند به فجایع جبران‌ناپذیری منجر شود. نمونه‌ای مشهور از این دست، کاوشگر قطبی مریخ است که به دلیل خطای نرم‌افزار کنترل فرود، موتور فرود را در ارتفاع چهل متری به‌اشتباه خاموش کرد و سقوط کرد. این رویداد نشان می‌دهد که توسعه‌دهندگان به ابزارهای بهتری برای نوشتن نرم‌افزار در محیط‌های دارای مشاهده‌پذیری جزئی نیاز دارند. این پایان‌نامه با هدف ارائه چنین ابزارهایی، سه دستاورد اصلی را معرفی می‌کند: برنامه‌نویسی باور، منطق هور معرفتی و استنتاج نیمه‌نمادین. این سه دستاورد در کنار یکدیگر چارچوبی کامل برای نوشتن، اثبات درستی و اجرای کارآمد نرم‌افزار در محیط‌های نامطمئن فراهم می‌آورند.

دستاورد نخست، برنامه‌نویسی باور است؛ روشی نوین که در آن توسعه‌دهنده به‌جای نوشتن دستی تخمین‌زننده وضعیت، تنها مدلی از نحوه مشاهده‌پذیری محیط را در قالب یک برنامه توصیف می‌کند. زبان برنامه‌نویسی به‌طور خودکار این مدل را به یک تخمین‌زننده وضعیت قابل اجرا تبدیل می‌کند که مشاهدات محیطی را به تخمینی از وضعیت واقعی محیط نگاشت می‌کند. برای تحقق این ایده، زبانی نمونه‌ای به نام بلایمپ طراحی شده که از زبان آموزشی ایمپ الهام گرفته و سازوکارهایی برای مدل‌سازی محیط، ثبت مشاهدات و استنتاج درباره باورها ارائه می‌دهد. در این زبان، مفهوم «حالت باور» نقش محوری دارد؛ مجموعه‌ای از همه وضعیت‌های ممکن که برنامه معتقد است محیط می‌تواند در آن‌ها باشد. هر دستور برنامه، به‌جای به‌روزرسانی یک محیط مشخص، این مجموعه از وضعیت‌های ممکن را به‌روزرسانی می‌کند. این رویکرد باعث می‌شود توسعه‌دهنده به‌جای درگیر شدن با خطاهای اندازه‌گیری و پیچیدگی‌های تلفیق داده‌های حسگرها، بر مدل‌سازی دقیق عدم‌قطعیت تمرکز کند و زبان، خود به‌طور خودکار تخمین‌زننده صحیح را بسازد.

برای نشان دادن توانایی این روش، چند نمونه عملی در پایان‌نامه پیاده‌سازی شده است. یکی از این نمونه‌ها، کنترل‌کننده ارتفاع یک هواپیمای بدون سرنشین است که هدف آن حفظ ارتفاع در محدوده‌ای امن با وجود خطای اندازه‌گیری و وزش باد است. نمونه دیگر، بازنویسی نرم‌افزار کنترل موتور کاوشگر قطبی مریخ با زبان برنامه‌نویسی باور است؛ نسخه‌ای که برخلاف نرم‌افزار اصلی، می‌توان درستی آن را به‌طور رسمی اثبات کرد. نمونه سوم، پیاده‌سازی سیستم‌های افزونگی دوگانه و سه‌گانه است که در آن‌ها چند نسخه از یک ورودی نامطمئن تکرار می‌شود و برنامه باید با مقایسه آن‌ها خطا را تشخیص دهد و در صورت امکان تصحیح کند. این مثال‌ها نشان می‌دهند که برنامه‌نویسی باور می‌تواند در دامنه‌های متنوعی از کنترل پرواز تا سیستم‌های مقاوم در برابر خطا به کار گرفته شود و در هر مورد، فرایند تولید تخمین‌زننده وضعیت را خودکار و قابل‌اعتماد سازد.

دستاورد دوم، منطق هور معرفتی است؛ یک نظام منطقی که برای اثبات ویژگی‌های برنامه‌های نوشته‌شده با برنامه‌نویسی باور طراحی شده است. منطق هور کلاسیک ابزاری برای استدلال درباره برنامه‌های معمولی است، اما برای برنامه‌هایی که با حالت باور و عدم‌قطعیت سر و کار دارند کافی نیست. منطق هور معرفتی با افزودن عملگرهای وجهی، این شکاف را پر می‌کند. عملگر «ضرورت» به این معناست که یک گزاره در همه وضعیت‌های ممکن موجود در حالت باور صادق است و عملگر «امکان» به این معناست که گزاره در دست‌کم یک وضعیت ممکن صادق است. با این عملگرها، توسعه‌دهنده می‌تواند عباراتی مانند «در همه حالت‌های ممکن، ارتفاع هواپیما کمتر از یک متر نیست» را صورت‌بندی و اثبات کند. این منطق همراه با قواعد استنتاج و اثبات درستی آن ارائه شده و نسخه‌ای کامل‌تر نیز معرفی شده که توان اثبات بیشتری دارد، هرچند استفاده از آن دشوارتر است. بدین ترتیب، توسعه‌دهنده می‌تواند اطمینان یابد که نرم‌افزارش تحت هر شرایطی که مدل محیط مجاز می‌داند، ویژگی‌های ایمنی موردنظر را رعایت می‌کند.

کاربرد منطق هور معرفتی در چند مطالعه موردی نشان داده شده است. در نمونه هواپیمای بدون سرنشین، اثبات می‌شود که کنترل‌کننده ارتفاع را در محدوده مجاز نگه می‌دارد. در نمونه کاوشگر قطبی مریخ، اثبات می‌شود که موتور تا زمانی که کاوشگر روی سطح زمین قرار نگرفته خاموش نمی‌شود؛ همان خطایی که باعث سقوط نسخه اصلی شده بود. در نمونه افزونگی سه‌گانه نیز اثبات می‌شود که سیستم همیشه می‌تواند مقدار صحیح را بازیابی کند، حتی اگر یکی از ورودی‌ها معیوب باشد. این اثبات‌ها بر پایه قواعد منطقی و با استفاده از ویژگی‌های عمومی عملگرهای وجهی انجام می‌شوند، مانند توزیع‌پذیری عملگر ضرورت بر عطف، رابطه دوگانگی میان ضرورت و امکان، و امکان انتقال دانش از گزاره‌های کلی به گزاره‌های وجهی. مجموع این مطالعات نشان می‌دهد که منطق هور معرفتی ابزاری عملی و قدرتمند برای تضمین درستی نرم‌افزار در محیط‌های نامطمئن است.

دستاورد سوم، استنتاج نیمه‌نمادین است؛ تکنیکی برای اجرای کارآمد برنامه‌های باور. پیاده‌سازی ساده‌لوحانه یک برنامه باور، با شمارش تمام وضعیت‌های ممکن در حالت باور کار می‌کند و همین امر باعث می‌شود زمان اجرا به‌طور نمایی با تعداد متغیرها رشد کند. استنتاج نیمه‌نمادین به‌جای شمارش کامل، از بازنمایی نمادین استفاده می‌کند؛ برای مثال، به‌جای فهرست کردن همه ارتفاع‌های ممکن یک هواپیما، آن‌ها را به‌صورت یک بازه نمایش می‌دهد و تنها نقاط ابتدا و انتهای بازه را به‌روزرسانی می‌کند. عملیات اصلی این روش شامل جابه‌جایی متغیرهای نمادین، جایگذاری مقدار مشاهده‌شده، و ارزیابی جزئی عبارات است. این عملیات به‌گونه‌ای طراحی شده‌اند که مجموعه وضعیت‌های ممکن را بدون تغییر معنای آن، فشرده‌تر و سریع‌تر بازنمایی کنند. همچنین مفهوم «خانواده‌های بسته» معرفی شده که تضمین می‌کند در برخی برنامه‌ها، عملیات نمادین بدون نیاز به بازگشت به شمارش کامل انجام می‌شوند و بنابراین کارایی برنامه قابل پیش‌بینی است.

ارزیابی عملکرد نشان می‌دهد که استنتاج نیمه‌نمادین سرعت اجرا را به‌طور چشمگیری افزایش می‌دهد. در مجموعه‌ای از محک‌ها، این روش نسبت به پیاده‌سازی ساده‌لوحانه سرعت‌هایی بین پانصد و پانزده برابر تا پنجاه و هشت هزار و نهصد و نوزده برابر به دست می‌آورد. در برخی دامنه‌ها، مانند کنترل کاوشگر مریخ، تنها با استنتاج نیمه‌نمادین است که زمان اجرا به آستانه‌های عملی و موردنیاز می‌رسد. این نتایج نشان می‌دهد که کارایی، نه یک موضوع حاشیه‌ای، بلکه پیش‌نیازی برای به‌کارگیری عملی برنامه‌نویسی باور در سیستم‌های واقعی است. در مجموع، این پایان‌نامه نخستین ارائه کامل یک روش‌شناسی یکپارچه برای برنامه‌نویسی و استدلال در محیط‌های دارای مشاهده‌پذیری جزئی است. این روش‌شناسی به توسعه‌دهندگان امکان می‌دهد مدل محیط را بنویسند، درستی نرم‌افزار را به‌طور رسمی اثبات کنند و آن را به‌صورت کارآمد اجرا کنند. با رفع چالش‌های باقی‌مانده در خودکارسازی اثبات‌ها و گسترش دامنه‌های کاربرد، این چارچوب می‌تواند به ابزاری فراگیر برای ساخت سیستم‌های کامپیوتری خودمختار و ایمن در آینده تبدیل شود.

وقتی ماشین‌ها «باور» پیدا می‌کنند: سفری به دنیای مشاهده‌پذیری جزئی

تصور کنید در حال رانندگی در مه غلیظ هستید. چراغ‌های جلو فقط چند متر جلوتر را روشن می‌کنند و شما نمی‌دانید جاده دقیقاً به کجا می‌رود. با این حال، باید تصمیم بگیرید: ترمز بگیرید، بپیچید یا مستقیم بروید. این وضعیت دقیقاً همان چیزی است که سیستم‌های کامپیوتری امروزی در محیط‌های واقعی با آن دست‌وپنجه نرم می‌کنند. خودروهای خودران، کاوشگرهای فضایی و ربات‌های صنعتی هیچ‌گاه نمی‌توانند وضعیت واقعی محیط را با قطعیت کامل بدانند. آن‌ها فقط مشاهدات ناقصی دریافت می‌کنند و باید بر اساس همین اطلاعات محدود، تصمیم‌های حیاتی بگیرند. حالا سؤال این است: اگر یک کاوشگر فضایی به‌اشتباه فکر کند روی سطح مریخ فرود آمده، در حالی که هنوز چهل متر بالاتر است، چه فاجعه‌ای رخ می‌دهد؟

داستان واقعی یک سقوط: کاوشگر قطبی مریخ

در سال ۱۹۹۹، کاوشگر قطبی مریخ در حال فرود بر سطح سیاره سرخ بود. این کاوشگر مجهز به یک ارتفاع‌سنج راداری و چند حسگر تماس روی پایه‌های فرود بود. قرار بود موتور فرود تا لحظه تماس با سطح روشن بماند. اما نرم‌افزار کنترل، داده‌های حسگرها را اشتباه تفسیر کرد. وقتی کاوشگر هنوز چهل متر بالاتر از سطح بود، نرم‌افزار باور کرد که فرود انجام شده و موتور را خاموش کرد. کاوشگر سقوط کرد و از بین رفت. این حادثه نشان می‌دهد که وقتی سیستم نمی‌تواند وضعیت واقعی محیط را مستقیماً ببیند، باورهای نادرست می‌توانند به فاجعه منجر شوند.

نکته تأمل‌برانگیز اینجاست که مشکل از سخت‌افزار نبود. حسگرها کار خود را درست انجام می‌دادند. مشکل از نرم‌افزاری بود که نمی‌توانست عدم‌قطعیت را به‌درستی مدیریت کند. این دقیقاً همان جایی است که ایده «برنامه‌نویسی باور» متولد می‌شود.

برنامه‌نویسی باور: وقتی کد، عدم‌قطعیت را می‌فهمد

تصور کنید به‌جای اینکه برنامه‌نویس دستی تخمین بزند که «ارتفاع واقعی چقدر است»، خود زبان برنامه‌نویسی این کار را انجام دهد. در برنامه‌نویسی باور، توسعه‌دهنده فقط مدلی از محیط می‌نویسد؛ مثلاً «ارتفاع می‌تواند بین ۴۷۵ تا ۵۲۵ متر باشد» یا «حسگر تماس ممکن است خطای گذرا داشته باشد». سپس زبان برنامه‌نویسی به‌طور خودکار این مدل را به یک تخمین‌زننده وضعیت تبدیل می‌کند که مشاهدات را دریافت می‌کند و می‌گوید: «بر اساس آنچه دیده‌ام، ارتفاع واقعی احتمالاً این محدوده است.»

برای تحقق این ایده، زبانی به نام «بلایمپ» طراحی شده است. در این زبان، مفهومی به نام «حالت باور» وجود دارد؛ یعنی مجموعه‌ای از همه وضعیت‌هایی که برنامه فکر می‌کند محیط ممکن است در آن‌ها باشد. هر دستور برنامه، این مجموعه را به‌روزرسانی می‌کند. برای مثال، وقتی حسگر تماس می‌گوید «زمین را لمس کردم»، برنامه فقط آن وضعیت‌هایی را نگه می‌دارد که با این مشاهده سازگارند. این رویکرد باعث می‌شود برنامه‌نویس به‌جای درگیر شدن با جزئیات پیچیده تلفیق داده‌های حسگرها، بر مدل‌سازی دقیق عدم‌قطعیت تمرکز کند.

«در برنامه‌نویسی باور، توسعه‌دهنده فقط مدل محیط را می‌نویسد و زبان، خود به‌طور خودکار تخمین‌زننده صحیح را می‌سازد.»

این نقل قول از خود پایان‌نامه، جوهره اصلی این روش را نشان می‌دهد: خودکارسازی فرایندی که قبلاً دستی و خطاپذیر بود.

منطق هور معرفتی: اثبات درستی در دنیای نامطمئن

نوشتن برنامه کافی نیست. باید مطمئن شویم برنامه درست کار می‌کند. در دنیای برنامه‌های معمولی، از «منطق هور» استفاده می‌کنیم؛ یعنی مجموعه‌ای از قواعد برای اثبات اینکه برنامه ویژگی‌های موردنظر را رعایت می‌کند. اما در برنامه‌های باور، وضعیت پیچیده‌تر است؛ چون برنامه با مجموعه‌ای از وضعیت‌های ممکن سر و کار دارد، نه یک وضعیت مشخص.

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

نکته جالب اینجاست که این منطق نه‌تنها درستی را اثبات می‌کند، بلکه نسخه کاملی نیز دارد که می‌تواند هر ویژگی درستی را که در دنیای واقعی برقرار است، به‌طور رسمی اثبات کند. این یعنی توسعه‌دهنده می‌تواند با اطمینان کامل بگوید: «نرم‌افزار من تحت هر شرایطی که مدل محیط مجاز می‌داند، ایمن است.»

استنتاج نیمه‌نمادین: سرعتی باورنکردنی

حالا تصور کنید برنامه‌ای نوشته‌اید که باورها را به‌درستی مدیریت می‌کند و درستی آن را نیز اثبات کرده‌اید. اما یک مشکل بزرگ باقی می‌ماند: سرعت. پیاده‌سازی ساده‌لوحانه یک برنامه باور، باید تمام وضعیت‌های ممکن را یکی‌یکی بررسی کند. اگر متغیرها زیاد باشند، این کار مثل شمردن دانه‌های شن است؛ زمان اجرا به‌طور نمایی رشد می‌کند و برنامه غیرقابل استفاده می‌شود.

راه‌حل «استنتاج نیمه‌نمادین» است. به‌جای فهرست کردن همه مقادیر ممکن، از بازنمایی نمادین استفاده می‌شود. مثلاً به‌جای گفتن «ارتفاع می‌تواند ۵۰۰، ۵۰۱، ۵۰۲… باشد»، می‌گوییم «ارتفاع در بازه ۵۰۰ تا ۵۲۵ است». این کار مثل این است که به‌جای شمردن تک‌تک برگ‌های یک درخت، فقط بگوییم «این درخت بین ده تا پانزده هزار برگ دارد». نتیجه؟ سرعت اجرا تا پنجاه و هشت هزار برابر افزایش می‌یابد.

در برخی کاربردها، مثل کنترل کاوشگر مریخ، تنها با همین تکنیک است که زمان اجرا به آستانه‌های عملی می‌رسد. این نشان می‌دهد که کارایی، نه یک موضوع حاشیه‌ای، بلکه پیش‌نیازی برای استفاده واقعی از این فناوری است.

چرا این موضوع مهم است؟

همه ما در دنیایی زندگی می‌کنیم که ماشین‌ها هر روز بیشتر در تصمیم‌گیری‌های حساس دخالت می‌کنند. خودروهای خودران، پهپادهای تحویل دارو، ربات‌های جراح و کاوشگرهای فضایی همه در محیط‌هایی کار می‌کنند که عدم‌قطعیت بخش جدایی‌ناپذیر آن‌هاست. اگر نتوانیم نرم‌افزاری بنویسیم که این عدم‌قطعیت را به‌درستی مدیریت کند، فاجعه‌هایی مثل سقوط کاوشگر مریخ تکرار خواهند شد.

این پایان‌نامه نشان می‌دهد که راه‌حل وجود دارد. با ترکیب برنامه‌نویسی باور، منطق هور معرفتی و استنتاج نیمه‌نمادین، می‌توان نرم‌افزاری نوشت که هم درست باشد، هم قابل اثبات و هم سریع. این یعنی آینده‌ای که در آن ماشین‌ها با اطمینان بیشتری در کنار ما کار می‌کنند و تصمیم‌هایشان قابل اعتمادتر است. شاید روزی برسد که دیگر هیچ کاوشگری به‌خاطر یک باور نادرست سقوط نکند.