Nestandardní pojmosloví je nejlevnější detektor toho, že agent ujel
Pět týdnů práce na částečný úvazek, zhruba 40 miliard tokenů a asi 40 tisíc dolarů v API cenách skončilo důkazem jedné Conwayovy domněnky. Použitelných z toho bylo deset až patnáct procent. Zbytek nebyl špatný výpočet, byla to plynulá rétorika, která přestala odkazovat na cokoli skutečného.
Zajímavé není, že model umí matematiku. Zajímavé je, podle čeho autor poznal, kdy ji umět přestal.
Model si vyrobí vlastní pojmy a schová do nich odchylku
První pokusy vypadaly sebevědomě a byly nesmyslné. Výstup měl strukturu důkazu, ale operoval s termíny, které model zavedl sám a nikde je nedefinoval proti existující literatuře.
To není kosmetika. Dokud agent mluví standardním jazykem oboru, každé tvrzení se dá porovnat s něčím vnějším. Jakmile si zavede vlastní názvosloví, ztratíš referenční bod a odchylka se stane nezjistitelnou. Text zůstane vnitřně konzistentní, protože si model konzistenci definuje sám.
Léčba byla mechanická: vyškrtat každý nestandardní pojem a vynutit slovník z publikovaných prací. Po tom kroku začalo být vidět, která tvrzení nejdou napasovat na nic existujícího. To jsou přesně ta, která byla vymyšlená.
Ověřovač, kterého nelze přemluvit
Druhá pojistka byla formalizace v Leanu, která běžela souběžně s matematickými agenty. Ti drželi mírný náskok, formalizace zavírala mezery během hodin.
Ten timing je podstatný. Kdyby formalizace zaostala víc, agenti by stihli postavit celé patro na prohnilém základu. Kdyby běžela příliš těsně, práce by se zastavila na každém detailu. Cílem není ověřit všechno, ale držet vzdálenost mezi tvrzením a jeho ověřením tak krátkou, aby se nevyplatilo na neověřeném stavět.
Formalizace existující matematiky přitom běžela odděleně od formalizace nových výsledků. Jinak by si jedno vlákno tahalo kontext z druhého a ověřovač by začal potvrzovat to, co sám předtím napsal.
Co model nevidí, to neoptimalizuje
Poslední krok byl prořez. Z nasbírané práce šlo pryč zhruba osmdesát pět procent a zbytek se zjednodušoval.
Zjednodušení fungovalo teprve tehdy, když model dostal graf závislostí důkazu jako explicitní artefakt, ne jako něco, co si má odvodit ze stovek stránek textu. Sám ze sebe strukturu nevyčte. Model optimalizuje jen to, co má před očima jako data.
Totéž platí pro jakoukoli velkou refaktorizaci vedenou agentem. Pokud po něm chceš, aby zkrátil cestu, musíš mu tu cestu nejdřív nakreslit. Jinak zkrátí to, co má zrovna v okně.
Co si z toho odnést
Drift agenta nepoznáš podle tónu ani podle sebejistoty, ty zůstávají konstantní. Poznáš ho podle slovníku. V okamžiku, kdy začne používat pojmy, které jsi mu nedal a nejsou v oboru zavedené, přestal se odkazovat ven a začal se odkazovat na sebe.
Z toho plyne levná praxe pro dlouhé běhy: vynuť standardní názvosloví a periodicky kontroluj, jestli se v textu neobjevily nové termíny. Je to gramatická kontrola, ne sémantická, a odchytí většinu případů dřív, než se na nich postaví další práce.
A druhá věc, dražší, ale nezbytná: mezi agenta a výstup patří ověřovač, který se nedá přesvědčit argumentem. Lean, typový systém, konformanční testy, cokoli, co buď projde, nebo neprojde. Bez něj je pět týdnů práce jen pět týdnů plynulého textu.