Por que los problemas matematicos son dificiles para los Agents en la practica

Introduccion

Desde hace un tiempo sigo los avances de la IA en la investigacion matematica. Tambien he leido papers, informes de sistemas de Agents y registros publicos de revision.

Este articulo es una organizacion provisional de lo aprendido. Mediante casos concretos, intenta aclarar algunas dificultades actuales en la interseccion entre investigacion matematica e IA, aunque el panorama aun esta lejos de ser completo.

El texto sigue cuatro tipos de dificultad: incertidumbre estrategica, problemas tecnicos interdependientes, acumulacion de errores en pruebas largas y conservacion de informacion util de los intentos fallidos. A partir de implementaciones reales y revisiones de expertos, analizo como surgen estos problemas y por que no son faciles de resolver.

1. Incertidumbre estrategica

La primera dificultad de la investigacion matematica es no saber que ruta de demostracion elegir. Hay un problema mas sutil: el sistema puede encontrar una ruta que parece completa sin poder determinar si realmente ha reducido la dificultad del problema.

1.1 Llamar “lema” a la dificultad central no equivale a resolverla

Consideremos el Problema 3 del segundo lote de evaluacion de First Proof. La propuesta C redujo el problema a dos lemas clave. La revision senalo que la bibliografia citada no contenia ninguno de los dos resultados; incluso una version debilitada de uno de ellos implicaria una forma de la conjetura de Csóka que seguia abierta cuando se hizo la revision. La reduccion posterior era razonable en terminos generales, pero la dificultad central seguia intacta.

Este tipo de fallo puede abstraerse asi:

Si el lema L es cierto, entonces el teorema objetivo T es cierto.

Un Agent demuestra esta implicacion y agrega “demostrar (L)” a la lista de tareas, como si la mayor parte del trabajo ya estuviera hecha. Pero (L) puede ser tan dificil como el problema original, o incluso mas fuerte y mas dificil.

Una reduccion puede tener valor. Transformar un problema desconocido en otro con estructura clara y herramientas maduras ya es un avance.

Sin embargo, desde la perspectiva de ejecucion de un Agent, esto es especialmente peligroso. Si un planificador crea diez subtareas, nueve faciles y una que concentra casi toda la originalidad, una “tasa de finalizacion del 90%” no representa el progreso matematico real.

1.2 Revisar una y otra vez puede significar dar vueltas dentro del mismo marco incompleto

El paper de Momus analiza un flujo existente de solver y verifier. En PB-Adv-011, el sistema solo clasifico las soluciones inyectivas, no descarto las no inyectivas y reconocio explicitamente esa brecha. Aun asi, su verificador interno aprobo la respuesta cinco veces seguidas.

Si el generador sigue reescribiendo el argumento y el verificador solo revisa los resultados locales que ya son correctos, el sistema puede parecer cada vez mas estable sin acercarse a una respuesta completa.

Este caso procede de tareas de demostracion competitiva y no permite inferir directamente la tasa de exito en investigacion matematica abierta. Si revela un mecanismo que conviene evitar: aumentar las iteraciones no garantiza que el sistema abandone su marco de pensamiento original.

2. Dependencias distribuidas

Un problema matematico puede descomponerse, pero despues todas sus partes deben conectarse con precision estricta.

La conexion no se limita a “ejecutar B despues de A”. Incluye el espacio en que vive cada objeto, las hipotesis permitidas, los rangos de parametros, el orden de los cuantificadores y si un resultado anterior es valido bajo las condiciones exigidas mas adelante.

2.1 La version racional esta completa, pero la version entera no

Un caso de investigacion de Danus trata sobre la construccion de clases tangentes de matroides. El sistema completo primero una version con coeficientes racionales, mientras que la tarea original exigia coeficientes enteros. El paper explica que el enunciado usaba el mismo simbolo para un objeto entero y su racionalizacion; esta omision notacional contribuyo al malentendido. Solo cuando una persona senalo la diferencia, el sistema continuo con la version entera.

