Teodoro Calonge
Profesor Titular del departamento de Informática en la Universidad de Valladolid
El artículo es de buena calidad. Se trata de alimentar a modelos grandes de lenguaje (LLM) con lo que se denomina RAG (Generación Aumentada por Recuperación).
Lo del RAG es lo que ha motivado que mejorasen en los últimos tiempos los no tan buenos resultados en sus inicios que proporcionó la IA generativa, como ChatGPT. A grandes rasgos, se crearon modelos especializados a base de entrenarlos con RAG especializados en ciertos ámbitos (por ejemplo, derecho, medicina, etc.). A partir de aquí, fue cuando se empezaron a ver resultados mucho mejores.
Esto es lo mismo: se crea o se ajusta un modelo alimentado con demostraciones matemáticas, con la esperanza de que genere (IA generativa) resultados satisfactorios ante problemas nuevos o no vistos por el sistema. Según los autores, ha sido útil para algunos retos, pero ha fracasado para otros muchos.
Por este motivo, creo que este artículo está bien como uno de los primeros intentos de aplicar la IA a la demostración matemática, pero los resultados dicen que hay todavía un gran margen de mejora en este campo.