La IA ya puede demostrar matemáticamente que un código funciona; ahora falta convencer al ordenador.

Las redes neuronales aprendieron a escribir programas más rápido de lo que los humanos pueden encontrar sus errores, pero ahora la inteligencia artificial intenta controlar también la propia verificación. La startup Harmonic, fundada por el director de Robinhood Vlad Tenev y Tudor Akim, amplió las capacidades del modelo Aristotle. El sistema pasó de demostrar teoremas matemáticos a verificar código de programas y circuitos electrónicos.

27 de octubre la compañía presentó soporte para los lenguajes C y Verilog, en los que se diseñan los circuitos integrados digitales. Aristotle utiliza verificación formal, es decir, demuestra matemáticamente que un programa cumple los requisitos especificados. A diferencia de las pruebas convencionales, este enfoque permite verificar propiedades concretas para todos los posibles datos de entrada dentro del modelo elegido.

Aristotle sugiere de forma autónoma las propiedades a verificar, intenta demostrar cada una y muestra el resultado junto con las suposiciones realizadas. Los desarrolladores pueden guardar las condiciones verificadas en el repositorio y repetir el análisis en cada cambio del código. El enfoque pretende reducir el número de defectos que se pasan por alto durante la revisión del software, especialmente en la generación masiva de código por redes neuronales.

Los primeros resultados prácticos fueron curiosos. Al trabajar con la biblioteca LibTomMath, que usan Tcl y Dropbear SSH, Aristotle corrigió tres errores. Al mismo tiempo, el modelo aceleró la exponenciación modular entre un 31 y un 38 % según pruebas internas de Harmonic. Los desarrolladores afirman que la implementación acelerada corresponde matemáticamente a los requisitos originales.

Al verificar diseños de hardware, Aristotle detectó en un proyecto de la empresa Tensordyne errores que se manifestaban solo tras 110000 ciclos de reloj. Ese tipo de defectos es particularmente difícil de detectar con la simulación convencional, porque el comportamiento problemático puede aparecer tras una secuencia de operaciones extremadamente larga. No obstante, esos resultados aún no han pasado una evaluación comparativa independiente.

Otro experimento se realizó en el centro de investigación de fusión nuclear DIII-D. Según los resultados presentados, Aristotle reprodujo en cuatro horas parte del software a partir de un artículo científico y una petición de 254 palabras. La verificación abarcó la implementación de los cálculos en C y una versión para aceleración por hardware en Verilog. Los autores del experimento informaron de la equivalencia lógica demostrada de ambas versiones.

La tecnología continúa la tendencia en la que la verificación automática de pruebas matemáticas se aplica para evaluar los resultados de la IA. Sin embargo, la demostración matemática de una propiedad concreta no garantiza la seguridad total de un programa. La calidad de la verificación depende de la corrección de los requisitos y las suposiciones, y los errores fuera del modelo elegido pueden pasar desapercibidos.

Aristotle ya está disponible para usuarios comerciales con pago según el volumen de consumo. Para clientes grandes, Harmonic ofrece opciones corporativas de despliegue, incluyendo infraestructura propia y nube privada. En noviembre de 2025 la startup atrajo 120 millones de dólares con una valoración de 1,45 mil millones de dólares. Entre los inversores figuran NVentures, Sequoia y Ribbit Capital.