In molti agenti IA è il modello linguistico a elaborare la risposta, e a chi la riceve resta solo la fiducia. SynaLemma divide il lavoro: il modello linguistico traduce la domanda in una regola, un motore logico verifica la regola e calcola la risposta nel database esistente. Ogni passaggio resta visibile.
Sviluppato da SynaLinks, un team di specialisti di IA formatisi al CNRS. Ogni livello del sistema è scritto internamente, dal motore logico all'agente.
Quali modelli di bicicletta si fermano se Shenzhen VoltPack non consegna?
Tutti e quattro: Urban S1, Cargo C2, Trekking T3 e Folding F1. Ogni modello richiede uno dei due pacchi batteria, ed entrambi i pacchi usano la scheda BMS e l'involucro forniti da VoltPack.
## Gli assiemi che si fermano se un fornitore non consegna,
## a ogni livello della distinta base.
@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 domanda semplice: quanta giacenza è disponibile per un componente? Ogni agente IA scrive una query SQL valida, eppure arriva a un numero diverso. Ogni agente deve infatti decidere da solo che cosa significa “disponibile”: con o senza la merce riservata, con o senza gli ordini in arrivo, per quale sito e a quale data. Lo stabilimento ha preso queste decisioni da anni, ma l'agente non le conosce.
Nessun errore è visibile. L'agente presenta il numero con piena sicurezza, qualcuno prende una decisione su quella base e nessuno può ricostruire come è stato calcolato. È il motivo principale per cui i progetti di IA si bloccano tra la demo e la produzione. Un modello più grande non risolve il problema: anche quello deve indovinare le definizioni.
| Agente | Conta come disponibile | Risultato |
|---|---|---|
| Primo | tutto ciò che è a magazzino | 1.240 |
| Secondo | giacenza meno le quantità riservate agli ordini di produzione | 870 |
| Terzo | giacenza meno le quantità riservate, più gli ordini d'acquisto aperti | 2.070 |
Gli agenti IA hanno bisogno delle definizioni dell'organizzazione: scritte una volta sola, in una forma che una macchina deve applicare e che una persona può verificare. SynaLemma costruisce questo livello e lo mantiene aggiornato.
Quando un agente IA “spiega il suo ragionamento”, si tratta di un testo che il modello genera a posteriori. Quel testo non mostra come la risposta è stata davvero calcolata, quindi controllarlo dice poco. In SynaLemma il modello linguistico traduce la domanda in una regola. Un motore logico calcola la risposta a partire da quella regola, in passaggi rieseguibili.
Ogni regola viene eseguita sulle tabelle reali prima che l'assistente risponda.
La risposta riporta le righe restituite dall'esecuzione; nulla proviene dalla memoria del modello. SynaLemma gira sui server dell'organizzazione, con un modello linguistico a scelta. L'assistente vede solo ciò che il ruolo di chi pone la domanda consente.
Il motore logico compie ogni inferenza, e ogni inferenza è rieseguibile.
Ogni risposta cita le regole usate, fino alla riga da cui proviene un numero. Il team può aprire una regola, leggerla, rieseguirla, modificarla o bloccarla. Le regole sono file in un repository Git: ogni modifica registra chi l'ha fatta (una persona o l'assistente), che cosa è cambiato e quando.
Il primo e unico sistema di IA che scrive le proprie regole, le verifica formalmente e ne confronta i risultati con enunciati matematici.
Ogni regola viene verificata formalmente prima che esista una riga di SQL; più di quindici tipi di errore vengono rifiutati, con il motivo. Inoltre il team esprime in logica del primo ordine ciò che un risultato deve sempre rispettare. Il motore logico cerca poi nei dati presenti controesempi a questi vincoli di controllo. Quando una regola cambia, tutto ciò che si basa su di essa viene segnalato finché non è stato rieseguito. Con un altro modello linguistico, le regole restano invariate.
Nessun ETL, nessun secondo data warehouse, nessun database a grafo da acquistare.
Le regole vengono compilate in SQL ed eseguite nel database esistente, su tabelle che mantengono i loro nomi. Anche i sistemi meno recenti restano utilizzabili, senza progetti di migrazione. Una definizione viene elaborata una volta e poi riutilizzata, risparmiando i token che un modello spenderebbe ogni volta per ricostruirla. SynaLemma funziona anche con modelli aperti su hardware proprio.
Ogni risposta rimanda a una definizione come questa: abbastanza breve per chi è responsabile del numero, e abbastanza precisa per una verifica formale automatica.
---
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 definizione tratta da un livello di conoscenza industriale. I vincoli di controllo sono scritti nella notazione del dimostratore di teoremi Lean e confrontati con i dati presenti. Se la ricerca di un controesempio non restituisce nulla, il vincolo è rispettato. È un controllo sui dati esaminati, non una dimostrazione sui dati che il sistema non ha visto.
SynaLemma si collega al database esistente (PostgreSQL, BigQuery, Databricks, Trino, Presto, DuckDB o SQLite) oppure importa file (CSV, Excel, JSON, JSONL, Parquet). I database vengono interrogati direttamente: le tabelle mantengono i loro nomi e nulla viene migrato.
Lemma, l'assistente, cerca prima una definizione esistente. Se manca, Lemma scrive una nuova regola, la verifica formalmente e la esegue sui dati. Solo allora arriva la risposta, con la regola citata.
La regola verificata viene salvata con un nome e una descrizione, così le domande successive possono basarsi su di essa. Il team può rivederla, correggerla o bloccarla.
Abbiamo constatato che il software da solo non basta, soprattutto per le organizzazioni senza competenze interne di IA. Per questo uno o più specialisti tecnici del team che sviluppa SynaLemma partecipano a ogni progetto, in base alle sue dimensioni. Lavorano con il team del cliente, con un ruolo definito all'interno della piattaforma. I loro compiti:
SynaLinks ha scritto il framework su cui gira l'assistente, il motore logico che ne verifica le regole, il formato che conserva la conoscenza e il prodotto che riunisce i tre. Poiché ogni livello tra il database e il modello linguistico è stato costruito internamente, i componenti si integrano tra loro ed è possibile indicare con precisione che cosa fa il sistema e dove sono i suoi limiti.
Il prodotto con cui lavorano i team. La piattaforma esegue i tre componenti open source sui dati dell'organizzazione e aggiunge l'assistente, l'editor di regole, il grafo delle dipendenze, i ruoli e l'integrazione con Slack o Teams. Un prodotto commerciale con licenza a pagamento, installato sull'infrastruttura del cliente.
Scopri SynaLemmaIl framework alla base dell'assistente. Produce risultati strutturati conformi a uno schema, fornisce agli agenti IA strumenti e un ambiente isolato integrato (sandbox), e ottimizza le istruzioni in base a risultati misurati, senza modificare i pesi del modello. Sviluppato sotto la supervisione di François Chollet, l'autore di Keras. Open source con licenza Apache-2.0.
Vedi su GitHubUn linguaggio di programmazione logica con verifica formale, scritto in Rust e compilato in sette dialetti SQL. I vincoli di controllo si esprimono come proposizioni Lean, la notazione del dimostratore di teoremi Lean, e vengono controllati sui dati. Open source con licenza Apache-2.0.
Vedi su GitHubIl formato in cui sono conservate le definizioni: un file leggibile per ogni concetto o regola, in un repository Git. La storia di ogni definizione si revisiona e si controlla come il codice, e un livello di conoscenza si installa da un repository Git. Open source con licenza Apache-2.0.
Vedi su GitHubIl modello linguistico traduce, il motore logico ragiona. Questa separazione rende il ragionamento verificabile e il modello sostituibile.
Scopri i componenti open sourceQuando un numero sbagliato può causare un fermo di produzione o un audit fallito, l'origine di ogni numero deve essere certa.
Catena di fornitura, acquisti, produzione e qualità. Distinte base, giacenze, consegne in ritardo e difetti hanno ciascuno una sola definizione, condivisa da pianificatori, addetti agli acquisti e dagli agenti IA che li supportano.
Sanità, aerospazio, energia e servizi finanziari. Ogni numero risale a una regola e alle tabelle che quella regola ha letto: esattamente ciò che un revisore chiede di vedere.
La demo ha funzionato, ma nessuno ha voluto approvarla: una demo riuscita non è ancora un sistema su cui basare decisioni. SynaLemma offre a chi deve approvare qualcosa da leggere e verificare: la regola dietro ogni risposta.
La dimostrazione dura 30 minuti ed è gratuita. Il punto di partenza ideale è una domanda su cui i team non sono d'accordo: mostriamo la risposta di SynaLemma e la regola usata per ottenerla. Se c'è corrispondenza, seguono una valutazione di idoneità e poi l'implementazione con gli specialisti del team di sviluppo.
