El problema que nadie quiere resolver a mano

Cuando alguien escribe "Si llueve, entonces la calle se moja. Está lloviendo. Por lo tanto, la calle está mojada", cualquier persona razonable entiende que eso es un modus ponens. La estructura lógica está ahí, visible, casi obvia. Y sin embargo, traducirla a código formal —a algo que una máquina pueda verificar con rigor— es un proceso que la mayoría de los sistemas simplemente le delegan a un modelo de lenguaje grande, cruzan los dedos y esperan.

Yo quería saber si eso era necesario. Si la dependencia de una LLM para este tipo de tarea era una comodidad o una inevitabilidad. La respuesta que encontré, después de construir autologic, es más matizada de lo que esperaba.

Reglas en lugar de pesos

autologic convierte texto en lenguaje natural —español o inglés— en código formal ejecutable en ST lang, un lenguaje lógico que desarrollé por separado. La restricción central del proyecto es explícita: sin modelos de lenguaje, sin APIs externas, sin dependencias de runtime. Todo el procesamiento es interno.

El pipeline tiene cinco etapas bien diferenciadas. Primero, un segmentador divide el texto en oraciones y cláusulas usando puntuación y marcadores discursivos. Luego, un analizador de discurso detecta el rol semántico de cada fragmento: ¿es una premisa? ¿una condición? ¿una conclusión? ¿una negación? A partir de ese análisis, un extractor de átomos identifica las proposiciones elementales y les asigna identificadores únicos. Después, un constructor de fórmulas mapea los roles detectados a operadores lógicos según el perfil activo. Finalmente, un generador emite el código ST con trazabilidad: cada fórmula referencia el fragmento de texto del que proviene.

El sistema soporta once perfiles lógicos: proposicional clásico, primer orden con cuantificadores, modal K, deóntico, epistémico S5, intuicionista, temporal LTL, paraconsistente Belnap de cuatro valores, silogístico aristotélico, probabilístico y aritmético. Cada perfil responde a un régimen distinto de lo que cuenta como inferencia válida.

Lo que me forzó a pensar con precisión

Lo más revelador de construir este sistema no fue el código en sí. Fue la disciplina que impone trabajar sin ambigüedad probabilística.

Un modelo de lenguaje, cuando formaliza texto, hace una apuesta estadística sobre qué estructura lógica probablemente corresponde a esa oración. Puede equivocarse de maneras que parecen razonables, y esa razonabilidad superficial es precisamente lo que las hace peligrosas si el objetivo es verificación formal. Un sistema basado en reglas, en cambio, es brutalmente honesto sobre lo que no sabe. Si el analizador de discurso no reconoce el patrón, no lo inventa. Devuelve un diagnóstico vacío o parcial, y esa honestidad tiene valor.

Escribir los ~200 marcadores discursivos bilingües que el sistema reconoce —"si", "entonces", "por lo tanto", "es necesario que", "siempre que", "en algún momento"— me obligó a pensar en qué distingue un condicional de una implicación, una obligación deóntica de una necesidad modal, una afirmación probabilística de una certeza lógica. Esas distinciones existen en la lengua, pero están enterradas bajo capas de uso cotidiano. El ejercicio de hacerlas explícitas como reglas es, en sí mismo, un ejercicio filosófico.

Once formas de ser coherente

La decisión de incluir once perfiles lógicos no es cosmética. Es una declaración sobre la naturaleza del razonamiento.

La lógica clásica asume que toda proposición es verdadera o falsa, que las contradicciones son fatales, y que el tiempo no existe. Esos supuestos funcionan bien en matemáticas formales y en algunos dominios de la computación. Pero el lenguaje natural no vive en ese espacio. Una oración como "es obligatorio pagar impuestos" no tiene el mismo régimen de verdad que "dos más dos es cuatro". Una afirmación sobre lo que "siempre ocurrirá" opera en lógica temporal, no proposicional.

La lógica paraconsistente de Belnap —uno de los perfiles más interesantes del sistema— permite cuatro valores de verdad: verdadero, falso, ambos y ninguno. Fue diseñada para razonar en presencia de información contradictoria sin que el sistema colapse. En bases de conocimiento reales, en textos jurídicos, en cualquier corpus que haya sido escrito por múltiples personas en distintos momentos, la contradicción no es un error a eliminar: es un dato a manejar. Tener un perfil específico para ese caso no es un capricho técnico. Es reconocer que diferentes dominios del pensamiento humano tienen diferentes ontologías de la verdad.

El límite honesto del enfoque

Autologic funciona bien cuando el texto tiene estructura discursiva reconocible: argumentos, condicionales, generalizaciones, negaciones. Falla o se vuelve superficial cuando el texto es ambiguo de una manera que requiere conocimiento del mundo para resolver. "El banco estaba cerrado" es una oración que un humano desambigua por contexto en milisegundos. Un sistema basado en reglas puras, sin modelo semántico, no puede hacer eso con fiabilidad.

Eso no es una falla del proyecto. Es el límite honesto de la apuesta que hice: demostrar que existe un espacio útil entre "el texto es trivialmente estructurado" y "necesito una LLM". Ese espacio es más grande de lo que la industria asume, especialmente en dominios donde la trazabilidad y la determinismo importan más que la cobertura semántica completa.

Los 74 tests con ~80% de cobertura no prueban que el sistema sea perfecto. Prueban que el sistema es predecible. Y en verificación formal, predecible vale más que flexible.

La pregunta que queda abierta

Hay una tensión que este proyecto no resuelve, y que me parece más interesante que cualquier resultado técnico: ¿hasta dónde puede llegar la formalización antes de traicionar el significado?

Formalizar "es necesario que las leyes se cumplan" como una fórmula modal □(leyes_se_cumplan) captura la estructura. Pero deja afuera la carga política, la historia de por qué esa obligación existe, el contexto en el que se enuncia. La lógica formal no tiene acceso a esas capas. Es, por diseño, una reducción.

Lo que autologic me dejó es la convicción de que esa reducción, hecha con rigor y con honestidad sobre sus límites, tiene usos precisos y valiosos. No reemplaza la interpretación. La prepara.