LLM2SMT: Building an SMT Solver with Zero Human-Written Code

Each language version is independently generated for its own context, not a direct translation.

Imagina que quieres construir un detective lógico capaz de resolver acertijos matemáticos extremadamente complejos. Normalmente, para crear a este detective, necesitarías un equipo de ingenieros humanos muy inteligentes, años de estudio y miles de líneas de código escritas a mano.

Pero, ¿qué pasaría si le pidieras a una Inteligencia Artificial (IA) que construya a este detective por ti, desde cero, sin que tú escribas ni una sola línea de código?

Eso es exactamente lo que hicieron los autores de este paper. Crearon un sistema llamado LLM2SMT, donde un agente de IA (un "programador robot") escribió todo el software necesario para crear un solver SMT (una herramienta que verifica si una serie de reglas lógicas pueden ser ciertas o no) sin ayuda humana directa en la escritura del código.

Aquí te explico cómo funcionó esta aventura, usando analogías sencillas:

1. El Reto: Construir un "Cerebro Lógico"

El objetivo era crear un "solver" para un tipo específico de lógica llamado QF_UF (funciones no interpretadas sin cuantificadores).

La analogía: Imagina que tienes un montón de piezas de Lego de diferentes formas y colores. El problema es saber si puedes encajar todas esas piezas juntas para formar una torre perfecta, o si hay alguna pieza que hace que la torre se caiga inevitablemente.
El problema: La IA no solo tenía que escribir el código, sino que ese código tenía que ser lógicamente perfecto. Un error pequeño en la lógica podría hacer que el detective diga "sí" cuando la respuesta es "no", lo cual es catastrófico en matemáticas.

2. El Proceso: El Arquitecto Robot

Los investigadores no escribieron el código. Solo dieron instrucciones generales al agente de IA (usando un modelo llamado Claude Sonnet 4.6).

El primer intento fallido: Al principio, la IA fue un poco "ingenua". Le dijeron "haz un solver", y la IA construyó algo que funcionaba, pero le faltaba la parte más importante: no entendía cómo conectar las piezas lógicas (los conectores booleanos). Fue como construir un coche sin ruedas.
La corrección: Los humanos tuvieron que decirle: "Oye, falta la parte de la lógica booleana". La IA corrigió el error. Luego, la IA escribió su propio "motor de búsqueda" (un solucionador SAT) en lugar de usar uno profesional. Los humanos tuvieron que decirle: "No, usa esta herramienta profesional llamada CaDiCaL". La IA lo integró rápidamente.

3. Los Obstáculos: Trampas en el Camino

Aunque la IA es muy inteligente, a veces comete errores sutiles, como un humano que está cansado.

El bug del "Bucle Infinito": La IA creó un programa que, a veces, se quedaba pensando eternamente en un problema difícil sin darse cuenta. Los investigadores tuvieron que darle una regla estricta: "Si piensas más de X segundos, ¡para y di que no sabes la respuesta!".
El acertijo del "Diamante": Hay un tipo de problema lógico (llamado "problema del diamante") que es muy difícil para los solvers porque requiere ver patrones ocultos. La IA, por sí sola, no lo veía. Los investigadores le dieron un ejemplo concreto: "Mira, si tienes estas dos opciones, ambas llevan a la misma conclusión. Úsalas". La IA entendió el patrón, creó una técnica de "pre-procesamiento" (un atajo mental) y resolvió esos problemas instantáneamente.

4. La Magia: La IA se explica a sí misma

Una de las partes más impresionantes fue pedirle a la IA que no solo resolviera el problema, sino que escribiera una prueba formal en un lenguaje llamado Lean (un lenguaje usado para verificar matemáticas).

La analogía: Es como si el detective no solo te dijera "la torre se cae", sino que te entregara un video en cámara lenta, paso a paso, demostrando exactamente qué pieza falló y por qué, para que un juez (otro programa) pueda verificarlo.
El desafío: Al principio, la IA se confundió. Intentaba explicar cosas demasiado complicadas de golpe. Los investigadores tuvieron que darle un ejemplo de cómo escribir la prueba correctamente. Una vez que lo entendió, la IA pudo generar pruebas matemáticas válidas que demostraban que su propio código era correcto.

5. El Resultado: ¿Funciona?

Al final, compararon a este "detective hecho por IA" con los mejores detectives del mundo (programas famosos como Z3 y cvc5).

El veredicto: ¡Funcionó! El solver creado por la IA resolvió casi la misma cantidad de problemas que los programas creados por humanos expertos. Fue muy rápido y eficiente.
La lección: La IA puede escribir software complejo y razonar, PERO no es infalible. Necesita supervisión humana para:
1. Darle instrucciones claras.
2. Proveerle ejemplos de errores (para que aprenda a corregirlos).
3. Ponerle límites de tiempo y recursos.

Conclusión

Este paper nos dice que la IA ya es capaz de construir herramientas de razonamiento lógico de alto nivel. Sin embargo, no es un "magia negra" que funciona sola. Es más como un aprendiz genio: tiene un potencial increíble, pero necesita un maestro humano que le señale los errores, le dé ejemplos concretos y le diga cuándo parar.

En resumen: La IA puede escribir el código, pero los humanos todavía son necesarios para asegurar que la lógica tenga sentido.

Each language version is independently generated for its own context, not a direct translation.

A continuación presento un resumen técnico detallado del artículo "LLM2SMT: Construyendo un solver SMT con cero código escrito por humanos", traducido y adaptado al español.

1. Problema y Motivación

El artículo aborda una pregunta fundamental en la intersección de la Inteligencia Artificial y la lógica computacional: ¿Pueden los Modelos de Lenguaje Grande (LLM) desarrollar herramientas de razonamiento automático fiables?

