Resumen Técnico: Escalado de la Computación en Tiempo de Prueba Basada en Grafos de Lenguaje Natural para la Demostración Automática de Teoremas

Declaración del Problema

Aunque los Modelos de Lenguaje de Gran Escala (LLM) han demostrado capacidades en el razonamiento lógico de múltiples pasos, la demostración automática de teoremas sigue siendo un desafío. Los obstáculos específicos incluyen la identificación precisa de conceptos matemáticos clave, la comprensión de sus interrelaciones y la formalización correcta de pruebas dentro del lenguaje natural o de sistemas formales. Los enfoques existentes suelen depender de un ajuste fino intensivo, iteración de expertos o entrenamiento sobre grandes volúmenes de datos formales (por ejemplo, Lean), lo cual puede ser pesado en recursos y limitar la capacidad del modelo para aprovechar conocimientos matemáticos más amplios e informales. Además, los enfoques puramente formales pueden tener dificultades con la flexibilidad del razonamiento natural, mientras que los enfoques puramente en lenguaje natural enfrentan ambigüedad al traducirse a sistemas de verificación formal.

Metodología: KG-Prover

Los autores presentan KG-Prover, un marco novedoso que aumenta los LLM de propósito general con un grafo de conocimiento (KG) extraído de textos matemáticos de prestigio (específicamente ProofWiki) para construir y formalizar pruebas. El sistema opera sin un ajuste fino adicional del LLM base, dependiendo en cambio del escalado de la computación en tiempo de prueba y de la generación aumentada por recuperación.

Componentes Principales

1. Construcción del Grafo de Conocimiento:

   • Fuente: El grafo se construye analizando ProofWiki, extrayendo nodos de espacios de nombres como "Definición", "Axioma" y "Prueba".
   • Estructura: Cada nodo representa una afirmación matemática autocontenida (por ejemplo, una proposición de teorema o una definición). Las aristas representan los hipervínculos encontrados dentro del texto, capturando dependencias y relaciones conceptuales.
   • Escala: El grafo resultante contiene más de 60.000 nodos y 300.000 aristas.
   • Incrustaciones: Los nodos se complementan con vectores de incrustación precalculados (utilizando text-embedding-3-large) para facilitar la recuperación semántica.

2. Pipeline de Inferencia:

   • Recuperación y Recorrido: Dada una proposición $P$, el sistema calcula su incrustación y recupera los $k$ nodos más similares. Si el intento inicial de prueba falla, el sistema expande iterativamente el contexto recorriendo el grafo hasta una profundidad $d$, seleccionando los $k$ vecinos más cercanos de los nodos visitados previamente.
   • Generación de Prueba Informal: El LLM genera una prueba informal en lenguaje natural utilizando el contexto recuperado. Esto aprovecha las capacidades de razonamiento emergentes del modelo y el amplio corpus de pruebas informales disponibles en el KG.
   • Autoformalización: Un modelo separado (DeepSeek-Prover-V1.5) traduce la prueba informal a código Lean 4.
   • Verificación y Refinamiento: El código Lean generado se verifica utilizando el demostrador de teoremas Lean 4. Si la verificación falla, los mensajes de error se retroalimentan al autoformalizador para su refinamiento. Si la prueba sigue fallando, el sistema puede aumentar la profundidad del recorrido del grafo o emplear estrategias de búsqueda.

3. Estrategias de Escalado (Computación en Tiempo de Prueba):

   • Mejor de N: El sistema genera $n$ pruebas informales independientes, las autoformaliza y utiliza un modelo "juez" dedicado para puntuarlas basándose en la corrección y la claridad, seleccionando al candidato con la puntuación más alta.
   • Búsqueda en Haz: Los candidatos de prueba se organizan en un haz de ancho $w$. En cada paso, los candidatos se expanden basándose en la retroalimentación del verificador, se puntuán y se retienen los mejores $k$ para la siguiente iteración. Esto equilibra la exploración de diversas rutas de prueba con el refinamiento impulsado por la verificación.

