برنامه هیلبرت، هوش مصنوعی و بحران فراموشی در درک کد

مقدمه و زمینه تاریخی

یک قرن پیش، ریاضیات با یک بحران بنیادین روبه‌رو شد. پارادوکس‌هایی مانند پارادوکس راسل در نظریه مجموعه‌ها نشان داد که پایه‌های ریاضیات آن‌چنان که تصور می‌شد قرص و محکم نیستند. در این میان، دیوید هیلبرت (David Hilbert) برنامه‌ای را آغاز کرد تا سیستمی از اصول موضوعه کامل و سازگار ایجاد کند که بتوان تمام حقایق ریاضی را از آن‌ها استخراج کرد. با این حال، قضیه‌های ناتمامیت گودل (Gödel) نشان دادند که چنین سیستم کاملی نمی‌تواند وجود داشته باشد. پس از آن، آلن تورینگ (Alan Turing) نیز با اثبات مسئله توقف (Halting Problem) نشان داد که ایجاد یک الگوریتم خودکار برای تصمیم‌گیری درباره درستی هر گزاره ریاضی ناممکن است؛ اتفاقی که به تولد علوم کامپیوتر انجامید.

تحقق رویای هیلبرت در عصر هوش مصنوعی

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

چرا این موضوع برای مهندسان نرم‌افزار مهم است؟

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

بر اساس تطابق کریستارد-هوارد (Church-Howard correspondence)، یک برنامه کامپیوتری در واقع همان اثبات ریاضی است. وقتی توسعه‌دهندگان کدهایی را که تمامی تست‌ها را پاس کرده‌اند بدون خواندن می‌پذیرند، دقیقاً کاری را می‌کنند که یک ریاضیدان در مواجهه با اثبات‌های غیرقابل‌هضم AI انجام می‌دهد؛ با این تفاوت که ریاضیدانان تلاش می‌کنند اثبات را ساده و قابل‌هضم کنند، اما برنامه‌نویسان تسلیم می‌شوند.

نگاهی به بحث‌های هکرنیوز

در بحث‌های پیرامون این مقاله در Hacker News، کاربران چالش‌های این دیدگاه را بررسی کرده‌اند:

• برخی کاربران پرسیده‌اند که آیا واقعاً باید کد ماشین یا اسمبلی تولیدشده از کدهای Go یا C را در ذهن خود نگه داریم؟ یا اینکه شاید انتزاع‌های سطح بالا مانند زبان‌های برنامه‌نویسی یا حتی مستندات طراحی (Design Docs) کافی هستند؟
• دیدگاه دیگر بر این تاکید می‌کند که خطر اصلی، پایین آمدن استانداردهاست و جامعه مهندسی نرم‌افزار نباید تسلیم وسوسه واگذاری کامل درک سیستم به ماشین‌ها شود.

نتیجه‌گیری

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