Souhrn
Startup Harmonic AI získal 120 milionů dolarů při ocenění 1,45 miliardy dolarů na vývoj pokročilého modelu umělé inteligence zaměřeného na formální matematické uvažování. Jeho systém Aristotle dokáže převádět matematické úlohy z běžného jazyka do formálně ověřitelných důkazů a nedávno dosáhl výkonu na úrovni zlaté medaile na Mezinárodní matematické olympiádě.
Klíčové body
- Harmonic AI vyvíjí model Aristotle, který eliminuje halucinace běžné u jiných LLM.
- Systém využívá proof assistant Lean 4 pro formální verifikaci matematických důkazů.
- Trénovací data nejsou sbírána z webu, ale generována synteticky jako páry „úloha–důkaz“.
- Model se zlepšuje prostřednictvím „self-play loopu“, kdy se učí sám od sebe.
- Aristotle je nyní dostupný veřejnosti a má i API pro výzkumníky a matematiky.
Podrobnosti
Harmonic AI, založená v roce 2023 spoluzakladatelem Robinhoodu Vladem Tenevem, se zaměřuje na tzv. matematickou superinteligenci – AI, jejíž schopnosti formálního uvažování přesahují lidské. Na rozdíl od běžných jazykových modelů, které často vymýšlejí nepravdivé odpovědi (tzv. halucinace), systém Aristotle pracuje s formálními důkazy ověřitelnými počítačem. K tomu využívá nástroj Lean 4, který umožňuje zapisovat matematické definice, věty a důkazy v přesném, strojově čitelném formátu.
Klíčovým prvkem vývoje je syntetická generace trénovacích dat. Místo sběru dat z internetu, který je plný chyb a nekonzistentních informací, model generuje vlastní úlohy a k nim formální důkazy. Tyto páry „úloha–důkaz“ slouží k tréninku a následnému zlepšování modelu v rekurzivní smyčce – tzv. self-play loopu. Tím se model postupně posouvá od řešení základních úloh k dokazování složitých matematických vět.
Nedávno dosáhl Aristotle výkonu odpovídajícího zlaté medaili na Mezinárodní matematické olympiádě, což je nejprestižnější soutěž pro středoškolské matematiky. Společnost také zpřístupnila API, které již využívají výzkumníci k urychlení objevů v matematice.
Proč je to důležité
Tento přístup představuje významný posun směrem k spolehlivé a verifikovatelné AI, zejména v oblastech, kde chyba může mít vážné důsledky – jako je vědecký výzkum, formální verifikace softwaru nebo kritické systémy. Pokud se podaří škálovat tuto technologii i mimo matematiku, mohla by sloužit jako základ pro budoucí systémy s vysokou spolehlivostí a transparentností uvažování, což je klíčový krok k bezpečnému vývoji pokročilé umělé inteligence.
Zdroj: 📰 SiliconANGLE News