Ante esta realidad, algunas empresas emergentes en Silicon Valley están buscando desarrollar tecnología para verificar la precisión del código creado por la IA.
Los chatbots de IA como ChatGPT o los sistemas de soporte de programación actuales pueden crear código informático en solo unos segundos. Sin embargo, los expertos dicen que estos sistemas a veces todavía tienen errores o incluso crean información inexacta.
Un estudio publicado en enero por investigadores de la Universidad Carnegie Mellon (EE. UU.) muestra que las herramientas de IA de creación de código pueden ayudar a acelerar el proceso de desarrollo de software. Sin embargo, también pueden reducir la calidad del código, causando problemas a largo plazo para los proyectos.
Ante este desafío, muchas empresas emergentes en Silicon Valley están desarrollando tecnología para verificar el código informático.
Las startups tecnológicas en el campo de la inteligencia artificial como Axiom Math y Harmonic (en Palo Alto, California) o Logical Intelligence (San Francisco) están construyendo sistemas de IA capaces de verificar código de manera similar a cómo los matemáticos demuestran un problema.
Carina Hong, fundadora y CEO de Axiom Math, cree que la autenticación de código podría convertirse en el siguiente paso en el proceso de desarrollo de la tecnología de IA.
Recientemente, esta empresa anunció que había recaudado con éxito 200 millones de dólares de fondos de capital riesgo, incluidos Menlo Ventures, Greycroft y Madrona.
Aunque se fundó hace aproximadamente un año y solo tiene unos 20 empleados, Axiom Math ya está valorada en 1.600 millones de dólares. Los inversores creen que la tecnología de la empresa puede ayudar a mejorar la calidad del código creado por sistemas de IA como Codex o Claude Code.
Según Matt Kraning (un inversor de riesgo en el campo de la tecnología y socio de Menlo Ventures), el mayor problema al usar la IA para escribir código hoy en día es que los usuarios no pueden estar seguros de si el código está defectuoso o no.
Matt Kraning cree que la tecnología de verificación de código como la de Axiom puede ayudar a resolver en parte este problema.
Inicialmente, Axiom desarrolló una tecnología para resolver problemas matemáticos complejos. El sistema de la empresa llamado AxiomProver obtuvo la máxima puntuación en el examen de matemáticas de Putnam (uno de los mejores concursos para estudiantes universitarios en Estados Unidos y Canadá).
Esta tecnología funciona utilizando el lenguaje de programación Lean, que se desarrolló hace más de una década para demostrar proposiciones matemáticas.
Gracias a la capacidad de determinar claramente lo correcto y lo incorrecto en matemáticas, el sistema puede eliminar errores lógicos en el proceso de resolución de problemas.
Los investigadores esperan que se pueda aplicar el mismo método para verificar el código informático. Este es un ejemplo de "aprendizaje de transferencia", cuando un sistema de IA aprende habilidades en un campo y las aplica con éxito a otras tareas.
Sin embargo, algunos expertos advierten que este método todavía tiene limitaciones. Según Bogdan Vasilescu, profesor de informática en la Universidad Carnegie Mellon, no siempre es posible definir claramente qué es un código informático "correcto".
En realidad, muchos programas, especialmente los servicios en línea que sirven a millones de usuarios, tendrán entornos operativos complejos y difíciles de predecir.
Por lo tanto, aunque la IA puede ayudar a verificar algunos errores, esta tecnología difícilmente puede eliminar por completo todos los problemas en el código informático.
