Cómo un laboratorio chino resolvió el cuello de botella en la demostración matemática impulsada por IA

Las demostraciones matemáticas formales, verificadas por máquinas y no por humanos, son el estándar de oro del rigor. Pero traducir las demostraciones informales que los matemáticos escriben en lenguaje natural a lenguajes formales como Lean sigue siendo un desafío persistente y de largo plazo. Un equipo de la Universidad de Nankín y Polixir Technologies ahora afirma haber resuelto un cuello de botella clave en esa tubería.

Su marco, llamado ToMap (Optimización en Tiempo de Prueba para la Autoformalización de Demostraciones Multiagente), trata la formalización completa de demostraciones no como una única tarea de traducción, sino como un sistema multiagente de tres etapas: un Descomponedor que divide la demostración en unidades atómicas, un Formalizador que convierte cada unidad a sintaxis de Lean, y un Demostrador que genera las tácticas para cerrar cada objetivo. El hallazgo sorprendente, publicado en un preprint, es que el eslabón más débil es la primera etapa, y que centrar el cómputo en mejorar solo la descomposición genera ganancias desproporcionadas.

Análisis del cuello de botella

Para identificar dónde es mejor invertir el cómputo en tiempo de prueba, los investigadores realizaron un experimento de intervención controlada. Bajo trazas de error idénticas de Lean y un presupuesto de corrección fijo, permitieron que solo uno de los tres agentes revisara su producción mientras congelaban a los otros dos. La intervención del Descomponedor logró consistentemente la mayor precisión completa de demostración: 51.1% después de cinco pasadas en la muestra de 184 del ProofFlowBench, frente al 45.1% del Formalizador y el 33.7% del Demostrador.

"El Descomponedor establece la dificultad de cada obligación posterior", escriben los autores. Una descomposición que produce unidades de demostración atómicas y autocontenidas con dependencias explícitas reduce la formalización y la demostración a tareas locales que los agentes posteriores pueden manejar. Las unidades mal delimitadas dejan al ejecutor con objetivos ambiguos o incompletos.

Cómo funciona ToMap

En lugar de distribuir el cómputo en tiempo de prueba entre los tres agentes, ToMap lo concentra en el Descomponedor. Mantiene un conjunto de candidatos de descomposiciones en lenguaje natural, evalúa cada uno según una rúbrica tridimensional (fidelidad semántica, demostrabilidad y amigabilidad con Lean), y utiliza la frontera de Pareto resultante para guiar la evolución iterativa de los avisos de descomposición, una técnica inspirada en el algoritmo GEPA para la optimización reflexiva de avisos.

Una puerta de confirmación reserva el costoso ciclo posterior Formalizador-Demostrador-verificación de Lean para los candidatos que cumplen un umbral mínimo en las tres dimensiones de la rúbrica. "La retroalimentación de la rúbrica es barata y densa, dirigiendo la mayor parte de la búsqueda, mientras que la verificación de Lean proporciona señales de verdad fieles pero costosas, reservadas para candidatos prometedores", explican los autores.

Resultados y comparaciones

En ProofFlowBench, ToMap impulsado por Gemini3-Pro logró una puntuación conjunta de corrección sintáctica y fidelidad semántica del 40.22%, una mejora de 19.0 puntos porcentuales sobre el mejor método anterior, Codex End2End (21.20%). En miniF2F, el conjunto de datos de problemas de competencia de nivel secundario, ToMap alcanzó el 55.74%, una mejora del 8.2%. El sistema también superó a enfoques basados en entrenamiento como ProofBridge, que requiere un modelo de recuperación y un traductor afinado, manteniendo costos de solo inferencia más bajos.

Los estudios de ablación revelan una clara compensación entre tiempo y rendimiento: la mayoría de las ganancias surgen dentro de 3-5 iteraciones de evolución, después de las cuales los rendimientos disminuyen. Esto proporciona una guía práctica para elegir el presupuesto de iteración bajo restricciones de latencia o costo.

"Los métodos que generan una única demostración monolítica de Lean pueden lograr una corrección sintáctica relativamente alta, pero tienen dificultades para traducir fielmente los pasos individuales de las demostraciones en lenguaje natural", señalan los autores. "La formalización paso a paso de la demostración preserva mejor la fidelidad semántica al alinear explícitamente el proceso de formalización con los pasos intermedios de la demostración."

Limitaciones y trabajo futuro

La evaluación se limita a demostraciones a escala de referencia, no a matemáticas largas de nivel de investigación. El sistema también asume que las demostraciones de entrada son correctas; manejar demostraciones informales incorrectas o incompletas sigue siendo un problema abierto. Ampliar el marco para detectar y reparar razonamientos defectuosos se señala como trabajo futuro.

La contribución del equipo de Nankín es menos un avance en la capacidad de razonamiento formal que una demostración de que una asignación inteligente del cómputo en tiempo de prueba, informada por un análisis sistemático de cuellos de botella, puede extraer más valor de los modelos existentes que simplemente escalar enfoques monolíticos. Para la creciente comunidad que trabaja para puentear las matemáticas informales y formales, esa idea puede resultar tan valiosa como los propios puntos de referencia.