تقابل عامل های هوشمند گوگل با معماهای ریاضی چندین ساله

گوگل از ارتقای چشمگیر سامانه چندعاملی «آنتی‌گراویتی» (Antigravity) خود با بهره‌گیری از مدل‌های پیشرفته جمینای ۴ (Gemini 4) پرده برداشت. این شرکت با معرفی چارچوب جدید «تیم‌ورک» (Teamwork)، رویکرد تازه‌ای را برای همکاری انسان و هوش مصنوعی بنا نهاده است که هدف آن حل پیچیده‌ترین مسائل حل‌نشده ریاضی، کشف ساختارهای نوین مولکولی و بهینه‌سازی زیرساخت‌های نرم‌افزاری است. در این معماری، به جای اتکا به یک مدل واحد، تیم‌هایی از عامل‌های هوشمند متخصص در کنار پژوهشگران انسانی قرار می‌گیرند و به‌صورت موازی، فرضیه‌ها را بررسی، مسیرهای حل را آزمایش و خروجی‌ها را با ابزارهای دقیق محاسباتی راستی‌آزمایی می‌کنند.

 

یکی از خیره‌کننده‌ترین دستاوردهای این سامانه، صورت‌بندی رسمی و ماشینی «حدس‌های ویل» (Weil Conjectures) است؛ مجموعه‌ای از قضایای بنیادی در هندسه جبری که تعداد جواب‌های معادلات چندجمله‌ای را بر روی میدان‌های متناهی بررسی می‌کند و نخستین بار در سال ۱۹۷۴ توسط ریاضی‌دان فرانسوی، پیر دولین، اثبات شده بود. سامانه Teamwork-LEAP که با همکاری بخش هوش مصنوعی ابری گوگل توسعه یافته، برای تبدیل این اثبات به زبان قابل فهم و بررسی توسط کامپیوتر، بدون دخالت مستقیم انسان حدود ۱.۸ میلیون خط کد به زبان Lean تولید کرده و در این مسیر بیش از ۲۸ هزار و ۸۰۰ بار عامل‌های فرعی را فراخوانی کرده است.

 

دامنه موفقیت‌های تیم‌ورک تنها به هندسه جبری محدود نمانده و به یکی از معروف‌ترین معماهای ۹۰ ساله ریاضی و فیزیک نیز راه یافته است. این سامانه موفق شد صورت‌بندی رسمی یک اثبات جدید پیرامون پدیده «انفجار در زمان متناهی» (Finite-Time Blowup) در معادلات سه‌بعدی ناویر–استوکس را بازتولید کند؛ معادلاتی که حرکت سیالات را توصیف می‌کنند و پاسخ به این پرسش که آیا جواب‌های هموار آن‌ها در زمانی محدود دچار تکینگی می‌شوند یا خیر، یکی از هفت مسئله «جایزه هزاره» است.

 

علاوه بر این، پژوهشگران گوگل با همکاری محققان دانشگاه‌های معتبری همچون کارنگی ملون (CMU)، کالیفرنیای جنوبی (USC) و دانشگاه چینی هنگ‌کنگ (CUHK)، از این چارچوب برای حل کامل «حدس کورتاد–کومار» (Courtade–Kumar Conjecture) در حوزه نظریه اطلاعات (مطرح‌شده در سال ۲۰۱۳) استفاده کردند. مدل‌های جمینای ۴ (از جمله نسخه تخصصی Argon) در این پروژه توانستند بدون محدود کردن مسئله به شرایط خاص، کران‌های تحلیلی را استخراج و اثبات نهایی را در قالب ۵۰ میلیون خط کد در محیط Lean 4 (دستیار اثبات خودکار که کوچک‌ترین خطای منطقی را رد می‌کند) نهایی سازند.

 

بزرگ‌ترین چالش مدل‌های زبانی در مسائل طولانی، «انحراف از زمینه» (Context Drift) و خطاهای زنجیره‌ای است. گوگل برای غلبه بر این ضعف، در معماری تیم‌ورک نوعی جداسازی ساختاری ایجاد کرده است؛ به این صورت که هر عامل تخصصی تنها به فایل‌ها و ابزارهای دقیقاً مورد نیاز برای گام خود دسترسی دارد و از اطلاعات اضافی ایزوله می‌شود. پس از تولید هر راه‌حل، عامل‌های دیگری در نقش «منتقد و حسابرس» (Critics & Auditors) وارد عمل می‌شوند؛ این ناظران مستقل بدون آنکه به روند استدلال اولیه دسترسی داشته باشند، خروجی را از صفر و در یک فضای پاک به چالش می‌کشند و صحت آن را می‌سنجند.

 

کاربرد این سیستم چندعاملی فراتر از ریاضیات محض رفته و در مهندسی سیستم‌ها نیز نتایج ملموسی به جا گذاشته است؛ برای نمونه، تیم‌های گوگل با استفاده از آن موفق به طراحی کرنل‌های سفارشی برای پردازنده‌های TPU شدند که مصرف حافظه پهنای باند بالا (HBM) را تا ۱۸۵ برابر کاهش داده و سرعت پردازش شبکه‌های عصبی گراف را تا ۱۵ برابر افزایش داده است. همچنین گوگل اعلام کرده است که در راستای تسریع پژوهش‌های علمی جهان، دسترسی رایگان به بالاترین سطح این ابزارها را به مدت ۶ ماه در اختیار ۱۰ هزار پژوهشگر دانشگاهی قرار خواهد داد.