Contribuciones Clave

• Marco KG-Prover: Un sistema que integra la generación de pruebas informales en lenguaje natural con un recorrido iterativo basado en grafos de conocimiento y un mecanismo de LLM como juez, eliminando la necesidad de entrenamiento especializado o iteración de expertos.
• KG Matemático a Gran Escala: La construcción de un grafo de conocimiento a partir de ProofWiki con más de 60.000 nodos y más de 300.000 aristas, modelando relaciones complejas entre conceptos matemáticos.
• Sistema de Refinamiento Iterativo: Un mecanismo de evaluación heurística y búsqueda en haz que mejora el rendimiento hasta en un 26,4% sobre las líneas base y un 21,8% sobre las configuraciones de KG-Prover sin escalado.
• Demostración de Escalado en Tiempo de Prueba: Evidencia de que modular la profundidad del recorrido del grafo y emplear estrategias de búsqueda (Mejor de N, Búsqueda en Haz) aumenta significativamente el rendimiento sin reentrenar los modelos subyacentes.

Resultados Experimentales

El marco se evaluó en tres puntos de referencia: miniF2F-test, ProofNet y MUSTARDSAUCE.

• Ganancias de Rendimiento:

  • KG-Prover superó consistentemente a los sistemas base y a la Generación Aumentada por Recuperación (RAG) estándar en todos los conjuntos de datos.
  • Las mejoras oscilaron entre un 2% y un 11% sobre las líneas base en múltiples modelos (Llama 3.1 8B, GPT-4o, o1-mini, etc.).
  • En miniF2F-test, los LLM de propósito general mejoraron hasta un 21% cuando se combinaron con KG-Prover.
  • La configuración de KG-Prover con o4-mini logró una tasa de éxito del 50% en miniF2F-test.
  • En la configuración de escalado más alta, las mejoras alcanzaron un 26,4% sobre las líneas base.

• Efectos de Escalado:

  • Profundidad de Recorrido: La precisión aumentó con una mayor profundidad de recorrido ($r$), particularmente para modelos de parámetros más pequeños como Llama 3.1 8B. Los primeros aumentos de profundidad produjeron las ganancias más significativas.
  • Estrategias de Búsqueda: Combinar el KG con Búsqueda en Haz y muestreo Mejor de N mejoró aún más la precisión, logrando hasta un 10,75% en ProofNet y un 50,40% en MUSTARDSAUCE.
  • Modelos Ajustados Fino: Incluso cuando se aplicó a modelos ya ajustados fino para Lean (por ejemplo, TheoremLlama, DeepSeek-Prover-V1.5), KG-Prover proporcionó ganancias adicionales de rendimiento (por ejemplo, +1,85% sobre una línea base ajustada fino en miniF2F).

Significado y Afirmaciones

El artículo postula que KG-Prover ofrece un enfoque prometedor y escalable para la demostración automática de teoremas que no requiere ajuste fino adicional ni iteración intensiva de expertos. Al aprovechar las capacidades de razonamiento en lenguaje natural integradas en los LLM de propósito general y aumentarlas con información estructurada recuperada mediante grafos, el marco cierra eficazmente la brecha entre el razonamiento informal y la verificación formal.

Los autores enfatizan que este método permite que los modelos base existentes logren un rendimiento comparable o superior al de sistemas especializados y ajustados fino simplemente inyectando conceptos relacionados durante la inferencia. El trabajo destaca el potencial del escalado de la computación en tiempo de prueba —modular la profundidad del recorrido del grafo y emplear estrategias de búsqueda— como una alternativa viable al escalado de parámetros del modelo para tareas de razonamiento complejo. Aunque el enfoque introduce desafíos en el paso de traducción de informal a formal, el sistema de dos agentes (generación + autoformalización) respaldado por la recuperación de grafos mitiga exitosamente estos problemas, proporcionando trazas de razonamiento interpretables y estrategias novedosas para la generación de pruebas.