AI جلو نرفته، زمین بازی عوض شده
هوش مصنوعیClaude Opus 5خلاصهٔ کامل‌تر
تو ۲۰۲۴، AlphaProof از DeepMind سه تا از پنج مسئلهٔ غیرهندسهٔ المپیاد جهانی ریاضی رو حل کرد؛ نه با نوشتن استدلال به زبان معمولی، بلکه داخل Lean (یعنی زبانی که اثبات ریاضی رو طوری می‌نویسه که ماشین بتونه درستیش رو چک کنه). ونکاتش رائو، نویسندهٔ مقاله، می‌گه برداشت رایج اینه که AI داره به قله‌های هوش انسانی می‌رسه، ولی یه خوانش دیگه هم هست.
به گفتهٔ نویسنده، AlphaProof با ریاضیاتِ وحشی روبه‌رو نشد؛ با زمینی روبه‌رو شد که آدم‌ها بیشتر از یه قرن وقت گذاشتن تا شبیه بازی بشه. تو Lean هر گزاره یه type هست و اثبات یه ترم از اون type، و کتابخانهٔ Mathlib انبوهی از تعریف‌ها و قضیه‌های آماده رو نگه داشته. یعنی وضعیت هست، حرکت هست، دانش انباشته هست، شرط پایان هست و از همه مهم‌تر یه verifier هست که می‌گه اثبات درسته یا نه. ماشین تو فضای همهٔ نمادهای منطقی نمی‌گرده، تو دنیایی بازی می‌کنه که آدم‌ها ساختنش.
همین الگو تو برنامه‌نویسی و فیزیک هم تکرار شده. تو کد، خلاقیت از نوشتن دستور به سمت طراحی بازنمایی رفته؛ نویسنده جمله‌ای رو نقل می‌کنه که «بازنمایی‌ای رو پیدا کن که الگوریتم توش احمق بشه»، مثل کوئری دیتابیس که به‌جای گفتن نحوهٔ پیمایش رکوردها فقط نتیجه رو توصیف می‌کنی. تو فیزیک هم مکانیک نیوتنی جاش رو به لاگرانژ و همیلتون داد و پروژهٔ Physlib داره فیزیک رو داخل Lean فرمال می‌کنه.
ولی این بازی‌پذیری مجانی نیست. نویسنده به ایدهٔ خوانایی از جیمز اسکات اشاره می‌کنه: هر بازنمایی دقیقاً چون چیزهایی رو دور می‌ندازه مفیده. جسم صلبِ شبیه‌سازی واقعاً صلب نیست و اثباتِ داخل Lean اون شکلی رو که جرقهٔ ایده بوده توش نداره. سؤال درست این نیست که چیزی از دست می‌ره یا نه، اینه که آیا همون چیزهایی که بازی لازم داره سالم مونده یا نه. مثال Go تو جولای ۲۰۲۶ همینو نشون می‌ده: شین جین‌سو با دو سنگ هندیکپ مقابل موتور فوق‌بشری KataGo دو تا از سه بازی رو برد، نه با محاسبهٔ بهتر، بلکه با ساده نگه داشتن بازی و شناختِ رفتار حریفش.
جمع‌بندی نویسنده اینه که AI هزینهٔ بازی‌پذیر کردن یه حوزه رو پایین آورده: قبلاً یه دامنه باید کامل فرمال می‌شد تا ماشین توش کار کنه، حالا کافیه به‌قدر کافی قاعده‌مند و یادگرفتنی باشه. برنامه‌نویسی چون از قبل کامپایلر و تست و CI و کنترل نسخه داشت زودتر وارد این مرحله شد و حالا بازی داره به سمت معماری و تصمیم محصول بالا می‌ره؛ رباتیک چون دنیای فیزیکی مدام از دل بازنمایی بیرون می‌زنه، سخت‌ترین آزمون این فرضیه‌ست.
نکات کلیدی:
- AlphaProof تو ۲۰۲۴ سه تا از پنج مسئلهٔ غیرهندسهٔ المپیاد جهانی ریاضی رو داخل Lean حل کرد
- شرط بازی‌پذیری: وضعیت قابل نمایش، حرکت‌های مشخص، بازخورد تکرارشونده و یه تأییدکننده
- معماری پیشنهادی نویسنده: مولدِ باز، بازیِ نیمه‌بسته، تأییدکنندهٔ بسته
- جولای ۲۰۲۶: شین جین‌سو با دو سنگ هندیکپ مقابل KataGo دو بازی از سه بازی رو برد
- AlphaFold نشون داد یه دامنهٔ کاملاً بسته و تخصصی هم می‌تونه پر از کشف باشه
- کار تازه‌ای نیست: کشاورزی و پول هم قرن‌ها پیش محیط رو ساده و تکرارپذیر کردن
