🤖 AI

Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

El artículo presenta Theoria, una arquitectura de verificación que mejora la confiabilidad de las respuestas de la IA al reescribir las soluciones en transiciones de estado tipadas y auditables con justificaciones explícitas, superando así a los jueces de LLM holísticos en la detección de premisas ocultas y citas fabricadas, mientras mantiene una alta precisión en problemas de nivel experto.

Autores originales: Ben Slivinski, Michael Saldivar

Publicado 2026-07-02

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Ben Slivinski, Michael Saldivar

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.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 contratando a un arquitecto brillante pero a veces excesivamente confiado para diseñar un puente. No solo quieres el plano final; necesitas saber por qué cada viga se coloca donde se coloca. Si el arquitecto dice: "Esta viga va aquí porque se siente bien", no puedes confiar en el puente. Pero si dice: "Esta viga va aquí debido a la Ley X, y aquí está el cálculo que lo demuestra", entonces puedes verificar las matemáticas.

Este es el problema que Theoria resuelve para la Inteligencia Artificial.

El Problema: Dos formas fallidas de confiar en la IA

Actualmente, tenemos dos formas principales de comprobar si la respuesta de una IA es buena, y ambas tienen deficiencias:

El enfoque del "Matemático" (Asistentes de prueba formal): Esto es como contratar a un robot que solo habla un código matemático estricto e inquebrantable. Es perfecto, pero solo puede entender problemas que ya han sido traducidos a ese código. La mayoría de los problemas del mundo real (como argumentos legales o teorías científicas) son desordenados e informales, por lo que el robot no puede leerlos.
El enfoque del "Sentimiento Intuitivo" (Jueces escalares): Esto es como pedirle a un humano que lea el ensayo de la IA y le dé una puntuación del 1 al 10. Cubre mucho terreno, pero la puntuación es una caja negra. No sabes por qué obtuvo un 7. ¿Pasó por alto una suposición oculta? ¿Inventó una cita? Solo obtienes un número, y no puedes auditarlo después.

La Solución: El detective de "Reescritura de Estados"

Theoria introduce una tercera vía. En lugar de pedirle a la IA que escriba un largo ensayo o que traduzca todo a código matemático, Theoria la obliga a reescribir su respuesta como un registro de cambios de estado paso a paso.

Piénsalo como un archivo de guardado de un videojuego o un sistema de control de versiones (como Git) para el razonamiento.

La Configuración: La IA comienza con un "Estado 0" (el enunciado del problema).
El Movimiento: Para llegar a la respuesta, la IA debe realizar un movimiento hacia el "Estado 1", luego al "Estado 2", y así sucesivamente.
La Regla: Para cada movimiento, la IA debe proporcionar un ticket (una justificación). El ticket solo puede ser de uno de estos tres tipos:
1. Una Cita: "Estoy usando el Teorema X".
2. Un Cálculo: "Hice la cuenta: 2+2=4".
3. Un Dato Dado: "El problema me indicó esto".

El Truco de Magia: "Completitud del Cambio"

Aquí está el ingrediente secreto. Theoria tiene una regla estricta: Cada cambio entre el Estado A y el Estado B debe estar explicado por el ticket.

Si la IA intenta colar una suposición oculta (como "Supongamos que el puente es de oro") sin un ticket, el sistema la atrapa. El "cambio" (añadir la suposición de oro) aparece en el registro, pero el ticket (la justificación) no lo cubre. El sistema grita: "¡Espera! Cambiaste el estado, ¡pero no nos mostraste el recibo!".

Esto obliga a la IA a ser honesta. No puede esconder una mentira en un largo párrafo de texto; tiene que mostrar el momento exacto en que la mentira entró en la conversación.

Cómo funciona en la práctica

El Solucionador (Solver): Una IA intenta resolver un problema.
El Formalizador: Una segunda IA reescribe esa solución en el "Registro de Cambios de Estado" descrito anteriormente. Si el solucionador hizo un salto lógico, el formalizador tiene que registrarlo como un paso específico.
Los Jueces: Especializados en auditoría, los jueces de IA revisan cada paso.
- Un "Juez Matemático" revisa los cálculos.
- Un "Juez de Citas" verifica si el teorema referenciado realmente existe y es aplicable.
- Un "Juez de Hechos" verifica si el dato estaba presente en el problema original.
El Veredicto: Si cada paso tiene un ticket válido, la respuesta es Certificada. Si incluso un paso carece de un ticket o tiene un ticket falso, la respuesta es Rechazada.

Lo que encontró el artículo

Los autores probaron esto en problemas difíciles (como los que se encuentran en exámenes de expertos) y descubrieron:

Alta Confianza: Cuando Theoria dice que una respuesta es correcta, es correcta el 91.4% de las veces.
Mejor para detectar mentiras astutas: Cuando la IA intenta ocultar una premisa (una suposición oculta) o inventar una cita, Theoria la detecta el 90.6% de las veces. Un juez estándar de "sentimiento intuitivo" solo detecta esto el 62.5% de las veces.
No es mágico con errores matemáticos: Si la IA simplemente hace mal una cuenta simple (como decir que 2+2=5), tanto Theoria como el juez estándar la detectan aproximadamente la misma cantidad de veces. La ventaja especial de Theoria es específicamente para detectar lógica oculta y fuentes falsas.
Complementario: Theoria y los jueces estándar fallan en problemas distintos. Si utilizas ambos, puedes detectar casi todos los errores.

