🤖 machine learning

Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game

Este trabajo introduce el Juego de Números Naturales Ofuscado como un punto de referencia para evaluar el "Razonamiento Arquitectónico"—la capacidad de sintetizar pruebas utilizando únicamente axiomas locales sin pistas semánticas—y demuestra que, mientras que los modelos de lenguaje grandes generales sufren una degradación del rendimiento bajo ofuscación, los modelos de razonamiento especializados mantienen su precisión, distinguiendo así el razonamiento lógico genuino de la coincidencia de patrones.

Autores originales: Lixing Li

Publicado 2026-05-04

📖 4 min de lectura☕ Lectura para el café

CC0 1.0

Autores originales: Lixing Li

Artículo original dedicado al dominio público bajo CC0 1.0 (http://creativecommons.org/publicdomain/zero/1.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que estás enseñando a un estudiante a resolver un acertijo matemático. Por lo general, el acertijo viene con etiquetas útiles como "Suma", "Multiplicación" o "Sucesor". Un estudiante inteligente podría no entender realmente las reglas del juego; podría simplemente reconocer la palabra "Suma" y recordar un truco memorizado que ha visto antes.

Este artículo plantea una pregunta difícil: ¿Están estos modelos de IA realmente haciendo matemáticas, o simplemente son buenos reconociendo palabras?

Para averiguarlo, los investigadores crearon una versión "vendada" de un famoso juego matemático llamado Natural Number Game. Así es como lo hicieron y lo que descubrieron, explicado de forma sencilla:

El Experimento: El Juego "Alienígena"

Los investigadores tomaron un juego matemático estándar donde cada regla y número tiene un nombre claro (como add o zero). Luego, aplicaron un "desordenador" a él. Reemplazaron cada nombre significativo con cadenas aleatorias y sin sentido como x9z, q22 y b7a.

El Juego Original: Ves add y sabes que significa suma.
El Juego Desordenado (NNG Ofuscado): Ves x9z y no tienes idea de lo que significa. No puedes adivinar; debes observar la lógica de cómo encajan las piezas para descubrir qué hace x9z.

Esto pone a prueba algo que los autores llaman "Razonamiento Arquitectónico". Es la capacidad de construir una solución utilizando únicamente los planos estructurales (la lógica), ignorando las señales útiles en las puertas (los nombres).

Los Resultados: El "Impuesto de Latencia"

Los investigadores probaron varios modelos de IA de primer nivel tanto en el juego original como en el desordenado. Descubrieron dos cosas principales:

1. El "Impuesto Universal de Latencia" (Todos se vuelven más lentos)
Cuando los nombres se desordenaron, cada modelo de IA tardó más en resolver los problemas.

Analogía: Imagina que conduces a una cafetería familiar. Conoces las señales, los nombres de las calles y los puntos de referencia. Ahora, imagina que alguien pintó sobre todas las señales y renombró las calles con letras aleatorias. Aún sabes conducir, pero tienes que detenerte, mirar el mapa y pensar más a fondo en cada giro. Llegas eventualmente, pero toma mucho más tiempo.
El Hallazgo: Los modelos de IA tuvieron que realizar esta "reconstrucción del mapa mental" para cada problema. No podían simplemente confiar en la memoria; tenían que procesar la lógica cruda, lo que les costó tiempo.

2. La División entre "Razonamiento" y "Memorización"
Aunque todos se volvieron más lentos, la precisión de los modelos se dividió en dos grupos distintos:

Los Modelos "Generales" (por ejemplo, GPT-4o, Claude): Estos modelos son como estudiantes que son excelentes memorizando tarjetas de estudio. Cuando los nombres se desordenaron, se confundieron. Su tasa de éxito disminuyó significativamente.
- Lo que esto significa: Estaban confiando en las "señales" (los nombres) para resolver el acertijo. Cuando las señales desaparecieron, no pudieron encontrar el camino.
Los Modelos de "Razonamiento" (por ejemplo, DeepSeek-R1, GPT-5, DeepSeek-Prover-V2): Estos modelos son como estudiantes que realmente entienden las reglas del juego. Incluso cuando los nombres se desordenaron, su tasa de éxito se mantuvo exactamente igual.
- Lo que esto significa: No necesitaban las etiquetas. Observaron la estructura lógica (la "arquitectura") y descubrieron la solución tan bien como antes.

La Conclusión

El artículo concluye que existe una diferencia real entre la IA que simplemente coincide con patrones (como reconocer la palabra "add") y la IA que puede razonar verdaderamente a través de estructuras lógicas.

Los modelos generales son como turistas que necesitan una guía con nombres. Si les quitas la guía, se pierden.
Los modelos de razonamiento son como arquitectos que pueden leer los planos. Incluso si el edificio no tiene señales, aún pueden descubrir cómo encajan las paredes y las vigas.

El estudio demuestra que, aunque todos los modelos de IA se vuelven "más lentos" cuando se les obliga a pensar sin etiquetas, solo los verdaderos modelos de "razonamiento" pueden mantener su precisión alta en este entorno "alienígena". Esto sugiere que, para que la IA descubra nuevas matemáticas en el futuro (donde aún no existen nombres ni etiquetas), necesitamos estos modelos centrados en el razonamiento, no solo aquellos que son buenos coincidiendo patrones.

Aquí se presenta un resumen técnico detallado del artículo "Evaluación de las Capacidades de Razonamiento Arquitectónico de los Provers LLM mediante el Juego de Números Naturales Ofuscado."

1. Planteamiento del Problema

A pesar del éxito de los Modelos de Lenguaje Grandes (LLM) en benchmarks de matemáticas formales como MiniF2F y PutnamBench, persiste una ambigüedad crítica: ¿poseen estos modelos capacidades de razonamiento lógico genuino, o simplemente están realizando coincidencia de patrones semánticos contra sus datos de pre-entrenamiento?

La Brecha: Los benchmarks actuales a menudo dependen de la recuperación de bibliotecas (por ejemplo, Mathlib), donde el éxito depende del reconocimiento de lemas de alto nivel e identificadores semánticos (por ejemplo, add, succ). Esto falla al probar la capacidad de un modelo para sintetizar pruebas en dominios matemáticos "alienígenas" donde no existen bibliotecas externas ni pistas semánticas familiares.
La Necesidad: Para lograr el descubrimiento automatizado de teoremas, la IA debe demostrar Razonamiento Arquitectónico: la capacidad de sintetizar pruebas formales utilizando únicamente axiomas locales, definiciones y lógica estructural, independientemente del significado semántico o de repositorios externos.

2. Metodología

Los autores introducen el Juego de Números Naturales Ofuscado (O-NNG), un benchmark de conocimiento cero diseñado para aislar el razonamiento estructural de la recuperación léxica.

A. El Algoritmo de Ofuscación

La innovación central es la eliminación sistemática de pistas semánticas del Juego de Números Naturales (NNG) en Lean 4:

Nivel de Ruido ( $\lambda$ ): Definido en el rango $[0, 1]$ $[0, 1]$ .
- $\lambda = 0$ : NNG original (identificadores semánticos intactos).
- $\lambda = 1.0$ : Aleatorización completa de identificadores.
Mecanismo de Perturbación: Una relación exponencial $P = \lambda^{2.5}$ $P = λ^{2.5}$ determina la probabilidad de perturbaciones a nivel de carácter.
- Sustitución: Reemplaza caracteres por candidatos válidos de Unicode/ASCII.
- Inserción: Inyecta nuevos caracteres (probabilidad $0.4P$ ).
- Borrado: Elimina caracteres (probabilidad $0.3P$ ), asegurando que los identificadores permanezcan no vacíos.
Objetivo: Este proceso transforma el conjunto de datos en un "entorno cerrado" donde los identificadores (por ejemplo, axiomas, teoremas, tácticas) son cadenas aleatorias, obligando al modelo a depender exclusivamente de la estructura lógica de los axiomas de Peano.

B. Configuración Experimental

Conjunto de Datos: 68 problemas formales del NNG, organizados en 8 módulos (Suma, Multiplicación, etc.).
Modelos Evaluados: Cinco modelos de última generación a través de API:
- Modelos de Razonamiento: DeepSeek-R1, GPT-5, DeepSeek-Prover-V2.
- Modelos Generales: GPT-4o, Claude-Sonnet-4.5.
Pipeline:
1. Análisis: Extracción del NNG con ordenamiento estricto de dependencias.
2. Ofuscación: Aplicación de perturbaciones a nivel de carácter basadas en $\lambda$ .
3. Generación de Consultas: Construcción de prompts que contienen axiomas "alienígenas", teoremas objetivo y tácticas disponibles.
4. Inferencia: Los modelos generan una salida JSON con un plan en lenguaje natural ("Borrador") y código Lean 4 ("Código").
5. Verificación: Validación automatizada utilizando el compilador Lean 4 (v4.27.0) para verificar errores de sintaxis y lógica.
Métricas:
- Tasa de Correctitud (%): Proporción de teoremas probados con éxito.
- Tiempo Promedio (s): Latencia de inferencia.

3. Contribuciones Clave

Definición de Razonamiento Arquitectónico: Formalizado como la capacidad de sintetizar pruebas utilizando exclusivamente definiciones y axiomas locales dentro de una teoría cerrada, excluyendo bibliotecas externas y tácticas automatizadas de alto nivel (como linarith).
El Benchmark O-NNG: Un marco de evaluación novedoso de conocimiento cero que cuantifica la "Brecha Semántico-Razonamiento" midiendo la degradación del rendimiento cuando se eliminan los identificadores semánticos.
Cuantificación del "Impuesto de Latencia": Se estableció que navegar por dominios alienígenas impone un costo computacional universal (aumento del tiempo de inferencia) en todos los modelos, independientemente de su arquitectura.

4. Resultados y Análisis

El estudio revela una divergencia aguda en el comportamiento de los modelos cuando se eliminan las pistas semánticas:

Impuesto Universal de Latencia:
- Todos los modelos mostraron un aumento estadísticamente significativo en el tiempo de inferencia a medida que aumentaba $\lambda$ .
- Implicación: Eliminar los identificadores semánticos obliga a los modelos a realizar búsquedas internas más intensivas o reconstrucción lógica, independientemente de su capacidad base.
Divergencia en Robustez (Precisión):
- Modelos de Razonamiento (DeepSeek-R1, GPT-5, DeepSeek-Prover-V2): Mantuvieron una precisión estable en todos los niveles de ruido ( $\lambda \in [0, 1]$ $λ \in [0, 1]$ ). La caída en el rendimiento no fue estadísticamente significativa.
  - Conclusión: Estos modelos dependen de la lógica estructural y pueden navegar por los axiomas de Peano sin anclas semánticas.
- Modelos Generales (GPT-4o, Claude-Sonnet-4.5): Sufrieron una caída estadísticamente significativa en las tasas de éxito a medida que aumentaba $\lambda$ $λ$ .
  - Conclusión: Su rendimiento en tareas formales estándar depende en gran medida de la coincidencia de patrones semánticos y la familiaridad con las convenciones de nomenclatura, en lugar de la síntesis lógica pura.
Significancia Estadística: Un ANOVA de un factor confirmó que la caída en el rendimiento de los modelos generales y el aumento de latencia para todos los modelos fueron estadísticamente significativos ( $p < 0.05$ ).

5. Significado e Implicaciones

Evaluación del Razonamiento Verdadero: O-NNG proporciona una métrica rigurosa para distinguir entre modelos que "conocen" las matemáticas mediante coincidencia de patrones y aquellos que pueden "razonar" mediante lógica estructural.
Dirección Arquitectónica: Los resultados sugieren que para el futuro del descubrimiento automatizado de teoremas (AI4Math), las arquitecturas centradas en el razonamiento (como DeepSeek-R1 y GPT-5) son superiores a los modelos de propósito general, ya que son robustas ante la ausencia de priores semánticos.
El "Valle Inquietante del Razonamiento": Los datos sugieren una relación no lineal donde el ruido parcial podría ser más perjudicial que la ofuscación total, indicando que las pistas semánticas residuales pueden actuar como heurísticas distractores.
Futuros Agentes de IA: Los hallazgos abogan por el desarrollo de "Agentes Semánticos Anclados al Conocimiento" capaces de operar en dominios con ontologías incompletas u oscurecidas, un prerrequisito para descubrir teoremas matemáticos novedosos.

En resumen, el artículo demuestra que, si bien los LLM actuales pueden resolver problemas conocidos mediante coincidencia de patrones, solo arquitecturas específicas de "razonamiento" poseen el Razonamiento Arquitectónico necesario para resolver problemas en entornos lógicos completamente desconocidos y ofuscados.