Souhrn
Startup Harmonic AI získal 120 milionů dolarů při ocenění 1,45 miliardy dolarů na rozvoj svého AI systému Aristotle, který se specializuje na formální matematické uvažování bez tzv. halucinací – chyb, kdy model vymýšlí nepravdivé odpovědi. Systém dosáhl úrovně zlaté medaile na Mezinárodní matematické olympiádě a nyní je veřejně dostupný i přes API.
Klíčové body
- Harmonic AI vyvinula AI model Aristotle zaměřený na formální matematické důkazy pomocí systému Lean 4.
- Model využívá syntetická trénovací data generovaná autonomně, nikoli z webu, což umožňuje rekurzivní sebe-zlepšování.
- Systém dosáhl výkonu na úrovni zlaté medaile na Mezinárodní matematické olympiádě.
- Společnost získala 120 milionů dolarů při ocenění přes 1 miliardu dolarů.
- Aristotle nyní podporuje vstup v běžné angličtině a je dostupný přes API pro výzkumníky a matematiky.
Podrobnosti
Harmonic AI, založená v roce 2023 Vladem Tenevem (CEO platformy Robinhood), vyvíjí AI systém nazvaný Aristotle, který se zaměřuje na formální matematické uvažování – schopnost odvozovat matematické důkazy s důkazovou korektností ověřitelnou počítačem. Na rozdíl od běžných jazykových modelů, které často generují pravděpodobné, ale chybné odpovědi, Aristotle využívá proof assistant Lean 4, což je nástroj umožňující formální zápis definic, vět a důkazů. Klíčovou inovací je metoda trénování na synteticky generovaných párech „problém–důkaz“, které model vytváří sám v tzv. self-play smyčce. Tento přístup umožňuje modelu postupně zvyšovat složitost řešených úloh – od základních cvičení až po pokročilé věty. Aristotle nedávno dosáhl výkonu srovnatelného se zlatým medailistou Mezinárodní matematické olympiády, což je považováno za nejprestižnější soutěž pro středoškolské matematiky. Společnost nyní nabízí veřejné API, které již využívají výzkumníci k urychlení objevů v matematice.
Proč je to důležité
Tento pokrok představuje významný krok směrem k tzv. matematické superinteligenci – AI schopné přesahovat lidské schopnosti v rigorózním uvažování. Eliminace halucinací v matematickém kontextu má potenciál transformovat výzkum v teoretické informatice, kryptografii i formální verifikaci softwaru. Harmonic AI tak přispívá k větší spolehlivosti AI v kritických oblastech, kde chyba není přípustná. Zároveň ukazuje, že syntetická data a self-play trénink mohou být udržitelnější a bezpečnější alternativou ke stávajícím metodám založeným na webových datech.
Zdroj: 📰 SiliconANGLE News
|