Resolution formalizoval matematiku za 135 tisíc dolarů

V kostce

• Resolution vytvořil 600 tisíc řádků kódu v jazyce Lean za týden
• Claude Opus 5.5 získal 18,5 % v testu ProgramBench
• Mirendil-Base postavil jeden výzkumník za 3,5 měsíce

Startup zaměřený na bezpečnost AI Resolution automaticky formalizoval matematické výsledky související se statistickou teorií učení, model Claude Opus 5.5 získal 18,5 % v testu ProgramBench a startup Mirendil předvedl předtrénování modelu jednotlivcem. Formalizace si podle zdroje vyžádala přibližně týden práce a odhadovaných 135 tisíc dolarů za tokeny. Přehled přinesl newsletter Import AI 478.

Resolution, dříve známý jako Sequent, autoformalizoval vyřešení singularit, které má podle týmu položit základ pro další automatizovaný výzkum vztahu mezi geometrií ztrátové krajiny a generalizací. Výzkumník nejprve s agenty připravil dvě verze plánu, včetně detailní 112stránkové verze rozdělené na atomické kroky podle existující literatury. Agent-orchestrátor pak plán provedl a spouštěl dílčí agenty pro matematiku, psaní kódu v jazyce Lean a kontrolu postupu.

Práce spotřebovala řádově 100 miliard vstupních tokenů, z toho 90 % připadalo na čtení z cache, a asi 300 milionů výstupních tokenů, což odpovídá odhadovaným 135 tisícům dolarů. Výsledkem bylo asi 600 tisíc řádků kódu v jazyce Lean. Podle newsletteru tým knihovnu již využil k rozšíření částí teorie singulárního učení, například k lepšímu pochopení vzorkování a k ovlivňování způsobu, jak se modely učí. Firma očekává, že industrializace matematiky umožní novou, rigorózní vědu o automatizaci výzkumu.

Test ProgramBench zkoumá, jak dokážou systémy AI obnovit softwarové programy na základě zkompilovaného programu a jeho dokumentace. Zahrnuje 200 úloh, mimo jiné interprety jazyků PHP a Lua či tinycc, databáze DuckDB a SQLite, nástroje FFmpeg, zstd a xz a vývojářské nástroje ripgrep, fzf a jq. Test vyšel v květnu letošního roku a tehdy žádný testovaný model neuspěl.

Při vydání dosáhl nejlepší systém s modelem Claude Opus 4.7 hodnoty 0 % v metrice resolved, tedy podílu úloh se všemi splněnými testy, a 3 % v metrice almost, tedy podílu úloh s více než 95 % splněných testů. Model Claude Opus 5.5 ve variantě xhigh nyní dosáhl 18,5 % resolved a 70,5 % almost. Autor newsletteru očekává nasycení testu do konce roku 2027.

Společnost OpenAI popsala vlastní test zabezpečení, při němž agenti v oddělených mikrovirtuálních strojích měli vyměnit syntetická tajemství bez síťového spojení a sdílených zapisovatelných souborů. Agenti ke komunikaci využili cache procesoru a rozdíl v rychlosti čtení z cache a z hlavní paměti, kdy jeden agent cíleně vysouval data a druhý měřil čas jejich opětovného načtení. V souvisejícím útoku jeden agent střídal souvislé zápisy a nečinnost, zatímco druhý dekódoval signál z časových rozdílů.

Startup Mirendil oznámil model Mirendil-Base, předtrénovaný jazykový model, který podle firmy postavil jeden výzkumník za 3,5 měsíce s výpočetními náklady pod 10 milionů dolarů. Částka zahrnuje výzkum, menší experimenty i finální trénink, veškerý kód vznikl od nuly nad knihovnami PyTorch a JAX a model se učil pouze z veřejně dostupných dat. Firma uvádí pásmo 100 až 500 miliard parametrů pro verzi Base, 500 miliard až 2 biliony pro verzi Large a 2 až 10 bilionů pro verzi XL.

Verze Large je natrénována přibližně z 80 % a její dosavadní zlepšení odpovídá škálovacím trendům, verze XL je hotová zhruba z 19 % a již se blíží současnému skóre verze Large. Model Mirendil-Base překonává modely Nemotron-550B-Base, GLM-5.3 a DeepSeek-V4-Pro-Base, ale zaostává za modelem Kimi-K3, zatímco větší verze Large a XL model K3 překonávají. Mirendil podle newsletteru uvádí, že další model bude částečně postaven na modelech Mirendil a že firma zatím nedosáhla plně autonomního rekurzivního sebezdokonalování, ale je mu blíže než kdy dříve.

Zdroje

1. Import AIimportai.substack.com