Publicación de Manuscritos Matemáticos por OpenAI en GitHub

Detalles sobre la Publicación

OpenAI ha compartido 722 manuscritos matemáticos organizados en 372 familias de resultados en GitHub, provenientes de un modelo interno no divulgado.

Solo 162 de estos manuscritos contienen un resultado principal formalizado en Lean, y la empresa advierte que algunos resultados sin formalización podrían presentar problemas.

Reacciones de Expertos

Andrew Sutherland, matemático del MIT, señala que la afirmación de obtener resultados con un solo intento y un único agente no ha sido verificada y que la publicación no incluye los prompts recomendados por un grupo asesor del Institute for Advanced Study.

“Hasta que se libere el modelo y se puedan replicar los resultados, cualquier afirmación sobre resolver problemas con un solo intento debe ser considerada como no verificada,” afirmó Sutherland.

Características de los Manuscritos

• Los 722 manuscritos están agrupados en 372 «familias» de resultados relacionados.
• OpenAI planteó aproximadamente 4,000 problemas al modelo y publicó lo que consideró como resultados significativos.
• Cada resultado utilizado fue generado en el equivalente a alrededor de tres horas de procesamiento de ChatGPT Pro.

OpenAI publicó resúmenes de razonamiento abreviados para 10 de los resultados, pero solo 162 manuscritos incluidos en el repositorio tienen un resultado principal verificado con el software Lean, lo que representa cerca del 22% del total.

Limitaciones de los Resultados

OpenAI ha indicado que no todos los manuscritos tienen formalizaciones en Lean y que “algunos de los resultados no formalizados podrían tener problemas.” Es importante destacar que una verificación de Lean solo confirma que la prueba sigue la afirmación como está escrita en Lean, pero no garantiza que la afirmación se corresponda con el problema original ni que el resultado sea nuevo o significativo.

Opiniones Divididas en la Comunidad Científica

El Institute for Advanced Study ha expresado su preocupación sobre la capacidad de los modelos de IA para generar argumentos matemáticos sin que los humanos puedan comprenderlos o verificarlos. “La comprensión humana de las matemáticas sigue siendo de suma importancia,” mencionó la institución.

Por otro lado, algunos académicos, como el profesor Abhishek Saha, han mostrado entusiasmo, describiendo la publicación como un gran día para las matemáticas. Sin embargo, Saha también ha notado que la mayoría de los problemas abordados no representan avances revolucionarios.

Recomendaciones y Futuro

El lanzamiento no cumplió con todas las recomendaciones de un grupo asesor, que solicitó la divulgación del nombre del modelo, prompts, un resumen del proceso de razonamiento y los costos de cómputo. OpenAI, sin embargo, planea añadir formalizaciones en Lean a medida que las obtenga y se comprometió a liberar el modelo de manera responsable.

En comparación, Anthropic optó por compartir públicamente todas las 13 millones de líneas de su prueba del Último Teorema de Fermat, formalizando un teorema publicado en 1995.

Conclusiones

La comunidad matemática sigue observando con atención las implicaciones de estas publicaciones y los desafíos relacionados con la verificación y la comprensión humana en el campo de la inteligencia artificial en matemáticas.

Descargo de responsabilidad: Los puntos de vista y opiniones expresadas en este artículo pertenecen a su autor y no necesariamente reflejan aquellas de CriptoPasion. La opinión del autor es a título informativo y en ninguna circunstancia constituye una recomendación de inversión ni asesoría financiera.