La Conclusión

Theoria no intenta hacer a la IA más inteligente; intenta que el razonamiento de la IA sea auditable.

Convierte un ensayo vago y poco fiable en un libro contable transparente de cambios. No promete que todas las respuestas sean correctas (rechaza aproximadamente el 43% de las respuestas porque no puede verificarlas), pero para las respuestas que sí aprueba, puedes revisar el recibo, verificar las matemáticas y saber exactamente por qué es seguro confiar.

En un mundo donde la IA podría alucinar hechos, Theoria es el sistema que dice: "Muéstrame el recibo de cada uno de los pasos, o no daré mi aprobación".

Resumen Técnico: Theoria – Verificación de la Aceptabilidad de la Reescritura sobre Estados de Razonamiento Informal

1. Declaración del Problema

El artículo aborda el "problema de la confianza" en el razonamiento de la IA: distinguir cuándo una respuesta generada por IA debe crear una confianza justificada, particularmente en campos de seguridad crítica (ciencia, derecho, finanzas, medicina). Los enfoques actuales enfrentan una dicotomía:

Asistentes de Prueba Formales (ej. Lean, Coq): Ofrecen certeza matemática pero no logran cubrir la mayoría de las distribuciones de problemas debido al alto costo y la fragilidad semántica de la autoformalización de los requisitos informales en lenguaje natural.
Jueces LLM Escalares: Ofrecen una cobertura amplia pero producen puntuaciones opacas que no pueden ser auditadas, heredan los problemas de coherencia de los LLM y no logran identificar por qué una prueba es defectuosa (ej. premisas ocultas, citas fabricadas).

El desafío central es verificar el razonamiento informal sin requerir una formalización completa, asegurando al mismo tiempo que los errores —específicamente las suposiciones no declaradas y los saltos lógicos— sean visibles y auditables.

2. Metodología: La Arquitectura Theoria

Theoria introduce una arquitectura de verificación que reescribe la respuesta en lenguaje natural de un solucionador en un testigo de prueba (proof witness): una secuencia de transiciones de estado tipadas.

2.1 El Encuadre de la Reescritura

En lugar de tratar una prueba como un bloque de prosa, Theoria la descompone en una trayectoria de estados $(S_0, S_1, \dots, S_n)$ .

Estado ( $S_i$ ): Una lista ordenada de cadenas de texto que representan los hechos establecidos y el objetivo actual.
Transición: Un paso de $S_{i-1}$ $S_{i - 1}$ a $S_i$ $S_{i}$ está licenciado por un tipo de justificación específico:
1. Citación: Un teorema, definición o regla de inferencia.
2. Computación: Manipulación aritmética o simbólica.
3. Dado en el Problema: Hechos declarados explícitamente en el texto del problema.
El Invariante de Completitud del Cambio: Cada diferencia semántica entre $S_{i-1}$ y $S_i$ debe estar contabilizada por la justificación declarada. Si una premisa es necesaria para derivar el nuevo estado pero no está presente en el estado anterior o en la justificación, constituye una mutación no licenciada.

2.2 Pipeline de Verificación

El sistema opera en un bucle: Resolver $\to$ Formalizar $\to$ Juzgar $\to$ Filtrar $\to$ Reparar.

Solucionador (Solver): Propone una solución en lenguaje natural (aumentada con herramientas, ej. búsqueda web).
Formalizador: Reescribe la solución en el testigo de transición de estados. Obliga a que las premisas sean explícitas antes de su uso.
Juzgado Especializado en Paralelo:
- Jueces de Computación: Recomputan los pasos desde cero.
- Jueces de Citación: Verifican la existencia y aplicabilidad de los teoremas citados contra el diferencial (diff) específico del estado.
- Jueces de Datos del Problema: Verifican los hechos contra el texto original.
- Juez del Estado Inicial: Audita $S_0$ para asegurar que no se introduzcan premisas injustificadas al inicio.
- Todos los jueces son instados adversarialmente a encontrar errores en lugar de confirmar la plausibilidad.
Filtro de Pedantería: Distingue entre errores sustantivos y un exceso de rigor respecto a la notación informal o la compresión.
Elevación de Convención (Convention Lift): Permite al sistema aceptar un paso si una convención de dominio estándar y citable resuelve un rechazo, siempre que la suposición se registre explícitamente.
Certificar o Declinar: El sistema emite una decisión binaria. Si todos los pasos pasan (o se resuelven mediante la elevación de convención), la respuesta es Certificada. Si cualquier paso falla y no puede ser reparado dentro de los límites, la respuesta es Declinada.

3. Contribuciones Clave

La contribución principal del artículo no es el uso de múltiples modelos o la comprobación de pasos (que son comunes), sino el formato de testigo específico y sus garantías teóricas:

