Por Canuto  

Un sistema desarrollado por investigadores de Meta y la Universidad de Nueva York obtuvo resultados destacados en pruebas de demostración matemática con una arquitectura deliberadamente sencilla. En problemas de Erdős, reportó una tasa de éxito superior a la de AlphaProof Nexus y un costo por prueba exitosa considerablemente menor.
***

  • h1 combina modelos de lenguaje con Lean 4 y retroalimentación inmediata del verificador, sin recurrir a una orquestación compleja.
  • El sistema alcanzó 670 de 672 puntos en PutnamBench y 90 de 100 en FATE-X, además de resolver ocho problemas abiertos.
  • En problemas de Erdős, h1 registró 82,5% de éxito y USD $121 por prueba exitosa, frente a 76% y USD $317 para AlphaProof Nexus.

Un sistema de inteligencia artificial desarrollado por investigadores de Meta y la Universidad de Nueva York (NYU) busca demostrar que una herramienta menos compleja también puede rendir al máximo en matemáticas formales. Llamado h1, conectó modelos de lenguaje con Lean 4 y obtuvo resultados destacados en varios puntos de referencia, además de resolver ocho problemas abiertos de una colección matemática.

Un ciclo de prueba sin una maquinaria extensa

El equipo de investigación FAIR de Meta y especialistas de NYU describieron h1 en el trabajo h1: A Taste of the Bitter Lesson in Automated Theorem Proving, publicado el 25 de octubre de 2026. Su diseño parte de una idea concreta: en lugar de rodear al modelo con una arquitectura sofisticada de agentes y tareas, conviene permitirle interactuar de forma directa con el verificador de Lean 4. La investigación pone así el foco en la calidad de esa interacción.

Lean 4 funciona como un entorno en el que las demostraciones matemáticas pueden expresarse formalmente y comprobarse mediante un verificador. En h1, el modelo trabaja sobre un archivo de prueba persistente, de modo que el estado de su trabajo continúa entre una edición y la siguiente. Esa continuidad evita que cada paso se trate como un intento separado y permite que el modelo revise una misma demostración a medida que avanza.

La segunda pieza del ciclo es la retroalimentación inmediata del compilador después de cada cambio. Si una edición contiene errores, el sistema puede recibir esa señal y utilizarla para orientar la siguiente acción, en lugar de esperar al final de un flujo largo para descubrir que la prueba no funciona. Los investigadores también incorporan reflexión del modelo sobre lo que salió mal, un mecanismo sencillo que complementa la verificación técnica.

La propuesta contrasta con otros sistemas automatizados que distribuyen un problema entre subtareas y coordinan varios componentes mediante flujos de trabajo predeterminados. h1 prescinde de buena parte de esa estructura, según la descripción del equipo, y atribuye su rendimiento principalmente a una interfaz eficaz con Lean. El artículo no sostiene que toda complejidad sea inútil, sino que, en este sistema, la orquestación elaborada no parece ser el elemento que más contribuye a los resultados.

Resultados en pruebas matemáticas

En PutnamBench, h1 obtuvo 670 puntos de un máximo de 672 al trabajar con GPT-5.5, de acuerdo con los resultados presentados por los investigadores. La cifra se acerca al tope de la evaluación, por lo que deja poco margen para distinguir mejoras dentro de ese conjunto específico de problemas. El desempeño, por tanto, es notable en el benchmark, aunque no debe leerse por sí solo como una medida completa de la capacidad matemática general del sistema.

El sistema también consiguió 90 puntos de 100 en FATE-X, otro referente utilizado para evaluar demostraciones formales. Además, resolvió ocho problemas abiertos de la colección FormalConjectures, que incluye variantes de preguntas matemáticas asociadas con Paul Erdős. Resolver con ayuda de una IA un problema abierto en ese entorno significa producir una demostración formal que el verificador pueda validar, no solo ofrecer una respuesta que parezca plausible en lenguaje natural.

La comparación destacada por el equipo se concentra en problemas de Erdős y en AlphaProof Nexus, el sistema de DeepMind mencionado en el estudio. h1 reportó una tasa de éxito de 82,5%, frente a 76% para AlphaProof Nexus. Estos porcentajes resumen el desempeño en la evaluación indicada y no establecen que h1 sea superior en cualquier área matemática o bajo cualquier configuración de prueba.

