ProofOfThought: razonamiento basado en LLM usando pruebas de teoremas con Z3

• ProofOfThought combina modelos grandes de lenguaje (LLM) con el demostrador de teoremas Z3 para ofrecer un razonamiento sólido e interpretable
• Este proyecto proporciona resultados de razonamiento precisos y confiables para consultas en lenguaje natural
• A través de una API de alto nivel en Python, los desarrolladores pueden implementar y experimentar fácilmente con tareas de razonamiento complejas
• Mediante Z3DSL, también ofrece acceso a un DSL de bajo nivel basado en JSON, lo que permite una personalización flexible
• Su publicación en el Sys2Reasoning Workshop NeurIPS 2024 muestra las ventajas de llevar resultados de investigación recientes a aplicaciones prácticas

---

Introducción al proyecto open source ProofOfThought

ProofOfThought es una biblioteca open source de razonamiento que adopta un enfoque de síntesis de programas neuro-simbólica que combina modelos grandes de lenguaje (LLM) con el demostrador de teoremas Z3. Su capacidad de ofrecer resultados de razonamiento robustos e interpretables para problemas complejos del mundo real le da una relevancia importante tanto en uso práctico como en investigación.

Por su naturaleza open source, cualquiera puede usarlo libremente para investigación, servicios o desarrollo, y tiene la ventaja de que facilita la verificación del proceso de razonamiento y la interpretación de errores frente a los sistemas de razonamiento tradicionales basados solo en LLM. En comparación con otros sistemas de razonamiento, su gran distintivo es la transparencia estructural de su flujo: entrada en lenguaje natural → conversión automática a programa lógico → razonamiento basado en Z3.

Arquitectura del sistema y componentes principales

• API de alto nivel (z3dsl.reasoning) :

  • Ejecuta consultas de razonamiento basadas en lenguaje natural
  • Ofrece una interfaz en Python fácil de aplicar incluso para principiantes

• DSL de bajo nivel (z3dsl) :

  • Permite acceder al demostrador de teoremas Z3 con base en JSON
  • Resulta conveniente para personalizaciones complejas y la construcción de pipelines de automatización

Ejemplos de funciones principales

• El LLM convierte la consulta de entrada en una fórmula lógica (programa simbólico)

• A través del demostrador Z3, genera resultados de verdadero/falso (yes/no) o interpretaciones basadas en condiciones

• Ejemplo:

  • Consulta: "¿Nancy Pelosi condenaría públicamente el aborto?"
  • Resultado: False (no)

• Incluye un pipeline de evaluación (EvaluationPipeline):

  • Permite evaluación por lotes sobre datasets grandes
  • Reportes automáticos de exactitud y otras métricas

Casos de aplicación y uso

• Automatización de benchmarks de razonamiento con fines de investigación
• Servicios de prueba automática para grafos de conocimiento basados en LLM o problemas de lógica de orden superior
• Posibilidad de aplicarse a diversos servicios de IA, como consultas complejas sobre políticas o clasificación automática de debates en lenguaje natural

Relevancia académica y características

• Presentado en el workshop Sys2Reasoning de NeurIPS 2024
• Confiabilidad basada en interpretación simbólica que complementa las limitaciones existentes de los LLM (incertidumbre en el razonamiento)
• La transparencia y la interpretabilidad de los resultados y sus fundamentos son una gran fortaleza para el desarrollo de servicios reales

Conclusión

ProofOfThought combina las fortalezas de los LLM y del demostrador de teoremas Z3 para ofrecer valor práctico a desarrolladores e investigadores que buscan construir una infraestructura de razonamiento de IA robusta e interpretable. La licencia y la estructura del proyecto están diseñadas para encajar bien en el ecosistema open source, por lo que resulta atractivo tanto para la investigación académica como para el uso industrial.

[GN⁺]

Opiniones de Hacker News

