**Tíz Claude Opus 5.5 ügynököt kértünk meg arra, hogy találjanak egy gyorsabb legrövidebb út algoritmust, és bizonyítsák azt Leanben. 15 órán belül létrehozták a C-HD-t: egy formálisan verifikált javítást a publikált korlátokon.**
A legrövidebb út problémája látszólag egyszerű: adott egy gráf csúcsokkal és (esetleg irányított) élekkel, amelyek összekötik őket, minden élhez valós súly tartozik, és egy kezdőcsúcsból minden más csúcsra meg kell találni a minimális összsúlyú utat, vagy jelezni, hogy az elérhetetlen. A vizsgált változatban a gráf irányított, pontos válaszokra van szükség, és az élek súlyai nemnegatív valós számok; a futásidőbe minden belső művelet beszámít. Ebben a felállásban a klasszikus Dijkstra-algoritmus O(m + n log n) időben fut, ahol n ≥ 2 a csúcsok, m pedig az élek száma, és ezt megfelelő prioritási sorral (például Fibonacci-kupaccal) érik el. Az m ≥ n esetre más determinisztikus algoritmusok O(m log^(2/3) n), illetve O(m √log n + √(mn log n log log n)) korlátot érnek el egy 2025-ös áttörést hozó cikk és egy 2026-os folytatás nyomán. Mivel az m és n viszonyától függő paramétertér jelentős részén a Dijkstra a jobb, a szerző arra kérte az ügynököket, hogy derítsék ki, mi lehetséges nemnegatív valós súlyok mellett, és bizonyítsák a helyességet és a hatékonyságot Leanben, a formális verifikációs eszközzel.
Körülbelül 15 óra és 733 üzenőfal-üzenet után a csapat befejezte a C-HD nevű új algoritmus javaslatát az irányított gráfokban mért pontos legrövidebb úttávolságok megtalálására, amelyet egy Lean-bizonyítás mutat be. Az algoritmus jól kezeli a lokális kereséseket, amelyek nem produktív élekkel találkoznak: továbbra is prioritás-összehasonlításokat használ, de egy újonnan elért csúcs felfedezetlen levélként beszámítható a keresés méretkorlátjába. Az algoritmus lokális invariánsokat (minden frissítés után érvényben maradó szabályokat) tart fenn gondos él-törléssel és korlátos lokális kereséssel, amivel a tanúsított tartományán belül eléri az O(n + m + m log(2 + m/(n+1)) + m^(1/3) (n log(n+2))^(2/3)) korlátot, ahol n ≥ 2 a csúcsok, m az élek száma, a tanúsított tartomány pedig m ≤ n⌊⌊log₂ n⌋^(3/4)⌋. Az elemzéshez a szerző hozzáadta a memóriafoglalás, az élek rendezése, a bemeneti gráf beolvasása és az eredmények kiírása jelentette többletköltséget is. Intuitív magyarázatként a C-HD azért ér el jobb korlátot a Dijkstránál vagy a felsorolt csúcstechnológiás algoritmusoknál a releváns rezsimekben, mert csökkenti az ismételt keresési és adatszerkezeti munkát: a forrásból és az aktuális határfelület csúcsaiból indulva korlátos lokális kereséseket futtat a kimenő élek mentén, az újonnan elért csúcsokat a keresési korlátba számítja – beleértve a felfedezetlen leveleket is, amikor egy él nem javít egy távolságbecslést –, majd a kapott keresőfákkal és pivotokkal szervezi a rekurzív munkát. Ez a determinisztikus eljárás korlátozza az ismételt munkát, és mivel az algoritmus gondosan kezeli a lokális invariánsokat, a csúcsok esetleges többszöri újralátogatása esetén is korlátos marad az ismételt feldolgozás. Az algoritmus a rendezett kimenő-éllistákra támaszkodik, amelyeket saját, elszámolt előfeldolgozása részeként állít elő, a kis bemenetek és a tanúsított sűrűségtartományon kívüli bemenetek kezelésére pedig az ügynökök egy külön Bellman–Ford algoritmust adtak hozzá O((n+1)(m+1)) futásidő-korláttal, amelyet a végrehajtás elején választ ki a rendszer; a Bellman–Ford nem a Dijkstra egy változata. A szerző bemutat egy részletet a bizonyított tételből a ténylegesen elért futásidő-céllal együtt, és a korábbi munkákkal való összehasonlításhoz megjegyzi: az m ≈ n log^(3/4) n élű gráfokon a Dijkstra korlátja O(n log n), míg a C-HD O(n log^(11/12) n)-t ér el.
Bár ez szerény javításnak tűnik, aszimptotikus értelemben jobb felső korlátot jelent, ahogy ezek a gráfok nőnek: például n = 2^1000 esetén a vezető kifejezések n log₂ n és n (log₂ n)^(11/12) aránya 1000^(1/12) ≈ 1,78 a konstansok és alacsonyabb rendű tagok elhagyásával, ami nem mért gyorsulás, hanem polilogaritmikusan skálázódó javulás – n négyzetre emelése a 2^(1/12) tényezővel szorozza az arányt. Fontos hangsúlyozni, hogy ez továbbra is csak bonyolultsági felső korlát, matematikai ígéret: lehet, hogy az algoritmus elméletileg jobb ebben a rezsimben, a gyakorlatban viszont rosszabbul teljesít. A szerző kis helyesség-szimulációkat futtatott, de a megvalósítást nagy valós gráfokon nem benchmarkolta, és mivel a formális konstrukció konstansai hatalmasak, ez nem igazol gyakorlati gyorsulást. A teljesítménykorlátot Leanben sikeresen verifikálták, és a bizonyítást a Lean Comparator eszközzel ellenőrizték: az eszköz igazolja, hogy a benyújtott bizonyítás a megadott tételt bizonyítja, csak engedélyezett axiómákat használ, és a Lean kernel elfogadja, így a formális teljesítménygarancia megfelel a kitűzött célnak. A bizonyítás azt állítja, hogy az m ≈ n log^(3/4) n profil mentén a vezető korlátkifejezések aránya (log n)^(1/12), ugyanakkor nem ad mért futásidőket vagy pontos iterációszámokat billió csúcsú gráfokra, és m = 10n esetén – más sűrűségi rezsimben – az eredmény nem igazol javulást az ott ismert legjobb korlátokhoz képest.
Ami a feladat kiadását illeti: ha az OpenAI Hugging Face-incidense és Navier–Stokes-eredménye tanított valamire, az az, hogy az ügynökök drámaian össze tudják tömöríteni a haladáshoz szükséges időt, és az együttműködés egyik egyszerű módja, ha kapnak egy csatornát egymás közti kommunikációra, azaz egy üzenőfalat. A szerző tíz maximális erőbedobással dolgozó Claude Opus 5.5 ügynököt indított el egy egyszerű üzenőfallal: kezdeti szerepeik voltak, de átszervezhették a munkájukat, megoszthatták felfedezéseiket, megkérdőjelezhették egymás ötleteit, és a legígéretesebbnek tűnő megközelítés felé csoportosíthatták az erőfeszítéseket. A viszonylag hosszú prompt pontosan leírta, mit keres: jelentős elméleti javulást a nemnegatív valós súlyú irányított gráfokon mért pontos legrövidebb utakra, teljes Lean-bizonyítással alátámasztva. Az ügynökök több irányt követhettek – logaritmikus tényezők eltávolítása, jobb kitevő keresése, lineáris idejű algoritmus keresése, vagy annak bizonyítása, hogy bármely algoritmus milyen alapvető alsó korlátot érhet el –, össze kellett vetniük eredményeiket a friss cikkekkel, rögzíteniük kellett a sikertelen megközelítéseket, hogy mások ne ismételjék meg őket, és meg kellett kérdőjelezniük egymás állításait. A siker kihirdetése előtt reprodukálható Lean-buildre és két külön szakmai bírálatra volt szükség, és ha nem sikerült javulást bizonyítaniuk, az utasítás szerint meg kellett őrizniük a részleges haladást és meg kellett mondaniuk, mi maradt nyitva. Lenyűgöző, mire képes az ügynökök egy csapata – az a jóslat, hogy „egy ország zseni egy adatközpontban”, nem járt túl messze a valóságtól. A teljes bizonyítási csomag (Lean-források, informális cikk és verifikációs jegyzőkönyvek) a github.com/spicylemonade/c-hd-proof oldalon érhető el.
Ez a cikk a Neural News AI (V1) verziójával készült.
Forrás: https://www.vals.ai/blogs/faster-shortest-path-algorithm.
A képet Johannes Plenio készítette, mely az Unsplash-on található.
