Bağlamın gideri
İspat arayan bir eylemcinin giderini yalnızca son yanıttaki uzunluğa bakarak yönetmek zor. LEVER ön baskısında araştırmacılar, aynı DeepSeek-V4-Flash-0731 modelini kullanan ispat aramalarını karşılaştırıyor. Değerlendirme için ayrılan 80 Putnam probleminde LEVER’in çözme oranı %96,3, karşılaştırılan yöntemin oranı %80. Aynı fiyat hesabında ortalama gider 0,95 dolar ve 1,44 dolar. Denemeler 3 dolarlık bütçeyle sınırlandırılmış; başarısızlıklar bu bütçenin tamamıyla ücretlendiriliyor. Bunlar seçilmiş matematik problemlerindeki araştırma sonuçları.[1]
İlginç taraf, LEVER’in daha fazla çıktı belirteci üretirken daha az girdi belirteci tüketmesi. Araştırmacılar gideri %90 önbellek isabeti varsayımıyla yeniden fiyatlıyor ve planlama çağrılarını da hesaba katıyor. Dolayısıyla burada verim, düşünme metnini kısaltmakla eş anlamlı değil. Benim çıkarımım, tekrar tekrar taşınan geçmişin bütçede ciddi bir mimari tercih haline geldiği. Başka bir açıklama ise seçilmiş problem kümesiyle önbellek fiyatlamasının yöntemin güçlü yanlarını öne çıkarması; bu farkın her kod görevine aynı biçimde taşınması beklenemez.[1]
LEVER, ispatı alt hedeflere ayıran bir VE/VEYA grafiği kuruyor. Bir düğüm birden çok koşulun birlikte sağlanmasını ya da alternatif yollardan birinin bulunmasını temsil edebiliyor. Tamamlanmış kısmi ispatların değerleri arama sırasında kullanılıyor. Her yeni çağrı, bütün geçmiş yerine yerel üst düğümlerden gelen bağlamı görüyor. Gider azalmasını işe yarar kılan bağlantı burada: parçalama, sonraki adımlara taşınması gereken bağlamı da değiştiriyor.[1]
Parçaları kabul etmek
Bu tasarımın kullanışlı yanı, parçalara ayrılmış işin sonunda Lean tarafından denetlenebilmesi. Alt hedefleri ayrı çözmek tek başına yeterli değil; birleşmiş ispatın geçerli olması gerekiyor. Denetleyici, arama biçimini değiştirmeye alan açan somut kabul ölçütünü sağlıyor. Yazılım geliştirenler için buradaki ders, eylemciyi daha çok parçaya bölmeden önce bu parçaları yeniden birleştiren kabul koşulunu belirlemek. Matematikteki denetleyicinin yerini sıradan bir kod işinde hangi sınamaların doldurduğu, aynı ölçüde önemli bir tasarım sorusu.[1]
Yerel bağlamın da bir bedeli var: birbirinden uzak alt hedefler arasındaki bağımlılıkların doğru temsil edilmesi gerekiyor. LEVER’in grafiği ispat aramasına göre kurulmuş; bu yapıdan genel amaçlı eylemciler için otomatik bir başarı sonucu çıkarmıyorum. Dar kapsam, yöntemin değerini azaltmıyor. Aksine sabit model, belirli bütçe ve açık doğruluk denetimi, hangi mimari değişikliğin neyi etkilediğini tartışmayı kolaylaştırıyor.[1]
Benim bakacağım karşılaştırma, aynı görevlerde model ve fiyatları sabit tutup tam geçmişle yerel bağlamı ayrı çalıştırmak. Ölçülebilir gösterge olarak kabul edilen tamamlanmış iş, girdi gideri ve başarısız denemelerin bütçesi birlikte görünmeli. Bu, daha kısa yanıtı başarı saymadan, bağlam taşımanın giderini doğrudan sınayan bir yaklaşım. LEVER’in somut katkısı da burada: aynı modeli farklı bir iş bölümüyle kullanmayı ölçülebilir bir mühendislik sorusuna dönüştürüyor.[1]