Compile to Compress tlačí formálne dokazovanie bližšie k lacnejšej prevádzke

Formálne dokazovanie patrí medzi oblasti, kde sa jazykovým modelom pripisuje veľký dlhodobý potenciál, ale zároveň aj vysoká cena za každý viditeľný pokrok. Najlepšie výsledky často vyžadujú rozsiahle roll-outy, dlhú históriu pokusov a veľa test-time compute, čo znižuje praktickú použiteľnosť. Práca „Compile to Compress“ preto zaujme najmä tým, že hľadá úsporu nie v novom obrovskom modeli, ale v inteligentnejšom využití spätnej väzby z kompilátora alebo verifikátora. Autori tvrdia, že veľké množstvo rôznych neúspešných dôkazových pokusov sa v skutočnosti mapuje na relatívne kompaktný súbor štruktúrovaných chybových režimov.

Práve táto „kompresia zlyhaní“ je jadrom celej metodiky. Ak verifikátor konvertuje obrovský priestor chybných postupov do menšieho počtu informatívnych signálov, dá sa tento signál využiť na lokálne opravy a efektívnejšie prehľadávanie stromu dôkazu. Namiesto toho, aby model držal v kontexte dlhú históriu predchádzajúcich pokusov, môže sa sústrediť na explicitnú spätnú väzbu o konkrétnom type chyby a na cielenú refináciu ďalšieho kroku. To je dôležité, lebo práve dlhý kontext a masívne roll-outy bývajú jedným z hlavných nákladových problémov moderného theorem proving stacku.

Autori hovoria o learning-to-refine prístupe a tree searchi, ktorý opravuje chyby lokálne podmienené verifikačnou spätnou väzbou. Prakticky to znamená zmenu filozofie: namiesto generovania obrovského množstva kandidátov a dúfania, že sa medzi nimi nájde správny, sa viac investuje do interpretácie toho, prečo kandidát zlyhal. Takýto prístup je zaujímavý aj mimo formálneho dokazovania. Podobný princíp by sa mohol uplatniť vo všetkých úlohách, kde existuje silný externý verifikátor a kde chyba nesie štruktúrovanú informáciu o tom, ako sa má model opraviť.

Výsledky sú v kontexte otvorene publikovaných modelov ambiciózne. Práca uvádza state-of-the-art výkon na PutnamBench medzi verejne reportovanými modelmi okolo 8B a 32B parametrov pri porovnateľnom test-time rozpočte. Samotné čísla budú ešte potrebovať širšie potvrdenie, no podstatnejšia je stratégia. Ak možno posilniť dôkazové schopnosti bez nekonečného navyšovania výpočtu, zlepšuje to vyhliadky na praktickejšie použitie formálneho dokazovania v softvéri, matematike aj verifikácii bezpečnostne citlivých systémov.

Pre AI priemysel je to ďalší príklad trendu, v ktorom sa výkon nezískava len väčším modelom, ale lepším spojením modelu a verifikátora. Čoraz viac zaujímavých smerov v reasoning AI sa nehrá na jednorazovú „superinteligentnú“ odpoveď, ale na iteratívnu slučku medzi generátorom a prostredím, ktoré vie dať presný feedback. Práve theorem proving je na to ideálnym laboratóriom, lebo verifikátor je nemilosrdný a jasný. Ak podobné techniky dozrejú, môžu neskôr ovplyvniť aj programovanie, plánovanie či prácu s databázami.

Zaujímavá je aj ekonomická vrstva celej témy. Veľa diskusií o reasoning modeloch dnes naráža na to, že vyššia kvalita často znamená neúmerne drahšie nasadenie. Compile to Compress ukazuje alternatívu: výkon možno posilniť aj tým, že lepšie zorganizujeme spätnú väzbu a lokálnu opravu chýb. Nie je to univerzálne riešenie pre všetky LLM úlohy, ale v doménach s formálnym verifierom ide o veľmi sľubnú cestu.

Ak sa táto línia potvrdí aj v ďalších benchmarkoch, môže posunúť theorem proving z fascinujúcej demonštrácie smerom k použiteľnejšiemu nástroju. Nie preto, že by model naraz začal „rozumieť matematike“ zázračne lepšie, ale preto, že sa zefektívni cesta od chybného pokusu k správnej oprave. A presne tam sa dnes láme praktická hodnota mnohých AI reasoning systémov.