Google /teamwork: 1,8 Milyon Satır Lean ile İspat

Google Research, Antigravity platformundaki /teamwork çok ajanlı sisteminin matematik, kimya, sistem yazılımı ve makine öğrenmesi mühendisliğinde açık problemlere uygulanmasından çıkan sonuçları yayımladı. Google Fellow ve Araştırma Başkan Yardımcısı Vahab Mirrokni imzalı yazıya göre çalışmalar Gemini 4 Argon, Carbon ve Hydrogen modelleri üzerinde yürütüldü ve tamamı insan uzmanlarla birlikte yapıldı. Google, bu araçları Antigravity'deki /teamwork üzerinden dış kullanıcılara da açtığını duyurdu.

Tasarımın çıkış noktası: modelin iki zayıflığı

Sistem, mevcut dil modellerinin iki sınırı üzerine kurulmuş. Birincisi, üretimin öngörülemez olması: tek bir denemeyle doğru cevaba ulaşma arasındaki mesafe açılıyor. /teamwork bunu paralel keşif ve adanmış doğrulayıcılarla kapatıyor — Lean 4 ispat denetleyicisi, değiştirilmemiş yazılım test paketleri, yürütme simülatörleri, web araması veya donanım sayaçları. İkincisi, uzun görevlerde bağlam büyüdükçe modellerin ayrıntıyı kaçırması. Çözüm, bağlamı tasarım gereği bölmek: her uzman ajan yalnızca o adım için gereken dosya ve araçları alıyor; koordinatörler görevi yeni haleflere devrediyor; eleştirmen ve denetçiler sonucu, üreticinin akıl yürütmesini görmeden temiz bağlamdan kontrol ediyor.

Weil sanıları: 1,8 milyon satır Lean

Yazının en çarpıcı sonucu, sonlu cisimler üzerindeki polinom denklemlerinin çözüm sayılarını sayan Weil sanılarının uçtan uca, makine tarafından denetlenmiş formalizasyonu. Pierre Deligne'in 1974'te tamamladığı ispatın formalizasyonu yaklaşık 1,8 milyon satır Lean koduna ve 28 bin 800 alt ajan çağrısına ulaştı. İş, Google Cloud AI ekibiyle geliştirilen LEAP adlı çok ajanlı çerçeve ile Argon modeli eşleştirilerek tamamen otonom biçimde üretildi.

Aynı hat, Hilbert'in onuncu problemi üzerine genel tamlık halkaları için yapılmış yeni bir ispatın ilk formalizasyonunu da üretti: 919 binden fazla satır Lean. Google, 2013 tarihli Courtade-Kumar sanısının tam genellikte ispatlandığını ve Lean 4 formalizasyonunun 50 milyon satıra ulaştığını da belirtiyor. Ek olarak 2014'ten beri açık olan uyarlanabilir veri analizi ve kuantum sorgu karmaşıklığı boşlukları, STOC 2024'ün ana açık sorusu ve Navier-Stokes patlama sonucunun yeniden üretimi listede.

Matematik dışı sonuçlar

Kimya: 30 uzman ajandan oluşan ekip, fizik tabanlı bir simülatörle nükleer manyetik rezonans (NMR) verisinden moleküler yapıları belirledi. Karmaşık referans moleküllerde ilk sırada %95, ilk üçte %100 isabet bildirildi.
Sistem yazılımı: Google'ın AV1 kod çözücüsünün Rust portu, özgün C++ sürümünden %20-30 daha hızlı çıktı.
Bilimsel hakemlik: Deep Review aracı, STOC 2027'ye gönderilen 578 bildirinin yazarlarından geri bildirim izni aldı; sürmekte olan ankette (70 katılımcı) katılımcıların %90'ı geri bildirimin büyük ölçüde veya neredeyse tamamen olgusal olduğunu söyledi.

İspat neden Lean'e giriyor?

Bilgisayar destekli bir el yazmasını elle kontrol etmek hakemler için ağır bir yük; ince hatalar uzun hesapların içinde saklanabiliyor. Lean 4 ile formalize etmek, ispatı satır satır bir çekirdeğin denetlediği koda dönüştürüyor. İnsan matematikçiler formal teoremin orijinal problemle eşleştiğini onayladıktan sonra, ispat yalnızca her mantık adımı tutarlıysa derleniyor. Bu, güvenilirliği modelin itibarına değil makine denetimine bağlayan tek yöntem.

Sınırlar ve dikkat edilmesi gerekenler

Sonuçlar Google'ın kendi yayını; yani birinci taraf verisi. En güçlü kanıt Lean 4'te makine denetimi olsa da yazı, sonuçların hakem değerlendirmesinden geçtiğini veya yayına kabul edildiğini söylemiyor; yazarların çıktıları doğrulayıp sadeleştirerek yayına hazırladığı belirtiliyor. Birkaç madde yeni bir ispat değil, mevcut bir ispatın yeniden üretimi ya da formalizasyonu. Ayrıca 50 milyon satır gibi rakamlar ortaya çıkan artefaktın büyüklüğünü gösteriyor, fikrin derinliğini değil.

Yine de pratik bir eşik geçilmiş durumda: Çok ajanlı düzenekler, otomatik doğrulama araçlarıyla birleştiğinde araştırma düzeyinde iş üretebiliyor. /teamwork şu anda Antigravity'de ücretli planlarda kullanılabiliyor; Deep Review haftada iki ücretsiz çağrı veriyor, araştırmacı erişim programı için ayrı başvuru formu açıldı.