Google'ın Gemini 4 ajanları ve Antigravity /teamwork, matematik ve bilimdeki açık problemlere el atıyor

Google, şirket genelindeki ve akademik partner kurumlardaki ekiplerin Gemini 4 model ailesini — Argon, Carbon ve Hydrogen — Antigravity ortamındaki çok-ajanlı /teamwork özelliğiyle birlikte kullanarak yıllardır açık kalan araştırma problemlerinde ilerleme kaydettiğini bildiriyor. Bir Google Research blog yazısı, bilgi kuramı, biçimsel doğrulama, optimizasyon, kuantum hesaplama ve streaming algoritmalarındaki sonuçların yanı sıra, şirketin halihazırda üreimde olduğunu söylediği moleküler yapı keşifleri, çekirdek (kernel) optimizasyonu ve altyapı kazanımlarını anlatıyor.

/teamwork nasıl çalışıyor

Yazı, tasarımı mevcut dil modellerinin iki eksikliğine bağlıyor: Tek bir üretim güvenilmezdir — bir deneme ile doğru cevap arasında geniş bir uçurum bırakır — ve modeller, dikkat büyüyen bağlam pencerelerine yayıldıkça günler süren görevlerde ayrıntıyı gözden kaçırır.

/teamwork ilk sorunu, birçok adayı paralel olarak keşfedip bunları hangi cevapların gerçekten geçerli olduğuna karar veren harici yanlışlayıcılara — Lean 4 kanıt denetleyicisi, değiştirilmemiş yazılım test paketleri, yürütme simülatörleri, web araması ve donanım sayaçları — karşı doğrulayarak ele alıyor. İkinci sorunu ise bağlamı bölerek çözüyor: Her uzman ajan yalnızca adımının gerektirdiği dosya ve araçları görür, koordinatörler işi taze haleflere devreder ve eleştirmen ile denetçi ajanlar, sonuçları onları üreten ajanın akıl yürütmesinden arınmış bağlamlardan yeniden kontrol eder.

İş akışları, bildirimsel, kendini geliştiren doğal dil kalıpları olarak yazılıyor ve her prompt, dağıtık kodlamadan (ayrı olarak /boost olarak paketlenmiş yinelemeli problem çözmeye) uzun kanıt ve belge incelemesine kadar en uygun kalıba yönlendiriliyor. Google, kalan özelliklerin önümüzdeki haftalarda harici Antigravity kullanıcılarına ulaşacağını söylüyor.

Courtade–Kumar sanısının kanıtlanması

Manşet sonuç, bilgi kuramında 2013'ten beri açık olan Courtade–Kumar sanısının bir kanıtı. Google, CUHK, USC ve CMU'dan araştırmacılar, Antigravity içinde Stellar Colosseum adlı bir harness'i uygulayan Long Proof kalıbını kullandı. Sanı, rastgele bir bit dizisi gürültülü bir kanaldan geçtiğinde, girdinin tek bite sıkıştırılmasının, bir girdi bitini kopyalayan bir "diktatör fonksiyonundan" daha fazla bilgi koruyamayacağını söylüyor.

İş birliği tek seferlik değil etkileşimliydi. Yazıya göre Gemini önce, önceki bir CUHK makalesindeki sanının genelleştirilmiş bir versiyonuna karşı örnekler buldu. CUHK ekibi daha sonra problemi 14 değişkenli bir optimizasyona indirgeyen bir aday fonksiyon ve kilit bir alt sınır önerdi. Gemini 4 Argon ve önceki modeller parametre uzayını böldü, yeni analitik sınırların ve aritmetik-aralık sertifikalarının çoğunu üretti ve kanıtı, insan girdisi olmadan dengeli fonksiyonlardan dengesiz fonksiyonlara genişletti. Tam kanıt daha sonra Lean 4'te biçimlendirildi ve toplam 50 milyon satır kod oluşturdu.

Kuram genelinde sonuçlar