Aunque los LLMs se utilizan ampliamente para escribir software general y formalizar matemáticas, su capacidad para crear un sistema que realice razonamiento lógico complejo (como un solver SMT) ha sido poco explorada. El desafío radica en que los errores en estos sistemas son sutiles y difíciles de detectar, pero críticos, ya que la corrección es primordial. El objetivo del estudio fue construir un solver SMT completo para la teoría de funciones no interpretadas sin cuantificadores (QF_UF) sin que ningún humano escriba una sola línea de código.

2. Metodología

El estudio se llevó a cabo utilizando un agente de codificación basado en el modelo Claude Sonnet 4.6 (a través de la interfaz Claude Code). La metodología se caracterizó por los siguientes puntos:

Desarrollo Autónomo: El agente escribió todo el código en C++20. No hubo intervención humana en la escritura del código, solo en la definición de los requisitos iniciales y la supervisión de la evaluación.
Arquitectura del Solver:
- Se implementó un solver estilo DPLL(T) para la teoría de igualdad con funciones no interpretadas (QF_EUF).
- Utilizó el algoritmo de clausura de congruencia de Nieuwenhuis-Oliveras.
- Integró el solver SAT CaDiCaL a través de la interfaz IPASIR-UP.
- Incluyó un módulo de preprocesamiento y un generador de pruebas en Lean (un probador de teoremas interactivo) para instancias insatisfacibles.
Estrategias de Depuración y Mejora:
- Dado que el agente cometió errores iniciales (como no manejar conectores booleanos correctamente o no usar CaDiCaL), los investigadores proporcionaron instrucciones explícitas y correcciones basadas en especificaciones.
- Se implementó un ciclo de fuzzing (generación de fórmulas aleatorias) y pruebas diferenciales (comparación contra un solver de referencia) para que el agente detectara y corrigiera sus propios errores.
- Se establecieron límites de tiempo (timeout) estrictos para evitar procesos infinitos.

3. Contribuciones Clave

A. Construcción de un Solver SMT desde Cero

El logro principal es la creación funcional de un solver SMT competitivo para QF_UF sin código humano. El sistema incluye:

Un parser utilizando ANTLR para el formato SMT-LIB2.
Implementación correcta de la clausura de congruencia.
Técnicas de preprocesamiento avanzadas, como la propagación de unidades y la simplificación de cortocircuito.

B. Técnica de Preprocesamiento para Problemas "Diamante"

El agente desarrolló autónomamente una técnica de preprocesamiento para resolver problemas de "diamante equacional" (ej. $(x_i = z_i \land z_i = x_{i+1}) \lor (x_i = v_i \land v_i = x_{i+1})$ ).

Funcionamiento: El agente identificó que el solver lazy estándar tenía dificultades con estas estructuras. Implementó un algoritmo que calcula la clausura de igualdad en cada rama de la disyunción, extrae las consecuencias comunes a todas las ramas y las añade como nuevas fórmulas unitarias. Esto resolvió problemas exponenciales de forma instantánea.

C. Certificación de Pruebas en Lean

El sistema es capaz de generar pruebas formales en Lean para instancias insatisfacibles.

El agente tradujo la lógica del solver a axiomas y teoremas en Lean.
Utilizó tácticas de automatización como grind (para lemas de teoría) y bv_decide (para la parte proposicional).
Aunque fue la parte más difícil (requiriendo guías humanas sobre cómo estructurar la prueba para evitar desbordamientos de pila o tiempos de espera), el agente logró generar pruebas correctas.

4. Resultados Experimentales

El solver fue evaluado en los benchmarks SMT-LIB (QF_UF no incrementales) y comparado con solvers maduros como Z3 y cvc5.

Rendimiento:
- El solver llm2smt resolvió 7,468 instancias de un total de 7,500.
- Comparado con Z3 (7,500 resueltos) y cvc5 (7,494), el rendimiento es altamente competitivo.
- Curiosamente, la versión sin propagación de teoría fue ligeramente más rápida en los benchmarks probados, sugiriendo que la propagación introduce sobrecarga en ciertos casos sin beneficios inmediatos.
Certificación:
- Se certificaron exitosamente 285 instancias con preprocesamiento.
- Hubo muchos fallos en la certificación debido a limitaciones de recursos de Lean (límites de recursión, heartbeats), pero no se encontraron pruebas erróneas, lo que valida la corrección lógica del sistema.

5. Significado y Conclusiones

El artículo concluye que la respuesta a si los LLMs pueden desarrollar herramientas de razonamiento automático es un "sí cualificado".

Capacidades: Un agente de codificación puede implementar algoritmos complejos descritos en literatura científica, depurar su propio código mediante pruebas sistemáticas y generar código funcional de alto nivel.
Limitaciones y Advertencias:
- Corrección no asumida: El agente requiere especificaciones muy detalladas, ejemplos concretos y un ciclo estricto de pruebas (fuzzing) para corregir errores sutiles (como tratar los booleanos como proposiciones y términos simultáneamente).
- Inteligencia "Jagged" (Irregular): El agente puede fallar en tareas triviales (como simplificar $t=t$ ) mientras resuelve problemas complejos, lo que representa un desafío para la fiabilidad.
- Generación de Pruebas: Fue el desafío más difícil, requiriendo una guía humana significativa para alinear la lógica del solver con las expectativas del probador de teoremas (Lean).

Impacto Futuro: Este trabajo demuestra que los LLMs pueden ser socios efectivos en la investigación de herramientas de razonamiento automático, acelerando la integración de nuevas técnicas y la experimentación, siempre que se utilicen con un marco de validación riguroso y supervisión humana estratégica.