Un grupo de investigadores está combinando LLMs con motores de razonamiento formal (Z3 para constraint solving, Tau Prolog para logic programming) para que los asistentes de código puedan analizar estructuralmente el código fuente sin halucinar, usando tree-sitter para parsear y gramáticas formales para razonar con certeza.
En 30 segundos
- Los LLMs usan grep y reconstrucción de call chains, lo que falla en preguntas como “¿puede input del usuario llegar a una query SQL?” o “¿qué código está muerto?”
- El paradigma neurosimbólico combina redes neuronales (para entender preguntas) con motores de razonamiento simbólico (para probar propiedades con certeza)
- Z3 resuelve restricciones, Tau Prolog hace razonamiento lógico, tree-sitter parsea código sin necesidad de compilar
- Reduce drásticamente tokens y alucinaciones en análisis de seguridad, dead code y control de flujo
Los motores de razonamiento formal para LLM son sistemas que combinan la capacidad del lenguaje natural de los LLMs con herramientas simbólicas capaces de probar propiedades del código con certeza matemática. En lugar de generar respuestas probabilísticas, estos motores analizan el código estructuralmente usando tree-sitter (parser universal), lo convierten en gramáticas formales, y luego aplican constraint solving (Z3) o logic programming (Tau Prolog) para responder preguntas sobre seguridad, dead code y control de flujo.
Por qué los LLMs fallan analizando código
Ponele que le preguntás a Claude o GPT: “¿puede el input del usuario llegar a esta query SQL a través de alguna cadena de llamadas?”. Lo que pasa internamente es que el modelo hace grep en los archivos, trata de reconstruir manualmente quién llama a quién, mira algunas rutas y te devuelve una respuesta. La cosa es que con sistemas complejos, con múltiples niveles de indirección, eso simplemente no funciona. El modelo no puede garantizar que encontró TODAS las rutas posibles (eso es un análisis transitivo), y menos aún verificar si una inyección SQL es posible o imposible.
El problema fundamental es que los LLMs son estadísticos, no lógicos. Son muy buenos generando código plausible y explicando conceptos, pero terribles probando propiedades formales. Si le decís “¿es seguro este código?”, te devuelve “sí” o “no” basado en probabilidades, no en certeza. Y en seguridad, la probabilidad no alcanza.
Razonamiento formal: Z3, Prolog y cómo funcionan
Ahora bien, existen herramientas que llevan décadas haciendo esto: constraint solving (Z3) y logic programming (Prolog). Son motores que NO generan texto, sino que PRUEBAN propiedades. La diferencia es enorme.
Z3 es un SMT solver (Satisfiability Modulo Theories). Le definís restricciones sobre variables (ponele: “X es mayor a 5”, “Y tiene que ser un string distinto de NULL”), y Z3 te dice: “sí, existe una asignación de valores que satisface eso” o “no, eso es imposible”. Se usa en verificación formal desde hace 15 años. Más contexto en análisis de seguridad en código.
Tau Prolog es logic programming: le definís reglas y hechos sobre tu código (ponele: “función A llama a función B”, “función B accede a tabla SQL”), y Prolog puede deducir “función A puede acceder a tabla SQL por transitoriedad”. Sin alucinaciones, sin probabilidades.
El drama es que combinar eso con LLMs no es trivial. Necesitás que el LLM entienda la pregunta en lenguaje natural, la traduzca a una query lógica, ejecute el motor formal, y luego devuelva la respuesta de nuevo en lenguaje natural.
El paradigma neurosimbólico
Acá viene lo bueno: la arquitectura neurosimbólica, que es lo que explica Yogthos en su post reciente. La idea es simple: usa redes neuronales para lo que hacen bien (procesar lenguaje natural, entender contexto), y usa sistemas simbólicos para lo que hacen bien (razonamiento lógico, pruebas formales).
Vos preguntás algo en lenguaje natural, el LLM entiende qué estás preguntando, convierte la pregunta a una query formal, el motor simbólico corre la query, devuelve certeza (sí, no, imposible), el LLM lo traduce de vuelta a lenguaje natural. Es una línea de ensamblaje. El LLM no tiene que razonar formalmente, solo tiene que entender y traducir. Y eso sí que lo hace bien.
Cómo funciona en la práctica: tree-sitter y gramáticas formales
El flujo es más o menos así: primero, tree-sitter parsea el código fuente en un árbol sintáctico. Tree-sitter no es un compilador (no necesita las dependencias instaladas, no necesita entender semántica), solo entiende la sintaxis. Eso ya es un avance respecto a grep.
Luego, ese árbol se convierte en una gramática formal que entiende el motor de razonamiento. Por ejemplo, para Python, la gramática diría: “si una variable X es asignada en línea 5 desde un parámetro de función, entonces X viene del exterior”. Y así para cada construcción del lenguaje. Una vez que el código está representado como restricciones y hechos lógicos, los motores Z3 y Prolog pueden responder preguntas complejas: “¿todas las rutas que llevan a esta query SQL validan el input?” (detección de inyección SQL), “¿qué variables nunca se usan?” (dead code), “¿qué funciones tienen side effects globales?”. Todo con certeza, no probabilidades. Tema relacionado: análisis avanzado en ChatGPT.
El ahorro de tokens es brutal. Analizar un módulo entero con grep tradicional requiere 5000+ tokens. Con análisis formal, podés hacerlo en 500.
Casos de uso reales: de la teoría al código que corre
| Caso de Uso | Métodos LLM tradicionales | Con motores formales |
|---|---|---|
| Detección SQL injection | Grep + heurísticas, falla en rutas indirectas | Rastreo transitivo de datos, certeza |
| Dead code detection | Búsqueda de referencias, muchos falsos negativos | Análisis de alcanzabilidad, definitivo |
| Control de flujo | “Parece que sí” | Prueba formal de propiedades |
| Side effects | Pattern matching, incompleto | Análisis simbólico exhaustivo |
Ejemplo 1: le pasás un módulo Python que usa Django ORM. Con LLM tradicional, el modelo busca .raw() queries y trata de inferir si hay validación. Con análisis formal, tree-sitter identifica TODAS las asignaciones a variables que finalmente llegan a la query, y Z3 verifica si cada una está validada. Respuesta: “seguro” o “vulnerable”, sin ambigüedad.
Ejemplo 2: tenés 500 líneas de código, 50 funciones. LLM busca llamadas a cada función, pero pierde referencias dinámicas o llamadas vía diccionarios. Prolog analiza el árbol sintáctico completo, identifica qué es alcanzable desde los entry points (main, handlers, etc.), y dice exactamente qué código nunca corre.
Herramientas y proyectos que lo implementan
El post de Yogthos (8 de abril de 2026) presenta un MCP server que integra Z3 y Tau Prolog. No es un producto comercial todavía, es una investigación que combina el framework de Model Context Protocol de Anthropic con motores formales.
SymbolicAI (en GitHub) es otro proyecto en esa línea: neurosimbólico desde cero, que permite combinar operaciones simbólicas con LLMs. CodeRLM es otro experimento que usa tree-sitter para indexación exhaustiva de código. Lo importante es que estos son prototipos. El concepto está en 2026 en fase “proof of concept”, pero la dirección es clara: los asistentes de código serio van a necesitar razonamiento formal. (Si no, te van a dar vulnerabilidades de seguridad sin que el modelo ni se dé cuenta.)
Limitaciones honestas
Seamos honestos: esto no es magia. Primero, requiere definir gramáticas formales para CADA lenguaje. No es lo mismo parsear Python que Go que Rust. Tree-sitter cubre varios, pero no todos. Segundo, el costo computacional de verificación formal sigue siendo alto en algunos casos.
Tercero, y quizás lo más importante: esto NO reemplaza revisión humana. Un análisis formal puede decir “no hay ruta donde input sin validar llega a SQL”, pero no puede decir “la validación es la adecuada para este contexto de negocio”. Para eso necesitás un humano. Sobre eso hablamos en razonamiento formal en GPT.
Y cuarto: la curva de aprendizaje para definir gramáticas formales es empinada. No es algo que el equipo de QA tenga listos en una semana.
Errores comunes
Creer que el motor formal descubre vulnerabilidades lógicas
No. Descubre vulnerabilidades en la RUTA de datos. Si validás con regex débil, el análisis formal dirá “está validado”. No sabe si la validación es buena o mala. Es trabajo del humano hacer el schema de validación correcta.
Esperar que funcione sin conocimiento de código
El motor necesita que le digas qué es una “variable externa”, qué es una “query SQL”, etc. No entiende semántica de negocio. Necesitás especialización en el lenguaje y dominio que estés modelando.
Creer que reemplaza testing
El análisis formal prueba PROPIEDADES del código. Testing prueba COMPORTAMIENTO. Un código puede ser formal-correcto pero fallar en producción por edge cases no previstos. Son complementarios, no sustitutos.
Preguntas Frecuentes
¿Cómo pueden los LLMs analizar código de forma exhaustiva sin halucinar?
No lo hacen solos. El LLM entiende la pregunta y la traduce a una query lógica, pero es el motor formal (Z3, Prolog) el que responde con certeza. El LLM no genera la respuesta por probabilidad; ejecuta un programa formal y reporta el resultado. Es como preguntarle a una calculadora si 2+2=5: no alucina, tiene una respuesta determinística. Para más detalles técnicos, mirá capacidades de razonamiento de Gemini.
¿Qué diferencia hay entre tree-sitter y un motor de razonamiento simbólico?
Tree-sitter parsea código (transforma texto en árbol sintáctico). El motor simbólico razona sobre ese árbol (responde preguntas lógicas). Tree-sitter es la entrada, el motor es la máquina de pensar. Podés tener tree-sitter sin razonamiento formal (solo análisis sintáctico), pero no razonamiento formal sin parseo correcto.
¿Cómo funcionan Z3 y Prolog en la seguridad de código?
Z3 (constraint solver) verifica si es POSIBLE que exista una asignación de valores que viole una propiedad. Por ejemplo: “¿puede existir un input X tal que la query SQL tenga inyección?” Si Z3 dice “no existe tal X”, entonces es imposible. Prolog (logic programming) deduce conclusiones a partir de hechos y reglas: “A llama B, B accede a SQL, luego A accede a SQL”. Sin alucinaciones.
¿Qué es la IA neurosimbólica y cómo mejora los asistentes de código?
Es la combinación de redes neuronales (para lenguaje natural) con sistemas simbólicos (para lógica formal). El LLM entiende qué pedís, pero no responde por predicción: traduce tu pregunta a una query formal, ejecuta el motor lógico, y devuelve la respuesta con certeza. Es más lento que puro neural, pero infinitamente más confiable para seguridad.
¿Cuándo va a estar disponible esto en mis herramientas de código?
Aún es investigación. GitHub Copilot, Claude y otros asistentes usan LLMs puros todavía. Pero dado que la seguridad es negocio crítico, espera que en 2027 o 2028 los asistentes premium comiencen a integrar razonamiento formal para análisis de seguridad.
Conclusión
El paradigma neurosimbólico no es una solución de marketing, es un cambio de arquitectura real. Los LLMs solos son buenos generadores, pero malos verificadores. Los motores formales son buenos verificadores pero no entienden lenguaje natural. Combinarlos cubre ambas debilidades.
Lo que pasó el 8 de abril con el MCP server de Yogthos es un piedrazo en la laguna. No es un producto que vaya a apestar como Copilot mañana, pero es investigación seria que apunta a donde tiene que ir la industria: asistentes de código que no solo escriben rápido, sino que verifican seguro.
Si alguna vez pasó (o te pasará) que un asistente te devolvió código que parecía “seguro” pero luego descubriste una SQL injection, sabés el drama. Con análisis formal, eso no vuelve a pasar. No es “probablemente seguro”, es “formalmente seguro”.