Reacción a "Un sistema de IA lograría una medalla en la Olimpiada Internacional de Matemáticas, según un estudio"

AlphaProof parece un sistema potente porque da garantías formales de las pruebas, no ‘alucina’ como los LLMs [Grandes Modelos de Lenguaje]. AlphaProof representa un avance conceptual fundamental: demuestra que los modelos de razonamiento pueden alcanzar la verificación formal, eliminando el riesgo de alucinaciones factuales que afecta a otros sistemas de IA.  

A diferencia de los modelos de lenguaje que pueden generar contenido plausible pero incorrecto, su arquitectura garantiza que cada inferencia sea lógicamente sólida y comprobable (esto es un aspecto fundamental del sistema). Pero hay que saber usarlo. Por ejemplo, si el sistema formal (Lean) tiene axiomas inconsistentes, producirá ‘verdades formales’ pero matemáticamente falsas. El artículo no describe con excesivo detalle el sistema, sino los resultados de la olimpiada. Yo destacaría el hecho de la verificación formal y que no ‘alucina’ como los LLMs.