Axiom Quant Inc. dijo hoy que está listo para dar un paso al frente y asegurarse de que el tsunami de código generado por inteligencia artificial sea seguro y preciso después de recaudar 200 millones de dólares en financiación inicial.
La ronda Serie A, que eleva la valoración de Axiom a 1.600 millones de dólares, fue liderada por Menlo Ventures y representa una apuesta por un nuevo paradigma que llama “IA verificada” que tiene como objetivo eliminar el riesgo de “alucinaciones” de una vez por todas.
Los fundadores de Axiom están tratando de abordar un defecto fundamental en la forma en que la IA crea software. Aunque las herramientas existentes como Claude Code y CodeRabbit pueden generar código realmente impresionante que generalmente funciona bien, su naturaleza probabilística es un motivo importante de preocupación.
Estas herramientas están diseñadas para producir resultados que parecen correctos, en lugar de aquellos que son demostrablemente correctos. Y este es un gran problema, según Matt Kraning y C.C., socios de Menlo Ventures. Gong. En una publicación de blog anunciando la ronda de hoy, dijeron que tener un código que "funciona con frecuencia" es un "estándar aterrador" cuando se va a utilizar en sistemas de infraestructura crítica.
“Los LLM son estadísticos por naturaleza: producen resultados plausibles, no demostrablemente correctos o seguros”, escribieron los socios. "No pueden garantizar que una función devuelva la respuesta correcta y no pueden garantizar que no introduzca una vulnerabilidad de seguridad en el proceso. Este no es un error que se solucionará con la próxima generación de modelos. Es arquitectónico. Las alucinaciones y el código inseguro de la IA no van a desaparecer".
Axiom soluciona esto entrenando sistemas de inteligencia artificial para generar resultados verificados formalmente en Lean, que es un lenguaje de programación especializado diseñado para pruebas matemáticas. Al utilizar Lean, Axiom puede garantizar que cada paso del proceso de razonamiento de un modelo de IA sea "comprobable por máquina" y esté lógicamente garantizado.
Utiliza verificadores de prueba deterministas para comprender cuándo una salida es incorrecta. Lo que esto significa es que puede proporcionar certeza matemática de que cualquier función de código generada por un modelo de IA siempre devolverá la respuesta correcta. Además, puede verificar que los nuevos fragmentos de código no introduzcan vulnerabilidades ocultas.
La startup llamó la atención por primera vez en octubre, cuando recaudó 64 millones de dólares en financiación inicial, y ha logrado avances significativos desde entonces. En diciembre, su IA determinista logró una puntuación perfecta en el concurso Putnam, considerado por los matemáticos como el examen universitario de matemáticas más exigente del mundo. En el último siglo, sólo cinco humanos han logrado la misma puntuación perfecta, señalaron Kraning y Gong.
En otro logro, Axiom probó de manera verificable una conjetura de la teoría de números de hace 20 años que involucra elementos de cálculo utilizados para medir distancias a lo largo de superficies curvas. Era un desafío que el matemático fundador de Axiom, Ken Ono (en la foto, izquierda), nunca había podido resolver, a pesar de los repetidos intentos de hacerlo a lo largo de los años.
Para cada salida de IA, Axiom genera un "volante de datos verificados" que consta de grandes cantidades de datos verificados. Luego, esto se retroalimenta a los ciclos de entrenamiento para mejorar las capacidades de sus modelos, sin introducir el riesgo de "colapso del modelo", que se refiere a la contaminación de datos que causa problemas con los modelos de IA no verificados. De esta manera, Axiom opera como un bucle recursivo de superación personal.
La startup fue fundada por un doctor de la Universidad de Stanford de 25 años. La estudiante y maga de las matemáticas Carina Hong (en la foto, derecha), quien se graduó en el MIT y se desempeña como su directora ejecutiva. A pesar de su corta edad, ya es ganadora del Premio Morgan, del Premio Schafer y autora de nueve publicaciones revisadas por pares. Ha reunido un equipo impresionante, incluido Ono, miembro de Guggenheim, Packard y Sloan, que anteriormente se desempeñó como vicepresidente de la Sociedad Matemática Estadounidense y es una de las principales autoridades mundiales en las matemáticas de Ramanujan.
El director de tecnología de Axiom es el ex director de investigación de inteligencia artificial de Facebook, Shubho Sengupta, quien ayudó a escribir las bibliotecas fundamentales de unidades de procesamiento de gráficos en Nvidia Corp.El equipo también incluye a François Charton, famoso por ser la primera persona en aplicar modelos de transformadores para resolver un problema matemático que había desconcertado a los expertos durante más de 130 años.
Holger Mueller de Constellation Research dijo que los desarrolladores que se han vuelto cada vez más dependientes de este tipo de herramientas buscan una solución viable a los riesgos de la codificación por vibración. Él cree que Axiom puede ganar muchos fanáticos si lo logra. "El riesgo de que los LLM tengan alucinaciones no es lindo; es completamente incorrecto y muy a menudo incluso peligroso cuando se trata de código escrito en LLM", dijo el analista. "Axiom ha adoptado el enfoque correcto, utilizando las matemáticas para validar y verificar que el código generado por IA es seguro. Después de todo, es un juego de números. El desafío ahora es escalar su solución para satisfacer las demandas del mundo de la codificación".
La startup ve una gran oportunidad para verificar de manera demostrable cada línea de código generado por IA en un mundo donde prácticamente todo el software se crea con la ayuda de grandes modelos de lenguaje. "Todas las empresas que envían código generado por IA están aceptando riesgos desconocidos hoy en día: no solo que el código pueda producir resultados incorrectos, sino que pueda crear superficies de ataque que nadie anticipó", dijeron Kraning y Gong. “Axiom elimina ambas categorías de riesgo simultáneamente.”
El siguiente paso de Axiom es ampliar su infraestructura de capacitación y ampliar su equipo de expertos en matemáticas, con el objetivo de hacer que la verificación formal sea rápida y asequible para todas las empresas que utilizan IA.
