فهرست مطالب
شرکت گوگل با توسعه سیستم چندعاملی Antigravity و استفاده از مدل‌های هوش مصنوعی Gemini، موفق شد اثبات‌های پیچیده ریاضی را بررسی کند و عملکرد نرم‌افزارها را تا ۳۰ درصد افزایش دهد.
به گزارش سرویس هوش مصنوعی تکناک، این شرکت با استفاده از چارچوب Teamwork، گروه‌هایی از عامل‌های هوش مصنوعی تخصصی را برای انجام وظایف پیچیده به کار گرفته است.
این عامل‌ها با کمک مدل‌های Gemini می‌توانند به‌صورت مستقل راه‌حل‌های مختلف را بررسی کنند، فرضیه‌ها را آزمایش کنند و درستی نتایج را بسنجند. گوگل این روش را برای کاهش خطاهای استدلالی و افزایش دقت سیستم‌های هوش مصنوعی طراحی کرده است.
یکی از مهم‌ترین دستاوردهای این پروژه، تبدیل اثبات حدس‌های ویل (Weil Conjectures) به کدهای قابل بررسی توسط کامپیوتر است. این حدس‌ها به تعداد جواب‌های معادلات چندجمله‌ای در میدان‌های متناهی مربوط می‌شوند و از دستاوردهای مهم ریاضیات مدرن به حساب می‌آیند.
سیستم Teamwork-LEAP گوگل برای رسمی‌سازی این اثبات‌ها حدود ۱.۸ میلیون خط کد به زبان Lean تولید کرده است. این فرایند با ۲۸ هزار و ۸۰۰ بار فراخوانی عامل‌های فرعی انجام شد. پیر دلین، ریاضی‌دان فرانسوی، نخستین بار در سال ۱۹۷۴ این حدس‌ها را اثبات کرده بود.
همچنین گوگل از موفقیت عامل‌های هوش مصنوعی در بازتولید نسخه رسمی یک اثبات جدید مرتبط با معادلات سه‌بعدی ناویر–استوکس خبر داده است. این معادلات رفتار سیالاتی مانند آب و هوا را توصیف می‌کنند و بررسی ویژگی‌های ریاضی آنها از مسائل دشوار علم محسوب می‌شود.
یکی از پرسش‌های اساسی درباره این معادلات، امکان ایجاد تکینگی در مدت‌زمان محدود است. ریاضی‌دانان می‌خواهند بدانند آیا جواب‌های هموار این معادلات می‌توانند در زمانی محدود به مقادیر نامتناهی برسند یا خیر.
این پرسش حدود ۹۰ سال است که بدون پاسخ قطعی باقی مانده است و با یکی از هفت مسئله جایزه هزاره ریاضیات ارتباط دارد. با وجود این، دستاورد جدید گوگل به معنای حل کامل این مسئله نیست. عامل‌های هوش مصنوعی نسخه‌ای قابل بررسی از یک اثبات مرتبط با پدیده تکینگی در زمان محدود را بازتولید کرده‌اند.
نقش عامل‌های هوش مصنوعی گوگل در اثبات‌های ریاضی
پژوهشگران گوگل از چارچوب Teamwork برای بررسی حدس کورتاد–کومار (Courtade–Kumar) نیز استفاده کرده‌اند. این مسئله در حوزه نظریه اطلاعات قرار دارد و نخستین بار در سال ۲۰۱۳ مطرح شد.
پژوهشگران گوگل با همکاری مؤسسات دانشگاهی توانستند اثباتی برای حالت کلی این حدس توسعه دهند. مدل‌های Gemini در این فرایند به استخراج کران‌های تحلیلی و تولید گواهی‌های قابل بررسی توسط کامپیوتر کمک کردند.
پژوهشگران اثبات نهایی را با زبان Lean 4 رسمی‌سازی کردند. این زبان علاوه بر قابلیت‌های برنامه‌نویسی، ابزارهایی برای بررسی خودکار درستی استدلال‌های ریاضی در اختیار کاربران قرار می‌دهد.
روش گوگل برخلاف رویکردهای متکی بر یک مدل هوش مصنوعی، از چندین عامل تخصصی استفاده می‌کند. هر عامل مسئول انجام وظیفه مشخصی است و می‌تواند بدون وابستگی مستقیم به سایر عامل‌ها، راه‌حل‌های احتمالی را بررسی کند.
گروه دیگری از عامل‌ها نیز نقش منتقد و حسابرس مستقل را بر عهده دارند. این عامل‌ها نتایج تولیدشده را بدون اتکا به استدلال اولیه مورد بررسی قرار می‌دهند و به شناسایی خطاهای احتمالی کمک می‌کنند.
همچنین گوگل دسترسی هر عامل را به فایل‌ها و ابزارهای ضروری محدود کرده است. این تقسیم وظایف باعث می‌شود عامل‌های مختلف بتوانند بخش‌های پیچیده یک مسئله را به صورت موازی بررسی کنند.
کاربرد این فناوری تنها به مسائل ریاضی محدود نمی‌شود. گوگل در پروژه دیگری از ۳۰ عامل تخصصی برای شناسایی ساختار مولکول‌های پیچیده استفاده کرده است.
این عامل‌ها با همکاری یک شبیه‌ساز مبتنی بر قوانین فیزیک، داده‌های تشدید مغناطیسی هسته‌ای (NMR) را تحلیل کردند. این روش اطلاعاتی درباره محیط اتم‌ها و ساختار مولکول‌ها در اختیار پژوهشگران قرار می‌دهد.
نتایج آزمایش‌ها نشان داد که سیستم گوگل در شناسایی ساختار صحیح مولکول‌ها به‌عنوان گزینه نخست، به دقت ۹۵ درصد دست یافته است. همچنین ساختار صحیح در تمام نمونه‌های آزمایشی میان سه گزینه پیشنهادی نخست قرار داشت و دقت سه گزینه برتر به ۱۰۰ درصد رسید.
این دستاورد توانایی عامل‌های هوش مصنوعی را در تحلیل داده‌های علمی پیچیده نشان می‌دهد. ترکیب مدل‌های زبانی با ابزارهای تخصصی محاسباتی، امکان بررسی مسائل مختلف را بدون وابستگی کامل به یک مدل فراهم می‌کند.
بازنویسی نرم‌افزارهای گوگل با Rust
گوگل علاوه بر پژوهش‌های علمی، چارچوب چندعاملی خود را برای بازنویسی و بهینه‌سازی نرم‌افزارها به کار گرفته است. یکی از مهم‌ترین پروژه‌ها، بازنویسی رمزگشای ویدیویی libgav1 AV1 از زبان ++C به Rust بود.
عامل‌های هوش مصنوعی در این پروژه حدود ۱۷۰ هزار خط کد Rust تولید کردند. نسخه بازنویسی‌شده توانست در مجموعه گسترده‌ای از آزمایش‌ها، خروجی کاملا یکسانی با نسخه اصلی ارائه دهد.
با وجود این، عملکرد اولیه نرم‌افزار رضایت‌بخش نبود. نخستین نسخه Rust تقریبا چهار برابر کندتر از برنامه اصلی اجرا می‌شد و برای استفاده عملی به بهینه‌سازی بیشتری نیاز داشت.
گوگل برای برطرف کردن این مشکل، ابزارهای تحلیل عملکرد نرم‌افزار را در اختیار عامل‌های هوش مصنوعی قرار داد. عامل‌ها با بررسی بخش‌های کند برنامه و اصلاح کدها توانستند سرعت اجرای نرم‌افزار را افزایش دهند.
در نهایت، نسخه Rust روی پردازنده‌های مبتنی بر معماری x86_64 و ARM بین ۲۰ تا ۳۰ درصد سریع‌تر از نسخه اصلی ++C اجرا شد.
گوگل در پروژه دیگری نیز کدهای باقی‌مانده ++C در ریزهسته Zircon را بازنویسی کرد. این پروژه طی دو هفته انجام شد و حدود ۸۰۰ هزار خط کد Rust تولید کرد.
نسخه جدید توانست آزمایش‌های واحد هسته را با موفقیت پشت سر بگذارد و روی سخت‌افزار ARM64 راه‌اندازی شود. استفاده از Rust اهمیت ویژه‌ای دارد، چرا که این زبان با سازوکارهای ایمنی حافظه، احتمال بروز بسیاری از خطاهای رایج برنامه‌نویسی را کاهش می‌دهد.
گوگل از عامل‌های هوش مصنوعی برای بهینه‌سازی زیرساخت‌های پردازشی داخلی خود نیز استفاده کرده است. سیستم زمان‌بندی هوشمند این شرکت توانست میزان قطع یا جابه‌جایی اجباری پردازش‌های TPU را در برخی سخت‌افزارها تا ۲۴ درصد کاهش دهد.
این بهبود بدون کاهش بهره‌برداری از خوشه‌های پردازشی یا نقض اهداف سطح خدمات به دست آمد. گوگل اکنون چارچوب Teamwork و گردش‌کار برنامه‌نویسی تکرارشونده /boost را از طریق Antigravity در اختیار کاربران قرار می‌دهد.
همچنین این شرکت ثبت‌نام را برای ارائه دسترسی رایگان به ۱۰ هزار پژوهشگر دانشگاهی آغاز کرده است. افراد پذیرفته‌شده می‌توانند به مدت شش ماه از بالاترین سطح دسترسی این سیستم از نظر میزان استفاده بهره‌مند شوند.
گوگل اعلام کرده است که در آینده ابزارهای تخصصی بیشتری، از جمله قابلیت‌های مربوط به اثبات رسمی قضایای ریاضی به سیستم چندعاملی Antigravity اضافه خواهد کرد.
