Yapay zeka ajanları, Dijkstra'dan daha sıkı bir sınırla Lean ile doğrulanmış en kısa yol algoritması teslim etti

Vals AI'nin Hacker News ana sayfasında dolaşan bir blog yazısına göre, on otonom yapay zeka ajanından oluşan bir ekip, yeni bir kesin en kısa yol algoritması ve çalışma süresinin makineyle doğrulanmış bir kanıtı üretti. C-HD adlı algoritma, yönlendirilmiş grafiklerde belirli bir yoğunluk aralığında Dijkstra'nın klasik yönteminin asimptotik en kötü durum sınırını iyileştiriyor. Vals AI sonucun sınırları konusunda açık sözlü: kazanım tamamen teorik ve gerçek dünyada bir hızlanma gösterilmemiş durumda.

Ortam ve yeni sınır

Problem, kenarları negatif olmayan gerçek ağırlıklı, kesin cevap gerektiren yönlendirilmiş bir graf üzerinde tek kaynaktan en kısa yolların bulunması. Fibonacci heap gibi bir priority queue ile eşleştirilen Dijkstra algoritması bunu O(m + n log n) sürede çözer; burada n tepe sayısını, m kenar sayısını gösterir.

Vals AI, m ≥ n için iki güncel deterministik sonuca dikkat çekiyor: 2025 tarihli bir makaleden O(m log^(2/3) n) algoritması ve 2026'da yayımlanan O(m√log n + √(mn log n log log n)) takibi. Bu sınırlar arasında, yoğunluk tayfının geniş bir bölümü — görece seyrek grafikler — Dijkstra'nın hâlâ kazandığı bölge. C-HD'nin hedeflediği boşluk tam da bu.

Yaklaşık m ≤ n(log₂ n)^(3/4) olan sertifikalı aralığında C-HD şu sonuca ulaşıyor:

O(n + m + m log(2 + m/(n+1)) + m^(1/3)(n log(n+2))^(2/3))

Vals AI'ye göre bu hesap, bellek tahsisi, kenarların sıralanması, girdi grafiğinin okunması ve çıktının yazılmasını da kapsıyor. m ≈ n log^(3/4) n profili boyunca Dijkstra'nın sınırı O(n log n) iken C-HD'ninki O(n log^(11/12) n)'e indirgeniyor — grafikler büyüdükçe daha küçük bir asimptotik tavan.

Algoritma nasıl çalışıyor

C-HD deterministik ve kaynak ile güncel tepe sınırından (frontier) başlatılan sınırlı yerel aramalar etrafında kurulmuş. Yeni karşılaşılan tepeler bir aramanın boyut bütçesinden düşülüyor ve bir mesafe tahminini iyileştirmeyen bir kenar da bütçeye keşfedilmemiş bir yaprak olarak ekleniyor. Algoritma güncellemeler arasında yerel değişmezleri koruyor, kenarları özenle siliyor ve elde edilen arama ağaçları ile pivotları özyinelemeyi yapılandırmak için kullanıyor; bu da aynı tepelerin yeniden ziyaretlerini sınırlı tutuyor. Kendi inşa ettiği sıralı giden-kenar listelerine dayanıyor ve bu ön işleme kendi çalışma süresine yazılıyor.

Sertifikalı yoğunluk aralığının dışındaki girdiler ile küçük girdiler, yürütmenin başında seçilen, O((n+1)(m+1)) sınırlı düz bir Bellman–Ford uygulamasına yönlendiriliyor. Vals AI, bu geri dönüş yolunun bir Dijkstra varyantı olmadığını belirtiyor.

Aslında ne kanıtlandı

Sonuç bir karmaşıklık üst sınırı — en kötü durum büyümesi hakkında matematiksel bir söz — bir benchmark değil. Vals AI iyileşmenin ölçeğini şöyle örnekliyor: n = 2^1000'de baş terimler n log₂ n ve n(log₂ n)^(11/12) arasında 1000^(1/12) ≈ 1.78'lik bir fark var ve bu çarpan yalnızca polilogaritmik büyüyor; n'yi karelemek onu 2^(1/12) ile çarpıyor.

Yazar küçük doğruluk simülasyonları çalıştırmış ama uygulamayı büyük gerçek grafiklerde benchmark'lamamış ve biçimsel kanıta gömülü sabitlerin devasa olduğunu belirterek pratik bir hızlanmanın ortaya konmadığını söylüyor. m = 10n gibi daha yoğun grafiklerde sonuç, bilinen en iyi sınırlara göre hiçbir iyileşme iddiasında bulunmuyor.

Performans iddiası Lean'de biçimlendirildi ve Lean Comparator aracıyla doğrulandı; bu araç, gönderilen kanıtın belirtilen teoremi kurduğunu, yalnızca izin verilen aksiyomlara dayandığını ve Lean'in çekirdek kontrollerinden geçtiğini teyit ediyor.

Ajan üretimi bir sonuç

Algoritma, yapay zeka araştırma ajanlarını orkestre etme deneyinden doğdu. Vals AI, on Claude Opus 5.5 ajanını maksimum efor ayarında başlattı ve onlara paylaşımlı bir mesaj panosu verdi. Rollere atanarak başladılar ama yeniden örgütlenme, keşiflerini paylaşma ve birbirlerinin yaklaşımlarına meydan okuma özgürlüğüne sahiplerdi. Yaklaşık 15 saat ve 733 mesaj sonra ekibin elinde önerilen bir algoritma ve hem doğruluğu hem de runtime hedefini kapsayan eksiksiz bir Lean kanıtı vardı. Orijinal prompt, negatif olmayan ağırlıklı yönlendirilmiş grafiklerde kesin en kısa yollar için biçimsel doğrulamay desteklenen, önemli bir teorik iyileştirme istiyordu.

Neden önemli

En kısa yol hesabı, yönlendirme motorlarının, ağ protokollerinin, derleyicilerin, build sistemlerinin ve lojistik yazılımlarının içinde yer alır; neredeyse her zaman Dijkstra ya da bir türevi aracılığıyla. Seyrek rejimde daha iyi bir asimptotik sınır — pratik olmayan sabitlere sahip olsa bile — genellikle daha ileri iyileştirmelerin tohumunu atan türden bir sonuçtur.

Öne çıkan iki başka açı daha var. Birincisi, iddia makineyle doğrulanmış: teslim edilen şey bir proof kernel tarafından kabul edilen bir Lean teoremi, okuyucunun sözüne güvenmesi gereken düz bir metin değil. İkincisi, bu çalışma, koordineli yapay zeka ajanlarının araştırma sürelerini çarpıcı biçimde kısaltabildiğine dair büyüyen kanıtlara ekleniyor; tipik olarak aylar süren teorik bir çabayı kabaca bir günlük ajan süresine dönüştürüyor. Vals AI'nin dürüst çerçevelendirmesi — gerçek dünya hızlanması gösterilmemiş bir asimptotik kazanım — bunu okumanın doğru yolu: doğrulanmış bir teorik ilerleme ve ajan odaklı araştırmanın nereye gittiğine dair bir veri noktası.