هوش مصنوعی گوگل برای حل یک مسئله ریاضی 90 ساله رفت

گوگل با توسعه سیستم چند عاملی Antigravity و استفاده از مدل‌های هوش مصنوعی Gemini، موفق شد اثبات‌های پیچیده ریاضی را بررسی کند و عملکرد نرم‌افزار را تا 30 درصد افزایش دهد.

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

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

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

سیستم Teamwork-LEAP گوگل حدود 1.8 میلیون خط کد را به زبان Lean برای رسمی کردن این اثبات ها تولید کرده است. این فرآیند با 28 هزار و 800 تماس فرعی انجام شد. پیر دلن، ریاضیدان فرانسوی، اولین بار این حدس ها را در سال 1974 اثبات کرد.

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

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

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

مطالب مرتبط: این مدل هوش مصنوعی راه حل هایی برای 10 مسئله حل نشده ریاضی ارائه کرد

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

محققان گوگل همچنین از چارچوب کار تیمی برای بررسی حدس کورتاد-کومار استفاده کرده اند. این موضوع در حوزه تئوری اطلاعات است و برای اولین بار در سال 1392 مطرح شد.

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

محققان اثبات نهایی را با زبان Lean 4 رسمی کردند. این زبان علاوه بر قابلیت های برنامه نویسی، ابزارهایی را در اختیار کاربران قرار می دهد تا به طور خودکار صحت آرگومان های ریاضی را بررسی کنند.

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

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

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

کاربرد این فناوری تنها به مسائل ریاضی محدود نمی شود. در پروژه دیگری، گوگل از 30 عامل تخصصی برای شناسایی ساختار مولکول های پیچیده استفاده کرده است.

این عوامل داده‌های تشدید مغناطیسی هسته‌ای (NMR) را با همکاری یک شبیه‌ساز بر اساس قوانین فیزیک تجزیه و تحلیل کردند. این روش اطلاعاتی در مورد محیط اتم ها و ساختار مولکول ها در اختیار محققان قرار می دهد.

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

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

مرتبط: ریاضیدان استرالیایی مسئله جبر 200 ساله را حل کرد

بازنویسی نرم افزار گوگل با Rust

علاوه بر تحقیقات علمی، گوگل از چارچوب چند عاملی خود برای بازنویسی و بهینه سازی نرم افزار استفاده کرده است. یکی از مهمترین پروژه ها بازنویسی رسیور ویدئویی libgav1 AV1 از C++ به Rust بود.

عوامل هوش مصنوعی در این پروژه حدود 170000 خط کد Rust تولید کردند. نسخه بازنویسی شده توانست دقیقا همان خروجی نسخه اصلی را در مجموعه وسیعی از تست ها ارائه دهد.

با این حال، عملکرد اولیه نرم افزار رضایت بخش نبود. نسخه اول Rust تقریبا چهار برابر کندتر از برنامه اصلی اجرا شد و برای استفاده عملی به بهینه سازی بیشتری نیاز داشت.

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

در نهایت، نسخه Rust بین 20 تا 30 درصد سریعتر از نسخه C++ اصلی روی پردازنده های x86_64 و مبتنی بر ARM اجرا شد.

در پروژه دیگری، گوگل کد C++ باقیمانده را در میکروکرنل زیرکون بازنویسی کرد. این پروژه طی دو هفته تکمیل شد و حدود 800000 خط کد Rust تولید کرد.

نسخه جدید توانست تست های واحد هسته را با موفقیت پشت سر بگذارد و بر روی سخت افزار ARM64 اجرا شود. استفاده از Rust اهمیت ویژه ای دارد زیرا این زبان با مکانیسم های ایمنی حافظه خود احتمال بسیاری از خطاهای برنامه نویسی رایج را کاهش می دهد.

گوگل همچنین از عوامل هوش مصنوعی برای بهینه سازی زیرساخت پردازش داخلی خود استفاده کرده است. سیستم برنامه ریزی هوشمند این شرکت توانست میزان وقفه یا جابجایی اجباری فرآیندهای TPU در برخی از سخت افزارها را تا 24 درصد کاهش دهد.

این بهبود بدون کاهش استفاده از خوشه های پردازش یا نقض اهداف سطح خدمات به دست آمد. Google اکنون چارچوب کار تیمی و گردش کار برنامه نویسی تکراری / تقویت را از طریق Antigravity فراهم می کند.

این شرکت همچنین برای دسترسی رایگان 10000 محقق دانشگاهی، ثبت نام را آغاز کرده است. افراد پذیرفته شده می توانند به مدت شش ماه از بالاترین سطح دسترسی این سامانه از نظر کاربری بهره مند شوند.

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

مطالب مرتبط: شرکت OpenAI دوباره جامعه ریاضی را شگفت زده کرد