El caso revela directamente un problema de comprension de la tarea y alineacion con el objetivo. En una colaboracion multi-Agent, la misma ambiguedad puede aparecer en los traspasos: el Agent anterior cree haber entregado el objeto requerido; el siguiente supone que ese objeto satisface una condicion mas fuerte; y el sintetizador final recibe un argumento que parece completo.

Otras diferencias parecidas son “dimension finita” frente a “dimension arbitraria”, o “para cada parametro existe una constante” frente a “existe una constante valida para todos los parametros”. Las expresiones se parecen, pero su significado matematico es distinto.

2.2 El grafo de dependencias rara vez esta completo desde el principio

Un caso de formalizacion de LeanMarathon muestra otra dificultad. Al formalizar una prueba relacionada con el Problema #1196 de Erdős, el sistema siguio una estimacion aparentemente sencilla hasta la monotonicidad de la funcion eta de Dirichlet, y despues hasta comparaciones de orden estocastico de distribuciones Gamma y una representacion de Mellin.

Que una seccion sea corta no significa que dependa de poca matematica. La frase “por metodos estandar” puede invocar todo un conjunto de conocimientos implicitos. Para un Agent de formalizacion, ese conocimiento debe convertirse en teoremas invocables o volver a demostrarse.

La tarea inicial “demostrar la estimacion A” puede transformarse en: A depende de B; B depende de C y D; C requiere una comparacion entre distribuciones; y D exige completar una representacion integral y sus condiciones de aplicabilidad.

No se trata simplemente de agregar pasos. La ejecucion revela que el limite de la tarea inicial no estaba bien entendido.

Ademas, una misma ruta suele requerir que varios lemas sean ciertos a la vez, mientras que rutas diferentes pueden sustituirse. Si falla un nodo, tal vez haya que descomponerlo, modificar una afirmacion anterior o abandonar la ruta completa.

Por eso el “retrabajo local” no consiste solo en volver a llamar al modelo. Si el sistema agrega una hipotesis para demostrar un lema, debe revisar todos los pasos posteriores que dependen de el y comprobar que cumplen la nueva hipotesis.

3. Pruebas largas

A medida que crece un argumento, el sistema debe mantener continuamente definiciones consistentes, hipotesis completas, dependencias validas y la relacion entre resultados locales y el objetivo global.

3.1 Las reglas locales simples no facilitan la demostracion de propiedades globales

El caso de los ciclos de Knuth pide dividir todas las aristas de una clase de grafos dirigidos en tres ciclos hamiltonianos. El paper informa que una construccion supero comprobaciones computacionales para (m\leq 2000), y que dos construcciones produjeron borradores de prueba de 46 y 75 paginas. El reto central es demostrar que reglas locales de enrutamiento breves producen los ciclos deseados para cualquier tamano relevante, no varios ciclos mas cortos.

Un ejemplo sencillo muestra la diferencia.

Supongamos que cada vertice de un grafo dirigido finito tiene exactamente una arista entrante y una saliente. Esa condicion local no garantiza que todos los vertices pertenezcan a un unico ciclo. El grafo puede estar formado por dos ciclos disjuntos.

“Cada regla local es valida” y “la construccion completa tiene la propiedad objetivo” son obligaciones de prueba distintas. Las comprobaciones locales no sustituyen un argumento global ausente, y los experimentos computacionales finitos no sustituyen una prueba para todos los tamanos.

3.2 Convertir hechos aceptados en un paper puede introducir nuevos errores

El equipo de Danus informa que reorganizar y comprimir hechos ya aceptados en un paper legible puede introducir errores.

La razon es sencilla. Convertir varios hechos en una narracion fluida suele exigir conexiones como:

“Por tanto, podemos intercambiar estas dos operaciones.”

“El resultado tambien se aplica al caso limite.”

“Sin perdida de generalidad, podemos fijar un parametro.”

Estas frases parecen editoriales, pero cada una puede contener una afirmacion matematica nueva. Si los resultados aceptados no la cubren, aparece una nueva obligacion de prueba.

Conservar una derivacion completa y generar una demostracion legible son tareas relacionadas, pero distintas. La primera busca no perder informacion; la segunda exige comprimir, reorganizar y explicar. Cuanto mayor es la compresion, mas cuidadosamente hay que revisar que premisas se omitieron y que conexiones se dieron por supuestas.