La diferencia económica fue mayor que la distancia entre las tasas de éxito: el estudio atribuye a h1 un costo de USD $121 por demostración exitosa, mientras que AlphaProof Nexus registró USD $317. En términos prácticos, esa brecha puede cambiar cuántos intentos resulta razonable dedicar a una conjetura, especialmente si el objetivo es explorar problemas difíciles. Sin embargo, las cifras comparan los sistemas en el contexto descrito por los investigadores y no bastan para anticipar el costo de cualquier uso futuro.

La simplicidad como apuesta de investigación

El título del trabajo alude a la llamada lección amarga, una idea según la cual los métodos generales que aprovechan más cómputo tienden a imponerse, con el tiempo, frente a técnicas especializadas y cuidadosamente elaboradas. Aplicada a la demostración automatizada, esa perspectiva favorece sistemas que dejan más trabajo al modelo y al proceso de verificación, en vez de depender de una planificación compleja diseñada para cada tarea. h1 presenta sus resultados como evidencia a favor de esa orientación.

La investigación continúa una línea previa de Meta en demostración automática, que incluye el sistema neuronal HTPS, presentado en 2022. La diferencia que plantea el nuevo trabajo está en el énfasis: en lugar de concentrarse en construir una búsqueda más inteligente alrededor del modelo, h1 busca que el modelo interactúe directamente con el verificador. Así, el sistema utiliza los errores y las respuestas de Lean como información de trabajo durante la elaboración de la prueba.

Ese giro no elimina la importancia de los modelos subyacentes. Los resultados descritos dependen de modelos de vanguardia y, en particular, la puntuación de PutnamBench de 670 sobre 672 se obtuvo con GPT-5.5. Por eso, el desempeño no puede atribuirse únicamente al diseño mínimo de h1: también depende de la capacidad del modelo conectado al entorno y de la forma en que ambos trabajan juntos.

El sistema tampoco convierte automáticamente cualquier problema matemático en una tarea de bajo costo o de resolución segura. La retroalimentación del verificador permite detectar si una prueba formal satisface las reglas del entorno, pero los resultados citados corresponden a colecciones y comparaciones concretas. Esa distinción importa para interpretar con prudencia las cifras y evitar que un buen resultado en benchmarks se confunda con una demostración de capacidad universal.

Qué indican los costos y qué queda abierto

La diferencia entre USD $121 y USD $317 por prueba exitosa es uno de los datos más prácticos del estudio porque vincula rendimiento con recursos. Si el costo de cada intento baja y la tasa de éxito se mantiene, un equipo podría probar más conjeturas dentro de un presupuesto equivalente. La investigación presenta esa posibilidad como una consecuencia de la eficiencia observada, no como garantía de que todas las conjeturas adicionales vayan a resolverse.

El resultado de PutnamBench exige una cautela particular: 670 de 672 puntos está cerca del máximo, de modo que el benchmark se encuentra casi saturado en esa evaluación. Cuando una prueba deja tan poco espacio para mejorar, una puntuación alta ofrece información sobre el desempeño en sus problemas, pero puede discriminar menos entre sistemas que ya están en la parte superior. Los 90 puntos de 100 en FATE-X y los problemas abiertos de FormalConjectures aportan otros indicadores, aunque tampoco eliminan los límites de cada conjunto.

Según el artículo publicado por Crypto Briefing, los autores plantean que el rendimiento de h1 surge sobre todo de una conexión eficiente con Lean y de la retroalimentación que el modelo recibe durante el proceso. La comparación con AlphaProof Nexus añade un referente de desempeño y costo, pero no equivale a una evaluación de todas las tareas posibles ni de las condiciones en que cada sistema puede operar. La lectura más prudente es que h1 obtuvo resultados competitivos en las pruebas informadas con una arquitectura menos elaborada.

El trabajo deja abierta una pregunta central para la investigación: cuánto de la mejora futura dependerá de simplificar las herramientas y cuánto de los avances en los modelos de lenguaje que las utilizan. También queda por determinar si la ventaja en costo y rendimiento se conserva al ampliar las evaluaciones a otros tipos de problemas y condiciones. Por ahora, h1 ofrece un argumento concreto a favor de combinar modelos potentes, verificación formal y ciclos de retroalimentación directos, sin asumir que más componentes siempre producen mejores demostraciones.


ADVERTENCIA: DiarioBitcoin ofrece contenido informativo y educativo sobre diversos temas, incluyendo criptomonedas, IA, tecnología y regulaciones. No brindamos asesoramiento financiero. Las inversiones en criptoactivos son de alto riesgo y pueden no ser adecuadas para todos. Investigue, consulte a un experto y verifique la legislación aplicable antes de invertir. Podría perder todo su capital.

Suscríbete a nuestro boletín

Artículos Relacionados