Souhrn
Startup Harmonic AI získal 120 milionů dolarů v sérii C na valuaci 1,45 miliardy dolarů, mezi investory je NVentures od Nvidia. Financování urychlí vývoj Aristotle, motoru pro formální matematické uvažování, který převádí přirozený jazyk na ověřitelné důkazy pomocí Lean 4 proof assistenta. Systém dosáhl zlaté medaile na Mezinárodní matematické olympiádě 2025 a 96,8 % na benchmarku Verifiable Code Generation Arena.
Klíčové body
- Investice 120 milionů dolarů v listopadu 2025 na valuaci 1,45 miliardy dolarů, investor NVentures (Nvidia).
- Aristotle: motor pro matematické uvažování bez halucinací, trénovaný na syntetických datech.
- Používá Lean 4 proof assistant pro formální důkazy z přirozeného jazyka.
- Úspěchy: zlatá medaile na IMO 2025, 96,8 % na VERINA benchmarku pro ověřitelné generování kódu.
- Cílem je matematická superinteligence s rekurzivním sebezdokonalováním.
Podrobnosti
Harmonic AI se specializuje na vývoj umělé inteligence schopné matematické superinteligence, což znamená uvažování překonávající lidské možnosti v formální logice a důkazech. Jejich hlavní produkt Aristotle je AI motor určený k řešení matematických úloh z přirozeného jazyka, který je převádí do formálních důkazů ověřitelných počítačem. K tomu slouží Lean 4 proof assistant, open-source nástroj umožňující definovat matematické pojmy, teoremata a důkazy v programovacím jazyce, kde correctness zajišťuje automatický checker. Na rozdíl od běžných velkých jazykových modelů (LLM), které trénují na webových datech a trpí halucinacemi – tedy vymýšlením nesprávných odpovědí –, Aristotle generuje syntetická data. Tato data sestávají z párů problém-důkaz, vytvářených autonomně, což umožňuje rekurzivní sebezdokonalování: model se zlepšuje iterativně bez závislosti na externích zdrojích.
Praktické výsledky ukazují sílu přístupu. Na Mezinárodní matematické olympiádě 2025 Aristotle dosáhl výkonu na úrovni zlaté medaile, což představuje průlom v automatickém řešení složitých soutěžních úloh. Nedávno rozšířil schopnosti do generování kódu: na benchmarku VERINA, vyvinutém výzkumníky z University of California at Berkeley a Meta Platforms, získal 96,8 %. VERINA testuje generování kódu, jehož správnost lze formálně ověřit, na rozdíl od neformálních metod, které jsou nákladné a manuální. Harmonic AI tvrdí, že ověřitelné generování kódu se stává klíčovým využitím LLM v softwarovém vývoji, kde chyba může mít vážné důsledky. Systém tak slouží k tvorbě bezpečného, ověřeného kódu pro aplikace od bezpečnostních systémů po vědecké simulace.
Financování od NVentures, které se zaměřuje na rané investice do AI a hardwaru pro Nvidia GPU, signalizuje zájem o technologie zesilující výkon grafických procesorů v AI tréninku. Celkové kolo proběhlo v listopadu 2025 a prostředky půjdou na škálování Aristotle.
Proč je to důležité
Tato investice podtrhuje posun v AI od statistického predikování k formálnímu uvažování, klíčovému pro spolehlivost v kritických oblastech jako medicína, finance nebo autonomní systémy. Eliminace halucinací prostřednictvím Lean 4 a syntetických dat může zlepšit důvěryhodnost AI, což je problém současných modelů jako GPT nebo Claude. Pro průmysl znamená potenciál pro automatizaci důkazů v softwaru a matematice, kde lidé selhávají kvůli složitosti. Nvidia zde vidí synergii se svými GPU, které urychlují trénink. Nicméně jako startup musí Harmonic AI prokázat dlouhodobou škálovatelnost mimo benchmarky; rekurzivní zlepšování je slibné, ale vyžaduje obrovské výpočetní zdroje. V širším kontextu posiluje to soutěž mezi OpenAI, Google DeepMind a novými hráči v AGI směru, kde matematika je základním kamenem.
Zdroj: 📰 SiliconANGLE News
