غوغل تستخدم وكلاء الذكاء الاصطناعي لحل مسائل رياضية استعصت لأكثر من عقد

خبر:

أعلنت غوغل حلّ مسائل مفتوحة في نظرية المعلومات والجبر الخطي والكيمياء الجزيئية عبر أنظمة وكلاء متعددة تعمل على نماذج Gemini 4. ووفق مدونة الشركة التي كتبها فهاب ميروكني، نائب الرئيس في غوغل ريسيرش، جرى العمل كله بالتشارك مع خبراء بشريين وجامعات شريكة. وقالت غوغل إنها تتيح هذه الأدوات للباحثين والمطورين عبر منصة Antigravity.

تفصيل:

• آلية العمل: بحسب غوغل، يعتمد /teamwork على استكشاف متوازٍ مقترن بأدوات تحقق مستقلة مثل مدقق البراهين Lean 4 ومجموعات الاختبار البرمجية وعدّادات العتاد. ويُقسَّم السياق بحيث يتسلّم كل وكيل متخصص الأدوات اللازمة لخطوته فقط، مع وكلاء نقد يفحصون النتائج من سياق نظيف.
• حدسية كورتاد-كومار: قالت الشركة إن باحثين من غوغل والجامعة الصينية في هونغ كونغ وجامعتي جنوب كاليفورنيا وكارنيغي ميلون أثبتوا حدسية طُرحت عام 2013 في نظرية المعلومات، بعد تحويلها إلى مسألة تحسين بـ14 متغيراً، ثم صياغة البرهان كاملاً في Lean 4 بـ50 مليون سطر برمجي.
• حدسيات فايل: ذكرت غوغل أن إطار LEAP أنتج ذاتياً صياغة شكلية مدقّقة آلياً لحدسيات فايل، تمتد على نحو 1.8 مليون سطر Lean عبر 28,800 استدعاء لوكلاء فرعيين. وأضافت أن النظام ولّد أكثر من 919 ألف سطر لبرهان حديث لمسألة هيلبرت العاشرة على حلقات أعداد صحيحة عامة.
• مسائل قديمة: وفق المدونة، أنجز النظام أول صياغة شكلية لحدسية بيركهوف المفتوحة منذ 1927، ولحدسية بوخنر-ريس ثلاثية الأبعاد المفتوحة منذ أكثر من 50 عاماً، مع رصد ثغرة في برهان غير رسمي حديث وإصلاحها. كما أعاد إنتاج صياغة لبرهان انفجار منتهٍ زمنياً لمعادلات نافييه-ستوكس.
• خوارزميات جديدة: قالت غوغل إن خوارزمية حتمية جديدة حسمت السؤال المفتوح الرئيسي في مؤتمر STOC 2024 حول ضرب المصفوفات البوليانية، بعد خمسين عاماً من مكاسب لوغاريتمية فقط. وأضافت أن النماذج حسمت سؤالاً مفتوحاً منذ 2014 في الحوسبة الكمومية بشأن دوال تحتاج أكثر من n/2 استعلام.
• الكيمياء: بحسب الشركة، نُظّم 30 وكيلاً متخصصاً في حلقة ذاتية التصحيح مع محاكي طيفي لتحديد بنية الجزيئات من بيانات الرنين النووي المغناطيسي، وبلغت الدقة 95% في المطابقة الأولى و100% ضمن أفضل ثلاثة خيارات، أي نحو ضعف أداء الوكيل المفرد.
• مراجعة الأبحاث: ذكرت غوغل أن مؤلفي 578 بحثاً مقدماً إلى STOC 2027، أي أكثر من ثلث المشاركات، اختاروا تلقي تغذية راجعة من أداة Deep Review. وفي استطلاع جارٍ شمل 70 مؤلفاً، قال 90% إن الملاحظات واقعية في معظمها، وأفاد أكثر من 30% بأنها رصدت أخطاء جوهرية في البراهين.
• معيار السببية: وفق المدونة، عمل 29 وكيلاً على نموذج أرغون مدة 11.5 ساعة لتحويل 13 جدول بيانات عامة إلى معيار اختبار يضم 50 مهمة في الاستدلال السببي، انطلاقاً من خمسة معايير قبول بشرية، فيما رفض وكلاء المراجعة نصوصاً مهلوسة وحوّلوا كل حالة إلى اختبار دائم.
• الإتاحة: قالت غوغل إن الأنماط متاحة اليوم داخل Antigravity إلى جانب وكيل /boost، مع منح المستخدمين مكالمتين أسبوعياً مجاناً لأداة Deep Review. ولم تحدد الشركة جدولاً زمنياً دقيقاً لإتاحة بقية الخصائص، مكتفية بالإشارة إلى تحديثات خلال الأسابيع المقبلة.

خلفية:

Antigravity منصة غوغل للوكلاء البرمجيين، و/teamwork نمط عمل يوزّع المهمة على وكلاء متخصصين يتبادلون التحقق. أما Lean 4 فلغة برهان شكلي يفحص فيها نواة حاسوبية كل خطوة منطقية سطراً بسطر، فلا يُجمَّع البرهان إلا إذا صحّت كل خطواته.

بين السطور:

تقدّم غوغل أدوات التحقق المستقلة، من مدقق Lean 4 إلى وكلاء النقد والتدقيق، بوصفها جوهر التصميم لا إضافة عليه، وهو ما يرتبط بإقرارها بأن توليد النماذج غير قابل للتنبؤ وأن انتباهها يتشتت في المهام الممتدة لأيام. والأرقام المعلنة، من 50 مليون سطر في برهان واحد إلى 28,800 استدعاء لوكلاء فرعيين، تشير إلى أن الكلفة الحسابية لهذه النتائج مرتفعة.

ماذا بعد؟

الإعلان عن بقية خصائص /teamwork للمستخدمين الخارجيين خلال الأسابيع المقبلة، ونتائج استطلاع مؤلفي STOC 2027 بعد اكتماله، ومراجعة الأوساط الأكاديمية للبراهين المصاغة في Lean 4 قبل النشر.