Las referencias bibliograficas plantean una dependencia similar entre documentos. El informe de Aletheia indica que el entrenamiento en uso de herramientas y el acceso a recuperacion redujeron los titulos y autores inventados, pero persistio otro error: el paper existia, aunque el resultado atribuido no aparecia en el.

3.3 Superar la verificacion formal no basta: hay que confirmar que se verifico la proposicion original

Un estudio de caso sobre colectivos autonomos de investigacion registra una desviacion de objetivo aun mas directa. En la simulacion de los autores, algunos Agents usaron notacion local para ocultar predicados matematicos, haciendo que el problema original se interpretara como una proposicion mas facil. El codigo compilo en Lean, pero no demostro el problema original. Tras incorporarse a la biblioteca compartida, otros Agents lo imitaron.

El sistema exterior no mantuvo de forma fiable la coherencia entre “la proposicion solicitada” y “la proposicion enviada realmente al verificador”.

Hay que distinguir dos preguntas:

Que una proposicion formal haya sido demostrada correctamente y que esa proposicion represente fielmente el problema original no son la misma comprobacion.

4. Intentos fallidos

El fracaso en la exploracion matematica no es un unico tipo de evento.

No encontrar una prueba, hallar un contraejemplo, demostrar un caso especial y descubrir que una hipotesis adicional es indispensable aportan informacion diferente. Comprimirlo todo como “fallo” elimina justamente lo que puede necesitar el siguiente ciclo de investigacion.

4.1 Una prueba rechazada puede contener resultados reutilizables

La propuesta B del Problema 3 de First Proof fue rechazada porque su lema comparativo central tenia un contraejemplo. Sin embargo, la revision confirmo que trataba correctamente (p=1/2) y (p=1), y que excluia correctamente los parametros fuera de ([0,1/3]\cup{1/2,1}). Que la prueba completa falle no invalida cada resultado que contiene.

El caso muestra que un fallo debe tratarse con mas precision que “reintentar” o “abandonar”.

Supongamos que una ruta depende del lema (L) y descubrimos que (L) es falso. Podemos concluir que el argumento dependiente de (L) no puede continuar, pero no que el teorema objetivo (T) sea falso.

Al mismo tiempo, los resultados locales independientes de (L) pueden seguir siendo validos. Aunque falle la version general, tal vez ya exista una prueba para cierto rango de parametros o bajo una condicion adicional.

Esto es extraccion de informacion matematica, no un resumen ordinario del historial de chat.

4.2 El fracaso de una busqueda no es una refutacion matematica

Conviene distinguir tres estados que parecen similares.

“No se encontro una prueba con el presupuesto actual” solo dice que esta busqueda no tuvo exito.

“Una construccion fallo en experimentos computacionales” dice que no funciono en las instancias probadas, pero no descarta otras construcciones.

Solo “existe un contraejemplo que satisface todas las hipotesis y contradice la conclusion” refuta la proposicion correspondiente.

Si un Agent registra el primer estado como el tercero, el siguiente ciclo puede abandonar por error una ruta valida. A la inversa, si un contraejemplo riguroso se reduce a “aqui puede haber un problema”, otros Agents pueden volver a invertir mucho trabajo en el mismo callejon sin salida.

5. Reflexion final

Al observar proyectos de Math Agents como Momus, Aletheia, LeanMarathon y Danus, aparece un principio comun: no tratar la investigacion matematica como una generacion unica de respuesta, sino organizarla como un proceso capaz de revisar, verificar y rastrear dependencias continuamente.

Pero tener un grafo de hechos no hace correctos todos sus hechos. Tener un verificador no impide que el objetivo verificado se desplace. Guardar registros de fallos no garantiza que expresen correctamente su significado matematico. El valor de una arquitectura debe medirse, al final, por su capacidad para proteger estos limites concretos.

El reto central de los problemas matematicos en la practica con Agents no es solo generar razonamientos nuevos. Es mantener con precision las fronteras entre “demostrado”, “cierto bajo condiciones”, “aun no demostrado” y “refutado” durante un proceso continuo de exploracion, descomposicion, revision y olvido.