Denetleyicinin onayladığı şey

Anthropic'in ajanları 11 günde 13 milyon satır Lean kodu üretti; bu kod 30.300 ara teoremi kapsıyor ve bunların 29.500'ü Fermat'nın Son Teoremi'nin makinece denetlenen nihai kanıtına girdi. Lean'in burada verdiği güvence hem dar hem eksiksiz: her adım aksiyomlardan derleniyor, yani hiçbir inceleyicinin kodu yazan ajanlara güvenmesi gerekmiyor. Aynı biçimselleştirmeyi elle yapmak için beş yıllık hibe alan Kevin Buzzard çıktıyı 13,4 milyon satır olarak ölçtü ve matematiğin değişmediğini söylüyor.[1]

İkinci sonuç da aynı biçimde çalışıyor. NEAR Protocol'ün kurucu ortağı Alex Skidanov, projenin Lean 4 ajanının PutnamBench'teki 672 problemin tamamını 111 dolara çözdüğünü bildirdi; daha önceki tam bench koşuları 10.000 ila 25.000 dolar aralığında aktarılmıştı. PutnamBench problemlerini Lean 4'te ifade ettiği için her çözüm yine denetleyicinin kabul ya da reddettiği bir nesne oluyor ve 672 sayısı tartışmalı değil.[2]

Belgenin dışında kalan sayı

Her iki sonuç da doğrulanmış bir nesneye bir süreç sayısı iliştiriyor ve denetleyici o sayıyı hiç görmüyor. Lean adımların derlendiğini kaydediyor. Kanıtın 11 gün sürdüğünü kaydetmiyor; koşunun 111 dolara mal olduğunu da kaydetmiyor. İki sayının ağırlığı da farklı: 11 gün, otomatik biçimselleştirmenin bugün nereye ulaştığının bir tarifi olarak sunuluyor; 111 dolar ise başka sistemlerle bir karşılaştırma olarak sunuluyor, yani geçtiği her rakamın fiyatlarına, donanımına ve muhasebesine bağlı.[1], [2]

Fermat koşusu maliyetin nereye kaydığını gösteriyor. Çıktının derlenmesi Mathlib'inkinin yaklaşık 20 katı sürüyor ve yaklaşık 100 satırı ne tanım ne kanıt. Mathlib şu anda yapay zekânın ürettiği kod incelemelerini kabul etmiyor; dolayısıyla bu işi içine alacak bir kütüphanenin 13 milyon satır için insan okuyucu bulması gerekiyor. Buzzard'ın hibesi beş yıl için 1 milyon sterlin; koşu ise yaklaşık 6 milyar çıktı belirteci, ilan edilen fiyatlarla yaklaşık 300.000 dolar tüketti. Kanıtı üretmek ucuzladı, okumak ucuzlamadı.[1]

Bunu çözecek ölçüm

Maliyet iddiası için temiz bir sınama var ve bu sınama ajanın açık kaynak olmasından geliyor. NEAR dışından biri ajanı aynı 672 problemle koşturabilir; modeli, fiyatları ve başarısız denemeleri yayımlayıp ya 111 dolar civarına iner ya inmez. O olana kadar rakam, bir projenin kendi koşusuna dair kendi bildiriminin kaldığı yerde kalıyor: makul, yinelenmemiş ve başkasının hesaplamadığı 250 katlık bir oranla anılıyor.[2]

Buradaki daha eski bir yazı, bir kaçırma puanının hangi rakibi anlattığını sormuştu; çünkü puan, kendi sınama ortamını anlatıyordu. Lean örneği bu şekli tersine çeviriyor ama dersi koruyor. Burada ürün, matematikte bir şeyin doğrulanabileceği kadar eksiksiz doğrulanmış durumda ve yanına yazılan sayı yine de doğrulamanın hiç dokunmadığı bir şeyi anlatıyor. Geriye kalan iş kanıtı okumak; denetleyicinin güvencesi o işi üstlenmiyor.[1], [3]