Equivalence Checking of ML GPU Kernels
Este artículo presenta Volta, el primer verificador de equivalencia sólido y completo para kernels de GPU, el cual verifica formalmente la corrección de computaciones de aprendizaje automático optimizadas a mano, por compiladores o por LLMs.
Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo
En la vasta e invisible maquinaria de la inteligencia artificial moderna, el trabajo más crítico no ocurre en la nube, sino en chips informáticos especializados llamados GPUs. Estos chips están diseñados para realizar millones de cálculos diminutos simultáneamente, una necesidad para entrenar los modelos de lenguaje extensos que ahora escriben código, traducen idiomas y generan arte. Para que estos modelos funcionen con la rapidez suficiente para ser útiles, los ingenieros deben escribir instrucciones altamente especializadas, conocidas como kernels, que le dicen a la GPU exactamente cómo mover los datos y realizar operaciones matemáticas. En los últimos años, las empresas han comenzado a utilizar la propia inteligencia artificial para escribir estos kernels, con la esperanza de encontrar formas más rápidas de realizar el trabajo que los ingenieros humanos. Sin embargo, esta velocidad conlleva un riesgo: cuando una IA o un compilador reescribe una pieza de código para que sea más rápida, puede introducir accidentalmente errores sutiles. Estos errores podrían causar que la computadora produzca la respuesta incorrecta o, lo que es peor, que falle silenciosamente de formas que son casi imposibles de encontrar mediante pruebas estándar. El desafío central es que estos chips ejecutan miles de hilos de trabajo al mismo tiempo y, si no se coordinan perfectamente, pueden estorbarse entre sí, creando una condición de carrera donde el resultado final depende del orden impredecible en que ocurren las cosas.
Un equipo de investigadores ha desarrollado una nueva herramienta llamada Volta para resolver este problema. En lugar de adivinar si una versión nueva y más rápida de un kernel es correcta, Volta actúa como un verificador formal que demuestra matemáticamente que las dos versiones producen resultados idénticos. Los investigadores construyeron un sistema que toma las instrucciones de bajo nivel de un kernel de referencia —la versión original y confiable— y el kernel optimizado —la nueva versión más rápida— y los pasa por un motor simbólico. En lugar de alimentar el código con números específicos y ver qué resulta, el motor trata las entradas como símbolos abstractos. Rastrea cada posible camino que el código podría tomar, siguiendo cómo se mueven los datos a través de los miles de hilos paralelos y cómo se sincronizan entre sí. Si el código intenta acceder a la memoria de una manera que podría causar un conflicto, o si los hilos se quedan esperando el uno al otro para siempre, la herramienta señala el error inmediatamente. Si el código se ejecuta sin problemas, la herramienta traduce la salida final de ambos kernels en expresiones matemáticas complejas y comprueba si esas expresiones son fundamentalmente las mismas, independientemente de los números específicos que se introduzcan.
Los investigadores probaron Volta en una amplia variedad de tareas de aprendizaje automático del mundo real, incluyendo multiplicaciones de matrices, convoluciones y los mecanismos de atención que impulsan los modelos de lenguaje extensos. Descubrieron que la herramienta podía verificar con éxito kernels que habían sido optimizados a mano, por compiladores e incluso por modelos de lenguaje extensos. En un caso, examinaron un kernel generado por una IA que había sido optimizado mediante trece rondas de mejora automatizada. Volta confirmó que este código generado por IA era matemáticamente equivalente al referente original escrito por humanos, demostrando que las agresivas optimizaciones no habían roto la lógica. La herramienta también demostró su valor al detectar errores que otros métodos pasaron por alto. Por ejemplo, detectó condiciones de carrera en un tutorial popular y ampliamente citado de programación de GPU que había sido utilizado por miles de desarrolladores durante años. Estos errores estaban ocultos porque solo aparecían bajo condiciones de tiempo muy específicas que las pruebas estándar rara vez detectan. La herramienta también identificó un error en un kernel generado por IA donde el código intentaba leer datos de una ubicación de memoria que no existía; aunque el hardware actual resultó ignorar este error, los investigadores demostraron que el código era fundamentalmente inseguro y podría fallar en máquinas futuras.
La fuerza de este enfoque reside en su capacidad para manejar la complejidad única de la programación de GPU, donde miles de hilos deben coordinar sus acciones. Las herramientas anteriores podían verificar programas de un solo hilo u operaciones matemáticas de alto nivel, pero tenían dificultades para descomponer el masivo paralelismo de una GPU en piezas manejables. Volta supera esto asumiendo que los kernels que analiza siguen un patrón específico y estructurado común en el aprendizaje automático, donde el número de hilos y el tamaño de los datos se conocen de antemano. Dentro de este marco, la herramienta puede demostrar con certeza que existe una condición de carrera si los hilos no están debidamente sincronizados, y puede demostrar que dos versiones diferentes de un programa son equivalentes si producen el mismo resultado simbólico. Los investigadores demostraron que su herramienta podía verificar estas propiedades en cuestión de segundos o minutos, incluso para kernels que contienen cientos de miles de instrucciones. También demostraron que la lógica matemática detrás de su herramienta es sólida, lo que significa que si la herramienta dice que dos programas son iguales, son verdaderamente iguales para todas las entradas posibles.
Este trabajo representa un paso significativo hacia la creación de una inteligencia artificial más segura y confiable. A medida que las empresas dependen cada vez más de sistemas automatizados para generar el código que impulsa sus modelos, la necesidad de una forma rigurosa de verificar ese código se vuelve crítica. Los investigadores demostraron que es posible ir más allá de las simples pruebas, que solo pueden verificar un número limitado de escenarios, hacia un método que proporciona una garantía formal de corrección. Al verificar la equivalencia de los kernels optimizados, Volta brinda a los desarrolladores la confianza para utilizar optimizaciones más rápidas y agresivas sin temor a introducir errores silenciosos. La herramienta está actualmente disponible para su uso, y los investigadores han puesto su código y las pruebas detrás de él a disposición del público, permitiendo que otros construyan sobre esta base. Aunque la herramienta aún no cubre todos los tipos posibles de código de GPU, maneja con éxito la gran mayoría de los kernels que impulsan el aprendizaje automático moderno, ofreciendo un nuevo estándar de confianza en la generación automatizada de código de computación de alto rendimiento.
¿Ahogado en artículos de tu campo?
Recibe resúmenes diarios de los artículos más novedosos que coincidan con tus palabras clave de investigación — con resúmenes técnicos, en tu idioma.