AxiomMath veut empêcher l'IA de polluer les mathématiques
techcrunch ·
AxiomMath, une startup évaluée à 1,6 milliard de dollars fondée par Carina Hong, ancienne étudiante de Stanford, a réussi à vérifier formellement le Stacks Project, l'un des corpus les plus vastes de mathématiques écrites par des humains. En traduisant environ 7 654 pages en 16 millions de lignes de code Lean, l'entreprise vise à créer une base fiable pour les agents d'IA utilisés dans le développement logiciel et la recherche scientifique. Cette initiative répond aux préoccupations croissantes concernant la prolifération de « déchets » (AI slop) de faible qualité dans les revues académiques, qui inondent ces publications avec des affirmations non vérifiées. Le processus de vérification garantit la cohérence logique grâce à des assistants de preuve, préservant ainsi la structure interconnectée des théorèmes complexes en géométrie algébrique. Axiom a entraîné ses propres modèles pour développer un sens intuitif de la correction mathématique, permettant à des agents d'IA parallèles de travailler efficacement sur le projet. La bibliothèque formalisée résultante sert de substrat réutilisable, permettant aux preuves futures de s'appuyer sur des résultats vérifiés plutôt que de repartir de zéro. La PDG Hong lance un défi aux autres entreprises de codage pour qu'elles adoptent des efforts de formalisation à grande échelle similaires, afin de garantir l'intégrité des infrastructures générées par l'IA.
techcrunch