Google, Antigravity'nin çok agent'lı /teamwork özelliğinden yeni sonuçlar paylaştı: Weil conjectures'ın Lean formalizasyonu ve 800 bin satırlık Rust çekirdek yeniden yazımı iddiası

Google Research, geliştirici ortamı Antigravity'deki /teamwork adlı çok agent'lı iş akışı özelliğiyle elde edildiğini söylediği yeni sonuçları 13 Kasım tarihli blog yazısında paylaştı. Yazıya göre Google ekipleri ve akademik ortaklar, Gemini 4 Argon, Carbon ve Hydrogen modelleriyle matematik, kimya, dağıtık sistemler ve ML mühendisliğinde yıllardır açık kalan problemler üzerinde çalıştı. Aşağıdaki sonuçların tamamı Google'ın kendi açıklamasıdır; bağımsız olarak doğrulanmadı.

/teamwork nasıl çalışıyor?

Google, tasarımın iki sorunu hedeflediğini anlatıyor. Birincisi, modelin tek denemede doğru sonuca ulaşamaması: sistem birden çok adayı paralel üretiyor ve bunları Lean 4 proof checker, değiştirilmemiş test paketleri, simülatörler veya donanım sayaçları gibi bağımsız "çürütücülerle" eliyor. İkincisi, günlerce süren işlerde context büyüdükçe ayrıntıların kaybolması: her uzman agent yalnızca o adım için gereken dosya ve araçları alıyor, eleştirmen ve denetçi agent'lar sonucu üreticinin akıl yürütmesini görmeden temiz bir context'te kontrol ediyor.

Günlük kodlama için bu yaklaşım /boost komutu olarak paketlenmiş durumda.

Google'ın öne çıkardığı sonuçlar

• Weil conjectures: Google'a göre /teamwork-LEAP, Deligne'in 1974'teki ispatıyla tamamlanan sonuçların uçtan uca makine kontrollü formalizasyonunu yaklaşık 1,8 milyon satır Lean ile, 28.800 alt agent çağrısında üretti.
• Courtade–Kumar varsayımı: Google, CUHK, USC ve CMU araştırmacılarının 2013 tarihli bu bilgi kuramı varsayımını tam genellikte ispatladığını ve ispatın 50 milyon satır Lean koduna dönüştürüldüğünü söylüyor.
• Rust yeniden yazımı: İki haftalık bir çalışmada Zircon mikroçekirdeğinin kalan C++ kodunun yaklaşık 800.000 satır güvenli Rust'a çevrildiği, tüm çekirdek birim testlerini geçtiği ve arm64 donanımda açıldığı belirtiliyor. AV1 kod çözücü libgav1'in Rust sürümünün ise optimizasyon sonrası orijinalden yüzde 20–30 hızlı olduğu iddia ediliyor.
• Deep Review: STOC 2027'ye gönderilen 578 bildirinin yazarları taslakları için geri bildirim almayı seçti; 70 kişilik ankette katılımcıların yüzde 90'ı geri bildirimi büyük ölçüde doğru bulduğunu söyledi.

Neden önemli?

Duyuru, AI agent'larında tartışmanın "daha büyük model"den "işi doğrulayan düzenek"e kaydığını gösteriyor. Google'ın vurguladığı nokta modelin kendisi değil; adayları otomatik eleyen test, ispat denetleyicisi ve ayrı context'te çalışan denetçi agent'lar. Bu, doğrulanabilir çıktı üreten işlerde (ispat, test paketi olan kod) güçlü, doğrulama aracı olmayan işlerde ise sınırlı bir yöntem.

Kimin işine yarar / ne yapabilirsiniz?

1. Araştırmacılar: Google, 10.000 akademik araştırmacıya en yüksek kullanım katmanına altı ay ücretsiz erişim için başvuru açtı; Deep Review'da haftada iki ücretsiz çağrı sunuluyor.
2. Geliştiriciler: /teamwork ve /boost Antigravity'de bugün kullanılabiliyor; formal proof deseni ve kod yeniden yazım deseni "yakında" olarak duyuruldu.
3. Güvenlik ve platform ekipleri: Bellek güvenli dile otomatik geçiş iddiaları cazip, ancak üretime almadan önce değiştirilmemiş test paketiyle doğrulama, kod incelemesi ve agent'ın erişebildiği dosya/araç kapsamının sınırlanması şart.