A medida que la inteligencia synthetic remodela el desarrollo de software program, una pequeña startup apuesta a que el próximo gran cuello de botella de la industria no será escribir código, sino confiar en él.
Teoremauna empresa con sede en San Francisco que surgió de Y Combinator’s Primavera 2025 lote, anunció el martes que ha recaudado 6 millones de dólares en financiación inicial para construir herramientas automatizadas que verifiquen la exactitud del software program generado por IA. Khosla Ventures lideró la ronda, con la participación de Combinador Y, e14, SAIF, Martín pescadore inversores ángeles, incluidos Blake Borgesson, cofundador de Recursion Prescribed drugs, y Arthur Breitman, cofundador de la plataforma blockchain Tezos.
La inversión llega en un momento essential. Asistentes de codificación de IA de empresas como GitHub, Amazonasy Google Ahora generamos miles de millones de líneas de código anualmente. La adopción empresarial se está acelerando. Pero la capacidad de verificar que el software program escrito por IA realmente funciona según lo previsto no ha seguido el ritmo, creando lo que los fundadores de Theorem describen como una “brecha de supervisión” cada vez mayor que amenaza la infraestructura crítica, desde los sistemas financieros hasta las redes eléctricas.
“Ya estamos allí”, dijo Jason Gross, cofundador de Theorem, cuando le preguntamos si el código generado por IA está superando la capacidad de revisión humana. “Si me pidieran que revisara 60.000 líneas de código, no sabría cómo hacerlo”.
Por qué la IA escribe código más rápido de lo que los humanos pueden verificarlo
La tecnología central de Theorem combina la verificación formal (una técnica matemática que demuestra que el software program se comporta exactamente como se especifica) con modelos de IA entrenados para generar y verificar pruebas automáticamente. El enfoque transforma un proceso que históricamente requería años de ingeniería a nivel de doctorado en algo que, según la empresa, se puede completar en semanas o incluso días.
La verificación formal ha existido durante décadas, pero permaneció confinada a las aplicaciones más críticas: sistemas de aviónica, controles de reactores nucleares y protocolos criptográficos. El costo prohibitivo de la técnica (que a menudo requiere ocho líneas de prueba matemática por cada línea de código) la hacía poco práctica para el desarrollo de software program convencional.
Gross lo sabe de primera mano. Antes de fundar Theorem, obtuvo su doctorado en el MIT trabajando en investigaciones verificadas. código de criptografía que ahora impulsa el protocolo de seguridad HTTPS protegiendo billones de conexiones a Web diariamente. Ese proyecto, según sus estimaciones, consumió quince años-persona de trabajo.
“Nadie prefiere tener un código incorrecto”, afirmó Gross. “La verificación del software program simplemente no period económica antes. Las pruebas solían ser escritas por ingenieros con nivel de doctorado. Ahora, la IA lo escribe todo”.
Cómo la verificación formal detecta los errores que las pruebas tradicionales pasan por alto
El sistema del teorema opera según un principio que Gross llama “descomposición de prueba fraccionaria”. En lugar de probar exhaustivamente todos los comportamientos posibles (computacionalmente inviables para software program complejo), la tecnología asigna recursos de verificación proporcionalmente a la importancia de cada componente del código.
El enfoque identificó recientemente un error que pasó desapercibido en las pruebas de Anthropic, la compañía de seguridad de inteligencia synthetic detrás del chatbot Claude. Gross dijo que la técnica ayuda a los desarrolladores a “detectar sus errores ahora sin gastar mucho procesamiento”.
En una demostración técnica reciente llamada SFBench, Theorem utilizó IA para traducir 1276 problemas de Rocq (un asistente de prueba formal) a Lean (otro lenguaje de verificación), y luego demostró automáticamente que cada traducción period equivalente al authentic. La empresa estima que un equipo humano habría requerido aproximadamente 2,7 personas-año para completar el mismo trabajo.
“Todos pueden ejecutar agentes en paralelo, pero también podemos ejecutarlos secuencialmente”, explicó Gross, señalando que la arquitectura de Theorem maneja código interdependiente (donde las soluciones se basan entre sí en docenas de archivos) que hacen tropezar a los agentes de codificación de IA convencionales limitados por ventanas de contexto.
Cómo una empresa convirtió una especificación de 1.500 páginas en 16.000 líneas de código confiable
La startup ya está trabajando con clientes en laboratorios de investigación de inteligencia synthetic, automatización de diseño electrónico e informática acelerada por GPU. Un estudio de caso ilustra el valor práctico de la tecnología.
Un cliente llegó a Theorem con una especificación PDF de 1500 páginas y una implementación de software program heredado plagada de pérdidas de memoria, fallas y otros errores difíciles de alcanzar. Su problema más urgente: mejorar el rendimiento de 10 megabits por segundo a 1 gigabit por segundo (un aumento de 100 veces) sin introducir errores adicionales.
El sistema de Theorem generó 16.000 líneas de código de producción, que el cliente implementó sin siquiera revisarlo manualmente. La confianza provino de una especificación ejecutable compacta (unos pocos cientos de líneas que generalizaban el enorme documento PDF) combinada con un arnés de verificación de equivalencia que verificaba que la nueva implementación coincidiera con el comportamiento previsto.
“Ahora tienen un analizador de nivel de producción que opera a 1 Gbps y que pueden implementar con la confianza de que no se pierde información durante el análisis”, afirmó Gross.
Los riesgos de seguridad que acechan en el software program generado por IA para infraestructuras críticas
El anuncio de financiación llega en un momento en que los responsables políticos y los tecnólogos examinan cada vez más la fiabilidad de los sistemas de IA integrados en infraestructuras críticas. El software program ya controla los mercados financieros, los dispositivos médicos, las redes de transporte y las redes eléctricas. La IA está acelerando la rapidez con la que evoluciona el software program y la facilidad con la que se pueden propagar errores sutiles.
Gross enmarca el desafío en términos de seguridad. A medida que la IA abarata la búsqueda y explotación de vulnerabilidades, los defensores necesitan lo que él llama “defensa asimétrica”: protección que escala sin aumentos proporcionales en los recursos.
“La seguridad del software program es un delicado equilibrio entre ataque y defensa”, afirmó. “Con el hackeo de IA, el costo de hackear un sistema está cayendo drásticamente. La única solución viable es la defensa asimétrica. Si queremos una solución de seguridad de software program que pueda durar más de unas pocas generaciones de mejoras del modelo, será a través de la verificación”.
Cuando se le preguntó si los reguladores deberían exigir la verificación formal del código generado por IA en sistemas críticos, Gross ofreció una respuesta contundente: “Ahora que la verificación formal es lo suficientemente barata, podría considerarse negligencia grave no usarla para garantías sobre sistemas críticos”.
Lo que separa a Theorem de otras empresas emergentes de verificación de códigos de IA
Theorem ingresa a un mercado donde numerosas empresas emergentes y laboratorios de investigación están explorando la intersección de la IA y la verificación formal. La diferenciación de la empresa, sostiene Gross, radica en su singular enfoque en ampliar la supervisión del software program en lugar de aplicar la verificación a las matemáticas u otros dominios.
“Nuestras herramientas son útiles para los equipos de ingeniería de sistemas que trabajan cerca del steel y necesitan garantías de corrección antes de fusionar cambios”, dijo.
El equipo fundador refleja esa orientación técnica. Gross aporta una profunda experiencia en teoría de lenguajes de programación y un historial de implementación de código verificado en producción a escala. El cofundador Rajashree Agrawal, ingeniero de investigación de aprendizaje automático, se centra en entrenar los modelos de IA que impulsan el proceso de verificación.
“Estamos trabajando en el razonamiento formal del programa para que todos puedan supervisar no sólo el trabajo de una IA promedio de nivel de ingeniero de software program, sino también aprovechar las capacidades de una IA de nivel Linus Torvalds”, dijo Agrawal, refiriéndose al legendario creador de Linux.
La carrera por verificar el código de la IA antes de que lo controle todo
Teorema planea utilizar los fondos para ampliar su equipo, aumentar los recursos informáticos para entrenar modelos de verificación e ingresar a nuevas industrias, incluidas la robótica, la energía renovable, las criptomonedas y la síntesis de fármacos. La empresa emplea actualmente a cuatro personas.
El surgimiento de la startup indica un cambio en la forma en que los líderes tecnológicos empresariales pueden necesitar evaluar las herramientas de codificación de IA. La primera ola de desarrollo asistido por IA prometió ganancias de productividad: más código, más rápido. El teorema es apostar a que la próxima ola exigirá algo diferente: una prueba matemática de que la velocidad no se consigue a costa de la seguridad.
Gross plantea lo que está en juego en términos claros. Los sistemas de IA están mejorando exponencialmente. Si esa trayectoria se mantiene, cree que la ingeniería de software program sobrehumana es inevitable: capaz de diseñar sistemas más complejos que cualquier cosa que los humanos hayan construido jamás.
“Y sin una economía de supervisión radicalmente diferente”, dijo, “terminaremos implementando sistemas que no controlamos”.
Las máquinas están escribiendo el código. Ahora alguien tiene que comprobar su trabajo.
