Theoria conecta prueba formal y jueces LLM con verificación auditable

Un artículo publicado el 1 de julio en arXiv presenta Theoria, una arquitectura de verificación que se sitúa entre asistentes de prueba formal frágiles y jueces LLM opacos. En lugar de requerir Lean o Coq, Theoria reescribe soluciones candidatas en transiciones de estado tipadas, cada una requiriendo justificación explícita — una cita, computación o hecho dado por el problema — antes de que la transición sea autorizada. En HLE-Verified Gold (185 problemas solo de texto de expertos), Theoria certifica 105 soluciones con precisión estricta del 91,4% (IC 95% Wilson [84,5%, 95,4%]). En GPQA Diamond (n=65), la precisión certificada alcanza el 97,1% (IC Wilson [85,1%, 99,5%]).

El diseño central es lo que los autores llaman el invariante de "completitud del cambio": toda diferencia entre estados de prueba consecutivos debe contabilizarse. Las premisas ocultas—la clase de error más asociada con salidas de LLM que suenan confiadas pero son incorrectas—emergen como mutaciones no autorizadas en lugar de pasar silenciosamente. Esta es la garantía estructural que los jueces escalares no pueden hacer. Una puntuación de 0,87 no te dice nada sobre qué paso falló o por qué.

En 95 pruebas envenenadas adversarialmente en 15 dominios, Theoria detecta el 94,7% de los errores inyectados versus el 83,2% para juzgamiento holístico de LLM (p=0,0017), una brecha de 11,5 puntos porcentuales. La brecha no se distribuye uniformemente. Para premisas ocultas, Theoria detecta el 90,6% versus el 62,5% para juzgamiento holístico — una delta de 28 pp donde el análisis formal predice una ventaja. Para citas fabricadas, Theoria alcanza el 100% versus el 90%. Para errores aritméticos y aplicación incorreta de teoremas, ambos enfoques funcionan idénticamente. Las victorias de la arquitectura rastrean las clases de error donde la trazabilidad a nivel de estado tiene una ventaja estructural.

Para estrategias de conjunto, la complementariedad importa. Los jueces LLM holísticos logran precisión comparable en cobertura equiparada. La superposición de Jaccard entre lo que Theoria certifica y lo que los jueces holísticos aprueban es 0,14–0,36 — genuinamente disperso, no ruido correlacionado. Ejecutar ambos en un pipeline por etapas—Theoria para certificación rigurosa de salidas de alto riesgo, jueces holísticos para filtrado inicial rápido—no es redundante. Los dos métodos fallan en diferentes problemas por diseño.

Theoria no elimina el trueque de cobertura. De 185 problemas de HLE-Verified Gold, 105 fueron certificados; 80 no lo fueron. Los asistentes de prueba formal cubren incluso menos de la distribución real de problemas. Una estimación reciente sitúa los mejores LLMs probadores en el 13% de PutnamBench resuelto formalmente, versus aproximadamente el 83% para LLMs de razonamiento informal. La zona de Theoria es razonamiento informal hecho auditable, no prueba formal de teoremas disfrazada.

Cada certificación Theoria produce un seguimiento de prueba legible por humanos en el cual cada paso puede ser desafiado independientemente después del hecho. Esta es la propiedad de pista de auditoría que los equipos orientados al cumplimiento no han tenido. Una puntuación de juez escalar no es un registro. Un seguimiento de transición de estado tipado con justificaciones explícitas en cada paso sí lo es. Si ese seguimiento satisface revisiones regulatorias o de seguridad específicas es una cuestión de despliegue, pero el artefacto ahora existe para responderla.

Para equipos de plataforma ML que envían canalizaciones de agentes en contextos de codificación, planificación o finanzas, la pregunta práctica es dónde en la pila insertar el verificador de Theoria. No es una protección en tiempo de ejecución—reescribir soluciones en transiciones de estado tipadas no es una operación de costo cero. Se posiciona mejor como una puerta post-generación para salidas que disparan decisiones de alto riesgo, o como una capa de auditoría en modo lote para registros de producción. Los equipos que ya ejecutan evaluaciones de LLM-como-juez deben tratar Theoria como una capa aditiva, no un reemplazo, dada la superposición de Jaccard de 0,14–0,36.

El código y detalles de referencia aún no están vinculados públicamente en el resumen de arXiv. Esté atento a un lanzamiento de repositorio de Ben Slivinski y Michael Saldivar.