سیستم چندعاملی گوگل، اثبات‌های ریاضی برجسته را به‌صورت رسمی صورت‌بندی و نرم‌افزارها را بهینه‌سازی می‌کند.

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

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

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

گوگل اعلام کرد این سامانه همچنین توانسته صورت‌بندی رسمیِ یک اثبات جدید درباره انفجار در زمان متناهی (Finite-Time Blowup) در معادلات ناویر–استوکس سه‌بعدی را بازتولید کند که این مسئله‌ا با یکی از هفت مسئلهٔ جایزه هزاره ارتباط دارد.

این پرسش که آیا جواب‌های هموار (بدون ناپیوستگی و تکینگی) این معادلات ممکن است در مدت‌زمانی محدود دچار تکینگی شوند، حدود ۹۰ سال است که همچنان حل‌نشده باقی مانده است.

سیستم مذکور همچنین به پژوهشگران کمک کرد تا به مسئله حدس کورتاد–کومار (Courtade–Kumar Conjecture) بپردازند که در حوزه نظریه اطلاعات که نخستین بار در سال ۲۰۱۳ مطرح شد.

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

پژوهشگران این اثبات را با استفاده از Lean ۴ صورت‌بندی رسمی کردند. Lean ۴ زبان برنامه‌نویسی و دستیار اثبات است که به رایانه امکان می‌دهد استدلال‌های ریاضی را بررسی و صحت آن‌ها را تأیید کند.

روش گوگل مبنی بر چند عامل است که به طور موازی کار می کنند و سیستم های جداگانه برای به چالش کشیدن و تایید راه حل های پیشنهادی تعیین شده اند. هدف از این کار کاهش اشتباهات یک مدل در زمان تولید زنجیره ای طولانی از استدلالات است.

هر عامل مخصوص فقط فایل ها و ابزارهایی را دریافت می کند که برای فعالیت مذکور مورد نیاز است. منتقدان و بازبین های مستقل نیز نتایج را بدون اتکا به استدلال اولیه عامل بررسی می کنند.