En muchos agentes de IA, el modelo de lenguaje elabora la respuesta por su cuenta, y a quien la recibe solo le queda confiar. SynaLemma reparte el trabajo: el modelo de lenguaje traduce la pregunta a una regla, y un motor lógico verifica esa regla y calcula la respuesta en la base de datos existente. Cada paso queda a la vista.
Desarrollado por SynaLinks, un equipo de especialistas en IA formados en el CNRS. Cada capa del sistema es de desarrollo propio, del motor lógico al agente.
¿Qué modelos de bicicleta se paran si falla Shenzhen VoltPack?
Los cuatro: Urban S1, Cargo C2, Trekking T3 y Folding F1. Cada modelo necesita uno de los dos packs de baterías, y ambos packs llevan la placa BMS y la carcasa que suministra VoltPack.
## Los conjuntos que se detienen si falla un proveedor,
## en todos los niveles de la lista de materiales.
@OrderBy(SupplierExposure, "supplier_id", "assembly_id");
SupplierExposure(supplier_id:, assembly_id:) distinct :-
Supplies(supplier_id:, part_id: component),
Requires(assembly_id:, component_id: component);
Una pregunta sencilla: ¿cuántas existencias disponibles hay de un componente? Cada agente de IA escribe una consulta SQL válida y, aun así, llega a una cifra distinta. Cada agente tiene que decidir por su cuenta qué significa «disponible»: con o sin las existencias reservadas, con o sin los pedidos en curso, para qué planta y en qué fecha. La fábrica tomó esas decisiones hace años, pero el agente no las conoce.
Nada falla de forma visible. El agente presenta la cifra con total seguridad, alguien toma una decisión basándose en ella y nadie puede reconstruir cómo se calculó. Es el principal motivo por el que los proyectos de IA se estancan entre la demo y la producción. Un modelo más grande no lo resuelve: también tiene que adivinar las definiciones.
| Agente | Cuenta como disponible | Resultado |
|---|---|---|
| Primero | todo lo que hay en almacén | 1.240 |
| Segundo | existencias menos lo reservado para órdenes de fabricación | 870 |
| Tercero | existencias menos lo reservado, más los pedidos de compra pendientes | 2.070 |
Los agentes de IA necesitan las definiciones de la organización: escritas una sola vez, de forma que una máquina tenga que aplicarlas y una persona pueda comprobarlas. SynaLemma construye esa capa y la mantiene al día.
Cuando un agente de IA «explica su razonamiento», se trata de un texto que el modelo genera a posteriori. Ese texto no muestra cómo se calculó realmente la respuesta, así que revisarlo aporta poco. En SynaLemma, el modelo de lenguaje traduce la pregunta a una regla. Un motor lógico calcula la respuesta a partir de esa regla, en pasos que se pueden volver a ejecutar.
Cada regla se ejecuta sobre las tablas reales antes de que la asistente responda.
La respuesta cita las filas que devolvió la ejecución; nada sale de la memoria del modelo. SynaLemma funciona en los servidores de la organización, con el modelo de lenguaje que se prefiera. La asistente solo ve lo que permite el rol de quien pregunta.
El motor lógico realiza cada inferencia, y cada inferencia se puede volver a ejecutar.
Cada respuesta cita las reglas utilizadas, hasta la fila de la que procede una cifra. El equipo puede abrir una regla, leerla, volver a ejecutarla, modificarla o bloquearla. Las reglas son archivos en un repositorio Git: cada cambio registra quién lo hizo (una persona o la asistente), qué cambió y cuándo.
El primer y único sistema de IA que escribe sus propias reglas, las verifica formalmente y contrasta sus resultados con enunciados matemáticos.
Cada regla se verifica formalmente antes de que exista una sola línea de SQL; más de quince tipos de error se rechazan, con el motivo. Además, el equipo expresa en lógica de primer orden lo que un resultado debe cumplir siempre. El motor lógico busca después contraejemplos a esas condiciones de control en los datos disponibles. Cuando una regla cambia, todo lo que se apoya en ella queda señalado hasta que se vuelva a ejecutar. Con otro modelo de lenguaje, las reglas siguen igual.
Sin ETL, sin un segundo almacén de datos y sin base de datos de grafos que comprar.
Las reglas se compilan a SQL y se ejecutan en la base de datos existente, sobre tablas que conservan sus nombres. Así también se aprovechan los sistemas más antiguos, sin proyecto de migración. Una definición se elabora una vez y después se reutiliza, lo que ahorra los tokens que un modelo gastaría cada vez en reconstruirla. SynaLemma también funciona con modelos abiertos en hardware propio.
Cada respuesta remite a una definición como esta: lo bastante breve para la persona responsable de la cifra, y lo bastante precisa para una verificación formal automática.
---
name: SupplierDeliveries
description: Purchase orders per supplier, and how many were late.
keywords: [supplier, delivery, late, on time]
---
import tables.PurchaseOrders.PurchaseOrders;
@Assert(SupplierDeliveries,
one_row_per_supplier: "∀ s a b c d, SupplierDeliveries s a b → SupplierDeliveries s c d → a = c",
late_within_total: "∀ s a b, SupplierDeliveries s a b → b ≤ a");
@OrderBy(SupplierDeliveries, "supplier_id");
SupplierDeliveries(supplier_id:, deliveries? += 1, late? += is_late) distinct :-
PurchaseOrders(supplier_id:, is_late:);
Una definición de una capa de conocimiento industrial. Las condiciones de control se escriben en la notación del demostrador de teoremas Lean y se contrastan con los datos disponibles. Si la búsqueda de un contraejemplo no devuelve nada, la condición se cumple. Es una comprobación de los datos examinados, no una demostración sobre datos que el sistema no ha visto.
SynaLemma se conecta a la base de datos existente (PostgreSQL, BigQuery, Databricks, Trino, Presto, DuckDB o SQLite) o importa archivos (CSV, Excel, JSON, JSONL, Parquet). Las bases de datos se consultan directamente: las tablas conservan sus nombres y no se migra nada.
Lemma, la asistente, busca primero una definición existente. Si no la hay, Lemma escribe una regla nueva, la verifica formalmente y la ejecuta sobre los datos. Solo entonces llega la respuesta, con la regla citada.
La regla verificada se guarda con un nombre y una descripción, para que las preguntas siguientes puedan apoyarse en ella. El equipo puede revisarla, corregirla o bloquearla.
Hemos comprobado que el software por sí solo no basta, sobre todo en organizaciones sin experiencia interna en IA. Por eso, uno o varios especialistas técnicos del equipo que desarrolla SynaLemma participan en cada proyecto, según su tamaño. Trabajan con el equipo del cliente, con un papel definido dentro de la plataforma. Sus tareas:
SynaLinks ha escrito el framework sobre el que funciona la asistente, el motor lógico que verifica sus reglas, el formato que almacena el conocimiento y el producto que reúne los tres. Como cada capa entre la base de datos y el modelo de lenguaje es de desarrollo propio, las piezas encajan entre sí y se puede explicar con precisión qué hace el sistema y dónde están sus límites.
El producto con el que trabajan los equipos. La plataforma ejecuta los tres componentes de código abierto sobre los datos de la organización y añade la asistente, el editor de reglas, el grafo de dependencias, los roles y la integración con Slack o Teams. Un producto comercial con licencia de pago, desplegado en la infraestructura del cliente.
Descubrir SynaLemmaEl framework en el que se basa la asistente. Genera salidas estructuradas conformes a un esquema, da a los agentes de IA herramientas y un entorno aislado integrado (sandbox), y optimiza las instrucciones en función de resultados medidos, sin modificar los pesos del modelo. Desarrollado bajo la supervisión de François Chollet, autor de Keras. Código abierto con licencia Apache-2.0.
Ver en GitHubUn lenguaje de programación lógica con verificación formal, escrito en Rust y compilado a siete dialectos de SQL. Las condiciones de control se expresan como proposiciones de Lean, la notación del demostrador de teoremas Lean, y se contrastan con los datos. Código abierto con licencia Apache-2.0.
Ver en GitHubEl formato en el que se guardan las definiciones: un archivo legible por concepto o regla, en un repositorio Git. El historial de cada definición se revisa y se audita como el código, y una capa de conocimiento se instala desde un repositorio Git. Código abierto con licencia Apache-2.0.
Ver en GitHubEl modelo de lenguaje traduce, el motor lógico razona. Esa separación hace comprobable el razonamiento y sustituible el modelo.
Ver los componentes de código abiertoCuando una cifra errónea puede provocar una parada de producción o una auditoría fallida, el origen de cada número tiene que estar claro.
Cadena de suministro, compras, producción y calidad. Listas de materiales, existencias, entregas con retraso y defectos tienen cada uno una sola definición, compartida por planificadores, compradores y los agentes de IA que los apoyan.
Salud, aeroespacial, energía y servicios financieros. Cada cifra se remonta a una regla y a las tablas que esa regla leyó: justo lo que pide ver un auditor.
La demo funcionó, pero nadie quiso darle el visto bueno: una demo lograda todavía no es un sistema en el que basar decisiones. SynaLemma ofrece a quien debe aprobar algo que se puede leer y comprobar: la regla detrás de cada respuesta.
La demostración dura 30 minutos y es gratuita. El mejor punto de partida es una pregunta en la que los equipos no se ponen de acuerdo: mostramos la respuesta de SynaLemma y la regla utilizada para obtenerla. Si encaja, siguen una evaluación previa y, después, la implantación con especialistas del equipo de desarrollo.
