Un innovador sistema de IA muestra promesa en la verificación de software sin errores
- Baldur, un sistema de IA desarrollado junto con Google, automatiza las demostraciones matemáticas para reducir errores de software y mejorar la precisión.
- Mediante el ajuste fino de modelos de lenguaje grandes, Baldur y Thor logran una tasa de éxito del 65,7 % en la generación de demostraciones.
- Este avance promete agilizar la verificación del software y mejorar su fiabilidad, marcando un progreso significativo en el desarrollo de software libre de errores.
Tradicionalmente, la verificación del código de software ha sido un proceso laborioso que implica revisiones manuales del código o la ejecución del código para identificar anomalías. Aunque valiosas, estos métodos son susceptibles al error humano e imprácticos para sistemas complejos.
Aquí entra Baldur, una solución meticulosamente diseñada que aprovecha el poder de los Modelos de Lenguaje Grande (LLM) para generar demostraciones matemáticas automáticamente. Al ajustar finamente los LLM en contenido matemático extenso y en el lenguaje Isabelle/HOL utilizado para las demostraciones, Baldur da un gran paso hacia la automatización de lo que antes era una tarea ardua. ¿El resultado? Un sistema que trabaja en conjunto con los demostradores de teoremas para verificar la corrección del código, reduciendo significativamente el margen de error.
En el corazón del éxito de Baldur está la asociación con Thor, la herramienta responsable de generar demostraciones automáticamente. Thor tiene una tasa de éxito del 57 %, pero cuando se combina con Baldur, los dos alcanzan una notable precisión del 65,7 % en la generación de demostraciones. Este dúo dinámico, inspirado en la mitología nórdica, demuestra el potencial de la verificación de software impulsada por IA.
Desafíos en los LLM
Uno de los principales desafíos encontrados al trabajar con LLM, como ChatGPT, es su ocasional falta de corrección. En lugar de levantar banderas rojas, pueden «fallar en silencio», proporcionando resultados erróneos que parecen válidos. Abordar este problema es crucial para garantizar la fiabilidad de las demostraciones generadas por IA.
El desarrollo de Baldur no fue una tarea menor, tomando varios meses y un esfuerzo colaborativo con Google. Emily First, autora principal del proyecto, empleó Minerva, un LLM entrenado en un vasto corpus de texto en lenguaje natural. Posteriormente, Minerva fue ajustado finamente (fine-tuned) en un conjunto de datos sustancial de 118 GB de artículos matemáticos y científicos y contenido web que contenía expresiones matemáticas. Sin embargo, el diferenciador clave fue el ajuste fino adicional del lenguaje Isabelle/HOL, sentando las bases para la generación de demostraciones matemáticas integrales.
El enfoque de Baldur para la corrección de errores es ingenioso. Cuando el demostrador de teoremas identifica un error en una demostración generada, devuelve esta información a Baldur, lo que permite al sistema aprender de sus errores. Este proceso iterativo mejora la precisión y fiabilidad de las demostraciones, convirtiéndolo en una herramienta altamente efectiva para la verificación de código.
Un futuro prometedor para el software sin errores
Aunque hay margen de mejora, Baldur representa una vía prometedora para la verificación formal de software. Los ingenieros siguen siendo responsables de desarrollar el software, pero ahora tienen un poderoso aliado en forma de Baldur, capaz de automatizar la creación de demostraciones matemáticas.
Yuriy Brun, profesor de la Facultad Manning de Ciencias de la Información y la Computación de la UMass Amherst, comentó: «Nuestro trabajo se centra en intentar automatizar la escritura de estas demostraciones. Baldur utiliza modelos de lenguaje grandes para, dada una demostración matemática, generar automáticamente una demostración de ese teorema que luego un demostrador de teoremas puede verificar.»
El éxito de Baldur se atribuye al equipo dedicado que trabajó incansablemente en este proyecto. Junto con Emily First, Markus Rabe, quien Google empleaba en ese momento, y Talia Ringer, profesora asistente en la Universidad de Illinois en Urbana-Champaign, contribuyeron significativamente. La Agencia de Proyectos de Investigación Avanzada de Defensa (DARPA) y la Fundación Nacional de Ciencias (NSF) apoyaron el proyecto.
Soluciones innovadoras como Baldur ofrecen esperanza mientras la industria tecnológica lidia con la creciente complejidad de los sistemas de software. Con las capacidades de la IA que continúan evolucionando y madurando, el potencial de Baldur para llevar la corrección del software a nuevas cotas sigue siendo prometedor.
No te limites a leer noticias sobre criptomonedas. Entiéndelas. Suscríbete a nuestro boletín. Es gratis.
Aviso de responsabilidad. La información proporcionada no es un consejo de trading. Cryptopolitan.com no asumimos responsabilidad alguna por las inversiones realizadas basándose en la información proporcionada en esta página. Recomendamos encarecidamente la investigación independiente y/o la consulta con un profesional calificado antes de tomar cualquier decisión de inversión.
Brenda Kanana
Brenda cuenta con más de 4 años de experiencia especializada en criptomonedas, inteligencia artificial y tecnologías emergentes. Ha trabajado en Zycrypto, Blockchain Reporter y The Coin Republic, y ahora tiene a Cryptopolitan como su hogar. Su licenciatura en Sociología de la Universidad Técnica de Mombasa la mantiene alineada con las necesidades de sus lectores.
