AxiomMath vuole tenere fuori la "spazzatura" dell'IA dalla matematica
techcrunch ·
AxiomMath, una startup da 1,6 miliardi di dollari fondata dalla studentessa abbandonata di Stanford Carina Hong, ha verificato formalmente con successo lo Stacks Project, uno dei corpus più estesi di matematica scritta da esseri umani. Traducendo circa 7.654 pagine in 16 milioni di righe di codice Lean, l'azienda mira a creare una base affidabile per gli agenti AI da utilizzare nello sviluppo software e nella ricerca scientifica. Questo sforzo affronta le crescenti preoccupazioni riguardo alla bassa qualità dell'"AI slop" che sta inondando le riviste accademiche di affermazioni non verificate. Il processo di verifica garantisce la correttezza logica attraverso assistenti di dimostrazione, preservando la struttura interconnessa di teoremi complessi nella geometria algebrica. Axiom ha addestrato i propri modelli per sviluppare un senso intuitivo della correttezza matematica, consentendo ad agenti AI paralleli di lavorare in modo efficiente sul progetto. La libreria formalizzata risultante funge da substrato riutilizzabile, consentendo alle future dimostrazioni di basarsi su risultati già verificati anziché partire da zero. L'amministratore delegato Hong sfida altre aziende di coding ad adottare sforzi di formalizzazione su larga scala simili per garantire l'integrità delle infrastrutture generate dall'IA.
techcrunch