Diğer açık problemler doğrudan Gemini 4'e ve çok-ajanlı harness'lere soruldu; Google, insan yazarların ortaya çıkan kanıt ve algoritmaları yayım için doğruladığını, sadeleştirdiğini ve düzenlediğini söylüyor. Yazıdan öne çıkanlar:

• Uyarlanabilir veri analizi: Gemini 4 Argon çalıştıran bir harness, önceki cevaplardan uyarlanabilir olarak seçilen istatistiksel sorgular için optimal-e-yakın örneklem sınırlarını bağımsız olarak kanıtladı ve Lean ile doğruladı; 2014'ten beri açık olan bir boşluğu kapattı ve hem ekleme hem de silme içeren akışlarda uyarlanabilir rakiplere karşı doğru kalan ilk, neredeyse uzay-optimal streaming algoritmasını ortaya çıkardı.
• Kuantum hesaplama: Yeni bir yapı, sabit hata altında kesinlikle n/2'den fazla kuantum sorgusu gerektiren ilk n-bitli Boolean fonksiyonlarıyla 2014 tarihli bir soruyu çözüyor ve simetrik fonksiyonlar için kesin ek yükü belirliyor.
• Matris çarpımı: Deterministik bir algoritma, STOC 2024'ün ana açık sorusunu çözüyor; kombinatorik Boolean matris çarpımı ve üçgen tespiti için kübik zaman üzerindeki hedef hızlanmayı elde ediyor — önceki elli yılda yalnızca logaritmik kazanımlar bulunabilmişti.
• Seyrek eskizler: İstiflenmiş eskizler 2025 tarihli bir açık soruyu yanıtlıyor; bir matrisi doğrusal boyuta sıkıştırırken r boyutlu bir alt uzayın her yönünü satır başına yalnızca √log r sıfır-olmayan değerle koruyor — bu, daha önce gerekli olan log r'de karesel olarak az ve yeni bir alt sınıra neredeyse denk.
• Streaming grafikler: Stellar Colosseum, dinamik kenar-ağırlığı güncellemeleri altında ağırlıklı grafiklerin kesitleme seyreltmesi için ilk tek geçişli streaming algoritmasıyla FOCS 2022'den beri açık kalan bir soruyu yanıtlıyor ve aynı anda optimal-e-yakın bellek, güncelleme süresi ve yeniden yapılandırma süresi elde ediyor.
• Optimizasyon ve aritmetik: Çevrimiçi ters lineer optimizasyon için deterministik bir algoritma optimal regret'e ulaşırken çalışma süresini boyutta üstelden polinomiyale indiriyor; ayrı çok-ajanlı kampanyalar n-bitlik tam sayı çarpımı için Turing makinesi sınırını n log n'in altına sadeleştirdi. Bir geometri alt sınırı da, n nokta arasındaki tüm çiftler arası uzaklıkları herhangi bir sabit çarpan içinde yaklaşmanın, ekstra Steiner noktaları ve istenildiği kadar çok geçiş olsa bile polinomiyel olarak n'den fazla kenar gerektirebileceğini gösteriyor.

Neden önemli

Bu çalışmayı sıradan "yapay zeka matematik yaptı" duyurularından ayıran iki şey var. Doğrulama içsel: En güçlü iddialar Lean 4 biçimlendirmeleri veya el değmemiş test paketlerine karşı kontrollerle geliyor, dolayısıyla bir modelin çıktısına güvenmeye dayanmıyorlar. Ve mimari, ajanların gerçek başarısızlık biçimlerini — güvenilmez tek üretimler ve uzun ufuklarda bağlam bozulması — paralel keşif ve katı bağlam izolasyonuyla hedefliyor.

Araçlar harici araştırmacılar eline geçtiğinde sağlam çıkarsa, kuramsal çalışmanın bazı bölümlerinde darboğaz aday argümanlar üretmekten problem çerçeveleme ve biçimlendirmeleri inceleme tarafına kayabilir. Sonuçlar Google tarafından kendi beyanıyla sunuluyor; gerçek test, yayımlanan makalelerin bağımsız incelemesi olacak.