Garantía de Exposición (Proposición 4.4): El invariante de completitud del cambio convierte las premisas ocultas (brechas de razonamiento global) en mutaciones locales y observables no licenciadas. Una premisa oculta debe aparecer como un nuevo elemento en el estado (activando una verificación de licencia) o violar el invariante. Esto fuerza los errores a la superficie donde pueden ser detectados por jueces locales.
Predicciones de Clase de Error (Proposición 4.5): El formato predice que las ventajas de la verificación se concentrarán en:
- Premisas Ocultas: Expuestas como mutaciones no licenciadas.
- Citaciones Fabricadas: Expuestas porque la evidencia se tipifica explícitamente y se verifica contra el diferencial.
- Sin Ventaja: Los errores aritméticos y las aplicaciones erróneas de teoremas (donde el teorema existe pero se aplica incorrectamente) no reciben una ventaja estructural de exposición sobre la prosa, ya que el error es semántico y no estructural.
Descomposición del Fallo: El artículo distingue entre Fallo de Exposición (el formato oculta el error) y Fallo del Juez (el juez pasa por alto un error expuesto). Theoria busca minimizar el primero, dejando el segundo para ser abordado empíricamente.

4. Resultados Empíricos

La evaluación se realizó en HLE-Verified Gold (185 problemas expertos) y GPQA Diamond (65 problemas científicos de nivel de posgrado).

4.1 Rendimiento en HLE-Verified Gold

Precisión Certificada: 91.4% (96/105 correctos) con un IC de Wilson del 95% de [84.5%, 95.4%].
Cobertura: 56.8% (105/185 problemas certificados).
Asimetría: Las respuestas declinadas fueron aproximadamente 5.0 veces más propensas a estar equivocadas que las certificadas (tasa de error del 42.5% frente al 8.6%).
Comparación con Solver-Solo: Un solucionador aumentado con búsqueda web logró un 83.8% de precisión con un 100% de cobertura. El pipeline de Theoria filtró una parte significativa de los errores, reduciendo la tasa de error en el grupo certificado al 8.6%.
Comparación con Jueces Holísticos: Los jueces LLM holísticos (que asignan una única puntuación de confianza) lograron una precisión comparable (92.4–93.3%) con una cobertura similar. Sin embargo, fallaron en problemas diferentes (índice de Jaccard 0.14–0.36), lo que indica una cobertura de error complementaria.

4.2 Robustez Adversarial

En un benchmark de 95 pruebas envenenadas (inyectando tipos de error específicos):

Detección General: Theoria detectó el 94.7% (90/95) frente al 83.2% (79/95) del juicio holístico ( $p = 0.0017$ ).
Especificidad de Clase de Error:
- Premisas Ocultas: Theoria 90.6% vs. Holístico 62.5% (brecha de 28 pp).
- Citaciones Fabricadas: Theoria 100% vs. Holístico 90%.
- Aritmética/Aplicación Errónea de Teoremas: El rendimiento fue idéntico (~95% y ~93% respectivamente), confirmando la predicción teórica de que el formato no ofrece una ventaja estructural para este tipo de errores.

4.3 Fuera de la Distribución (GPQA Diamond)

Precisión Certificada: 97.1% (33/34).
Cobertura: 52.3%.
La alta precisión en un benchmark diferente sugiere que el límite de "certificar o declinar" está impulsado por la formalizabilidad del razonamiento más que por la calibración específica del benchmark.

4.4 Potencial de Ensamblaje

Debido a que Theoria y los jueces holísticos fallan en conjuntos disjuntos de problemas, las estrategias de ensamblaje (ej. voto por mayoría) lograron un 93.6% de precisión con un 58.9% de cobertura, superando a cualquier método individual.

5. Significado y Reivindicaciones

El artículo afirma que Theoria proporciona un mecanismo de supervisión escalable que cierra la brecha entre la salida bruta de un LLM y la verificación formal.

Auditabilidad: A diferencia de las puntuaciones escalares, Theoria produce un rastro de prueba legible por humanos donde cada paso puede ser desafiado de forma independiente.
Ventaja Estructural: El sistema no depende de que el juez reconstruya una prueba a partir de la prosa. En su lugar, reduce la tarea de verificación a una pregunta local: "¿Esta justificación licencia este cambio de estado específico?".
Complementariedad: El artículo argumenta que Theoria no es un reemplazo para los jueces holísticos, sino un enfoque complementario. El bajo solapamiento de Jaccard en los errores sugiere que combinar arquitecturas de verificación estructuralmente diferentes produce una mayor fiabilidad.
Limitaciones: Los autores reconocen que Theoria no puede detectar errores que no producen una mutación de estado observable (ej. interpretaciones sutiles erróneas de la declaración del problema en $S_0$ ) y que actualmente depende de jueces LLM en lugar de backends formales (como Lean o solvers SMT), aunque está diseñado para ser compatible con ellos.

En resumen, Theoria demuestra que al imponer un invariante de completitud del cambio sobre el razonamiento informal, es posible sacar a la luz las suposiciones ocultas y la evidencia fabricada que la evaluación holística estándar pasa por alto, proporcionando un límite riguroso y auditable para la confianza en el razonamiento generado por IA.