• Comparte una experiencia interesante con Gemini 2.5 Pro. Mientras intentaba resolver un sistema de ecuaciones en un sistema CAS en línea, el CAS no funcionó como esperaba, así que le pidió ayuda a Gemini, y Gemini le dio directamente la solución. Explica que usó el paquete sympy de Python. Comparte la impresión de que la combinación de un LLM ambiguo con herramientas estrictas puede producir un efecto muy potente
  • Se siente parecido a los humanos. Somos malos para cálculos complejos, pero construimos computadoras increíbles que los hacen muy bien. Y después de un esfuerzo enorme, también creamos programas que, basados en cálculo numérico, más o menos predicen texto, aunque sean torpes para cálculos difíciles. Al final, este programa termina pudiendo predecir cómo crear y usar programas que sí son buenos para cálculos numéricos
  • Realmente me encanta la combinación de LLM y sympy para matemáticas. Si haces que el LLM escriba código de sympy, puedes confiar en que la manipulación simbólica se realizó correctamente. El código mismo queda como entregable y puede ser corregido y mejorado gradualmente por una persona o por otro LLM, además de poder gestionarse con historial de git y similares. La confianza en la precisión matemática se mantiene al pasar pruebas y validaciones. También uso funciones auxiliares para convertir fácilmente el código de sympy a LaTeX. Recientemente también trabajé así en matemáticas relacionadas con el experimento de quantum eraser. enlace de github
  • Entiendo que seguir el proceso de resolución del problema junto con un LLM usando herramientas es un método razonable. De hecho, funcionó mejor de lo esperado. Pero no usar un CAS y en su lugar hacer que el LLM procese las matemáticas es como mudarte de departamento haciendo varios viajes en autobús en vez de usar un camión de carga. Esa es la opinión, aunque ya tengas pase de autobús
• Se enfatiza que un LLM al final es un modelo estadístico del lenguaje. Según la experiencia, generar programas lógicos, especialmente código fuente en Prolog, funciona mejor de lo esperado. Probablemente porque Prolog se introdujo en el procesamiento simbólico del lenguaje natural y hay abundantes ejemplos de traducción en los datasets de entrenamiento. También vale la pena considerar usar la sintaxis Datalog de Z3 en lugar de la sintaxis SMTLib. Se recomienda consultar la demo relacionada y la sintaxis Datalog de Z3
  • La sintaxis Datalog en Z3 es bastante buena. En nuestro paper sobre grammars usamos SMT porque era lo más compatible con distintos solvers. Pero probamos durante el proceso de revisión de NeurIPS que ese enfoque también funciona bien con PROLOG. Esperamos que también funcione con Datalog. enlace al paper, ejemplo de datalog
• Parece un enfoque interesante. Nuestro equipo también creó de forma similar un prototipo que codifica políticas operativas del negocio con LEAN. Primero, el LLM convierte la base de conocimiento del wiki interno o de Google Docs a código LEAN. Luego se ejecuta un solver para verificar consistencia. Cuando se modifica el wiki, se vuelve a correr todo el proceso, funcionando como una especie de linter de procesos. Aun así, como la conversión a LEAN en sí requiere revisión de ingenieros, se quedó en fase de prototipo. Pero parece una vía prometedora para dominios que requieren cumplimiento legal y financiero
  • Se menciona que la barrera de la formalización automática es realmente alta. Comparte la experiencia de haber analizado cuantificando la incertidumbre de la formalización automática sobre gramáticas bien definidas en su paper de NeurIPS 2025. enlace al paper, y si alguien quiere una discusión más detallada, puede contactarlo en cualquier momento
  • Para quienes se preguntan qué es LEAN, se presenta como Lean Theorem Prover, creado por Microsoft. enlace al proyecto
  • Tengo curiosidad por ver ejemplos reales. Me gustaría escuchar qué tipo de políticas están descritas con suficiente precisión en el mundo real como para definirlas en LEAN
  • Parece muy útil que este enfoque permita identificar de forma sistemática lineamientos que se contradicen entre sí
