Google DeepMind libera el código de AlphaProof y lleva la verificación formal matemática a la era de los LLM
El sistema que resolvió problemas de la Olimpiada Internacional de Matemáticas en 2024 tiene código fuente y pesos liberados, permitiendo a investigadores acoplar modelos de lenguaje a probadores formales como Lean
Google DeepMind liberó el código fuente y los pesos de AlphaProof, el sistema que en 2024 resolvió problemas de la Olimpiada Internacional de Matemáticas (IMO) al acoplar un modelo de lenguaje a un probador formal. La apertura pone en manos de la comunidad de investigación una de las arquitecturas más influyentes para el razonamiento automatizado verificable.
La decisión transforma lo que era un experimento cerrado de laboratorio en infraestructura abierta para universidades, startups y grupos independientes que trabajan con demostraciones matemáticas asistidas por máquina.
Cómo funciona el sistema en la práctica
AlphaProof no genera texto suelto: produce pruebas escritas en el lenguaje formal Lean, en el que cada paso lógico es verificado por un kernel independiente. Si una etapa no se sostiene, la prueba es rechazada — lo que elimina buena parte de las alucinaciones típicas de los modelos de lenguaje.
La arquitectura combina un modelo de lenguaje que propone estrategias de demostración con un mecanismo de búsqueda que prueba y refina cada intento contra el verificador. El aprendizaje ocurre por refuerzo, con el sistema acumulando pruebas válidas a lo largo del entrenamiento.
Por qué importa la verificación formal
La verificación por Lean se ha convertido en uno de los campos más disputados de la investigación en IA. A diferencia de un chatbot que responde con confianza a una ecuación errónea, un sistema que escribe pruebas formales debe convencer a un verificador matemático — no a un lector humano.
Esta propiedad atrae el interés de laboratorios que buscan modelos confiables para ingeniería de software, criptografía y descubrimiento científico, áreas en las que un error silencioso cuesta caro.
Qué cambia con el código abierto
Con el acceso al código y a los pesos, los investigadores pueden reproducir el pipeline de entrenamiento, adaptar el sistema a otros probadores formales y medir su desempeño en benchmarks propios. La apertura también permite auditar las decisiones de diseño de DeepMind.
El movimiento sigue la estrategia del laboratorio de publicar artefactos de investigación en matemática formal, campo en el que la verificación por máquina se ha convertido en un estándar de calidad científica.