Anthropic, Claude'nin Fermat'ın Son Teoremi'nin ilk tam形式li kanıtını tamamladığını açıkladı. Bu, teoremi yeniden keşfetmek değil, mevcut kanıtı bilgisayarın satır satır doğrulayabileceği mantıksal kodlara dönüştürmekti. Şirket, bu çalışmanın 11 gün sürdüğünü ve nihayetinde yaklaşık 13 milyon satır içerik ürettiğini belirtti.
Formel kanıtın önemi, matematiksel argümanları makine tarafından kontrol edilebilir bir dile çevirmektir. Geleneksel makale kanıtları genellikle uzun süreli eşdeğer incelemeye ihtiyaç duyar; eğer arada bir adım da hata varsa, düzeltme süreci aylar hatta yıllar sürebilir. Fermat'ın Son Teoremi, İngiliz matematikçi Andrew Wiles tarafından 1995 yılında kanıtlanmıştır, ancak bu kanıtı tamamen makine tarafından kontrol edilebilir bir versiyona dönüştürmek, yoğun bir mühendislik projesi olarak kabul edilmiştir.
11 gün içinde uzun vadeli proje hedefini tamamlayın
2024'ten itibaren Londra İmparatorluk Koleji matematikçisi Kevin Buzzard, Wiles'in kanıtını Lean kanıt yardımcı programına dönüştürmeyi hedefleyen ilgili projeyi öncülük etti. Planlanan şekilde, bu çalışma uzun vadeli iş birliği gerektirecek ve finansman 2029 yılına kadar sağlanmıştır.
Anthropic, Claude'nin bu görevde benzer hedeflere önceden ulaştığını belirtti. Buzzard, bu kanıtın ek varsayımlara gerek kalmadan, sadece matematiğin en temel aksiyom sistemine dayanarak doğrulanabileceğini onayladı.
Çoklu ajan tarafından paralel olarak tamamlanır
Anthropic'a göre, Columbia Üniversitesi araştırmacıları Tianyi Peng ekibi, birden fazla Claude aracısını paralel olarak çalıştırdı; bunlar sırasıyla tanımlar yazdı, küçük sonuçları kanıtladı ve daha büyük kanıt yapıları oluşturmak için bunları birleştirdi. İnsan müdahalesi azdı ve ana amaç, aşamalı öncelik sıralaması sağlamaktı.
İlk adımlar sorunlu geçti. Anthropic, bazı ajanların tamamlanmış içerikleri paylaşamadığını ve işleri tekrarladığını belirtti. Daha sonra, ekip, ajanlara tekil bir görev listesi ve dosya organizasyonu sağlayıp doğal dil notları bırakarak sonuçları birbirlerinden yeniden kullanmalarına yardımcı olmak için Prove2Me adlı bir araç kullandı.
- Destekleyici teorem 30.000'den fazla
- Toplam tüketim milyarlarca token'a ulaştı
- Sonunda yaklaşık 13 milyon satır doğrulandı
Doğrulanabilirliğe odaklanın, yeni teoremlere değil.
Bu başarının vurgusu, yeni bir matematiksel önerme keşfetmekten ziyade, mevcut büyük ispatları bilgisayar tarafından adım adım doğrulanabilir hale getirmektir. Matematik makaleleri ve AI tarafından üretilen içerikler arttıkça, ispatların elle tek tek kontrol edilmesi maliyeti de artmaktadır; bu nedenle formel araçlara olan ilgi artmaktadır.
Anthropic, bu kanıtın matematik topluluğunun yaygın olarak kullandığı Mathlib paylaşım kütüphanesinden beş kat daha büyük olduğunu da belirtti. Tam dosya GitHub'a yüklendi ve araştırmacılar, yapısını ve doğruluğunu satır satır incelemeye devam edebilir.