• Es un campo de investigación muy interesante. Hace unos años verifiqué con motores de razonamiento basados en lógica y probabilidad si las premisas realmente llevaban bien a las conclusiones. También usé agentes para sintetizar, formalizar y criticar conocimiento de dominio. No es una bala de plata, pero sí podía garantizar cierto nivel de precisión. Creo que cierto grado de simbolismo y el concepto de agent-as-a-judge son prometedores para el futuro. paper de referencia
  • Leí esa investigación. Está bastante buena. Yo también recientemente tuve experiencia creando un agente de autoformalization en AWS ARChecks. Todavía no es público, pero ya hay productos de uso general que pueden servir como referencia blog de AWS
  • Considero que usar un Agent/LLM como juez tiene sesgos y solo es adecuado para bootstraping. Si el rendimiento sube lo suficiente, el juez LLM termina convirtiéndose en una limitación artificial, así que eventualmente habrá que pasar a jueces humanos expertos o a oráculos deterministas
• Se menciona que el knife-edge rolling kernel de RHEL se usa en la prueba de concepto
• Sintió que faltaba una explicación detallada en el repositorio, aunque eso puede deberse a que funciona como artefacto complementario del paper. En esencia, parece una API que intenta hacer que el LLM genere programas Z3. Busca que las consultas del mundo real se expresen lógicamente, capturando hechos, reglas de inferencia y objetivos. La función de supervisión consiste en poder leer directamente las descripciones lógicas y ejecutar el solver para comprobar si algo es verdadero o falso. Lo que genera dudas es: quién va a leer una por una las reglas SMT y contrastarlas con la realidad, quién valida los valores constantes, y si el LLM podría agregar por error o para cumplir el objetivo reglas lógicamente o factualmente desviadas. El paper reporta un 51% de false positive según benchmarks lógicos, lo que parece sorprendentemente alto y se interpreta como señal de que el LLM es débil para el modelado lógico o genera reglas incompletas. La evaluación es pobre y no explica con claridad por qué ocurre eso
  • Se afirma que este paper fue escrito el año pasado con GPT-4o y que con los modelos más recientes la situación ha mejorado mucho. Por ejemplo, en la paper reciente, la Tabla 1 compara el rendimiento basado en texto con el basado en SMT. o3-mini alinea bastante bien los resultados de text reasoning y SMT. En el producto comercial AWS Automated Reasoning Checks, se construye el modelo de dominio, se valida, y en la etapa de generación de respuestas se aplica una verificación estricta con solver para comprobar si los pares de preguntas y respuestas del LLM cumplen las políticas. Se enfatiza que esto puede garantizar más del 99% de validez de los pares Q/A respecto de políticas blog de AWS
• Es una pregunta sobre si su interpretación es correcta. Si la estructura consiste en que la salida probabilística del LLM pasa a un modelo lógico, expresa la sospecha de que entonces no sería más que “garbage in, garbage out”
  • La lógica formal actúa como filtro. O sea, “garbage in, filtered garbage out”. Lo compara con la evolución, donde mutaciones aleatorias “basura” son filtradas por el entorno natural
  • Se sostiene que no siempre sale “basura”. Con bastante frecuencia produce resultados útiles, y por eso tiene sentido
  • Es una cuestión subjetiva. Todo lo que la humanidad ha creado en los últimos miles de años también podría verse como basura. Si uno quiere ponerse estricto, quizá la vida en las cavernas era más simple
• Resulta muy interesante que la IA no solo piense, sino que además deje un diario verificable. Es como ver a un filósofo vivir con un notario criptográfico. Es un trabajo realmente asombroso
• La idea central es que el LLM hace un diseño inicial del proceso de razonamiento de forma estructurada y en un DSL JSON, y luego eso se transforma de manera determinista a lógica de primer orden para intentar una prueba de teoremas con Z3. Por eso, la salida final produce una conclusión demostrable (o un contraejemplo), y se destaca que eso es distinto de una simple cadena de texto persuasiva
• Es una investigación interesante. Revisé el repo porque me daban curiosidad los ejemplos del DSL, pero fue difícil encontrar ejemplos claros. Estaría bien tener un snippet de ejemplo en el README
  • Gracias por el interés, lo agregaré pronto. Mientras tanto, a partir de la página 11 del paper se explican varios escenarios PDF del paper