Dans beaucoup d'agents IA, le modèle de langage élabore seul la réponse, et il ne reste qu'à lui faire confiance. SynaLemma répartit le travail : le modèle de langage traduit la question en règle, puis un moteur logique vérifie cette règle et calcule la réponse dans la base existante. Chaque étape reste visible.
Conçu par SynaLinks, une équipe de spécialistes de l'IA issus du CNRS. Chaque couche du système est développée en interne, du moteur logique à l'agent.
Quels modèles de vélo s'arrêtent si Shenzhen VoltPack fait défaut ?
Les quatre : Urban S1, Cargo C2, Trekking T3 et Folding F1. Chaque modèle utilise l'un des deux packs batterie, et les deux packs intègrent la carte BMS et le boîtier fournis par VoltPack.
## Les assemblages qui s'arrêtent si un fournisseur fait défaut,
## à tous les niveaux de la nomenclature.
@OrderBy(SupplierExposure, "supplier_id", "assembly_id");
SupplierExposure(supplier_id:, assembly_id:) distinct :-
Supplies(supplier_id:, part_id: component),
Requires(assembly_id:, component_id: component);
Une question simple : quel est le stock disponible d'un composant ? Chaque agent IA écrit une requête SQL valide, et arrive pourtant à un chiffre différent. Chaque agent doit en effet décider seul de ce que « disponible » veut dire : avec ou sans le stock réservé, avec ou sans les commandes en cours, pour quel site et à quelle date. L'usine a tranché ces questions depuis longtemps, mais l'agent ne le sait pas.
Rien ne signale l'erreur. L'agent présente son chiffre avec assurance, quelqu'un prend une décision dessus, et personne ne peut retracer comment il a été calculé. C'est la principale raison pour laquelle les projets d'IA calent entre la démonstration et la production. Un modèle plus gros n'y change rien : il doit lui aussi deviner les définitions.
| Agent | Compte comme disponible | Résultat |
|---|---|---|
| Premier | tout ce qui est en stock | 1 240 |
| Deuxième | le stock, moins les réservations pour les ordres de fabrication | 870 |
| Troisième | le stock moins les réservations, plus les commandes d'achat en attente | 2 070 |
Les agents IA ont besoin des définitions de l'organisation : écrites une seule fois, sous une forme qu'une machine est tenue d'appliquer et qu'une personne peut vérifier. SynaLemma construit cette couche et la tient à jour.
Quand un agent IA « explique son raisonnement », il s'agit d'un texte que le modèle génère après coup. Ce texte ne montre pas comment la réponse a réellement été calculée ; le contrôler n'apprend donc pas grand-chose. Dans SynaLemma, le modèle de langage traduit la question en règle. Un moteur logique calcule la réponse à partir de cette règle, en étapes que l'on peut rejouer.
Chaque règle est exécutée sur les vraies tables avant que l'assistante ne réponde.
La réponse reprend les lignes renvoyées par l'exécution : rien ne vient de la mémoire du modèle. SynaLemma tourne sur les serveurs de l'organisation, avec le modèle de langage choisi. L'assistante ne voit que ce que permet le rôle de la personne qui pose la question.
Le moteur logique fait chaque inférence, et chaque inférence peut être réexécutée.
Chaque réponse cite les règles utilisées, jusqu'à la ligne d'où vient un chiffre. Les équipes peuvent ouvrir une règle, la lire, la réexécuter, la modifier ou la verrouiller. Les règles sont des fichiers dans un dépôt Git : chaque changement indique qui l'a fait (une personne ou l'assistante), ce qui a changé et quand.
Le premier et le seul système d'IA qui écrit ses propres règles, les vérifie formellement et confronte leurs résultats à des énoncés mathématiques.
Chaque règle est vérifiée formellement avant toute génération de SQL ; plus de quinze types d'erreurs sont refusés, avec le motif. L'équipe énonce en outre, en logique du premier ordre, ce qu'un résultat doit toujours respecter. Le moteur logique cherche ensuite, dans les données présentes, des contre-exemples à ces conditions de contrôle. Quand une règle change, tout ce qui en dépend est signalé jusqu'à sa prochaine exécution. Avec un autre modèle de langage, les règles restent les mêmes.
Pas d'ETL, pas de second entrepôt de données, pas de base graphe à acheter.
Les règles se compilent en SQL et s'exécutent dans la base existante, sur des tables qui gardent leurs noms. Les systèmes plus anciens restent ainsi exploitables, sans projet de migration. Une définition est établie une fois puis réutilisée, ce qui évite de repayer les tokens qu'un modèle dépenserait à chaque fois pour la retrouver. SynaLemma fonctionne aussi avec des modèles ouverts sur du matériel interne.
Chaque réponse renvoie à une définition comme celle-ci : assez courte pour la personne responsable du chiffre, et assez précise pour une vérification formelle automatique.
---
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:);
Une définition tirée d'une couche de connaissances industrielle. Les conditions de contrôle sont écrites dans la notation de l'assistant de preuve Lean et confrontées aux données présentes. Si la recherche d'un contre-exemple ne renvoie rien, la condition est respectée. C'est un contrôle des données examinées, pas une preuve sur des données que le système n'a pas vues.
SynaLemma se connecte à la base existante (PostgreSQL, BigQuery, Databricks, Trino, Presto, DuckDB ou SQLite) ou importe des fichiers (CSV, Excel, JSON, JSONL, Parquet). Les bases sont interrogées sur place : les tables gardent leurs noms et rien n'est migré.
Lemma, l'assistante, cherche d'abord une définition existante. S'il n'y en a pas, Lemma écrit une nouvelle règle, la vérifie formellement et l'exécute sur les données. La réponse ne vient qu'ensuite, avec la règle citée.
La règle vérifiée est enregistrée avec un nom et une description, pour que les questions suivantes puissent s'appuyer dessus. Les équipes peuvent la relire, la corriger ou la verrouiller.
Nous l'avons constaté : le logiciel seul ne suffit pas, surtout dans une organisation sans expertise IA en interne. Un ou plusieurs spécialistes techniques de l'équipe qui développe SynaLemma participent donc à chaque projet, selon sa taille. Ils travaillent avec les équipes du client, avec un rôle défini dans la plateforme. Leurs missions :
SynaLinks a écrit le framework sur lequel tourne l'assistante, le moteur logique qui vérifie ses règles, le format qui conserve la connaissance, et le produit qui réunit les trois. Comme chaque couche entre la base de données et le modèle de langage est développée en interne, les pièces s'ajustent entre elles, et il est possible de dire précisément ce que fait le système et où sont ses limites.
Le produit avec lequel travaillent les équipes. La plateforme fait tourner les trois composants open source sur les données de l'organisation et y ajoute l'assistante, l'éditeur de règles, le graphe de dépendances, les rôles et l'intégration avec Slack ou Teams. Un produit commercial sous licence payante, déployé sur l'infrastructure du client.
Découvrir SynaLemmaLe framework sur lequel repose l'assistante. Il produit des sorties structurées conformes à un schéma, donne aux agents IA des outils et un bac à sable intégré, et optimise les instructions sur des résultats mesurés, sans modifier les poids du modèle. Développé sous la supervision de François Chollet, l'auteur de Keras. Open source, sous licence Apache-2.0.
Voir sur GitHubUn langage de programmation logique avec vérification formelle, écrit en Rust et compilé vers sept dialectes SQL. Les conditions de contrôle s'énoncent en propositions Lean, la notation de l'assistant de preuve Lean, et se vérifient sur les données. Open source, sous licence Apache-2.0.
Voir sur GitHubLe format dans lequel sont conservées les définitions : un fichier lisible par concept ou par règle, dans un dépôt Git. L'historique de chaque définition se relit et s'audite comme du code, et une couche de connaissances s'installe depuis un dépôt Git. Open source, sous licence Apache-2.0.
Voir sur GitHubLe modèle de langage traduit, le moteur logique raisonne. C'est cette séparation qui rend le raisonnement vérifiable et le modèle remplaçable.
Voir les composants open sourceQuand un chiffre faux peut provoquer un arrêt de production ou un audit raté, l'origine de chaque chiffre doit être établie.
Chaîne d'approvisionnement, achats, production et qualité. Nomenclatures, stocks, retards de livraison et défauts ont chacun une seule définition, partagée par les planificateurs, les acheteurs et les agents IA qui les assistent.
Santé, aéronautique, énergie et services financiers. Chaque chiffre remonte à une règle et aux tables que cette règle a lues : exactement ce que demande un auditeur.
La démonstration a marché, mais personne n'a voulu signer : une démo réussie n'est pas encore un système sur lequel fonder des décisions. SynaLemma donne à ceux qui doivent valider quelque chose à lire et à vérifier : la règle derrière chaque réponse.
La démonstration dure 30 minutes et elle est gratuite. Le meilleur point de départ est une question sur laquelle les équipes ne sont pas d'accord : nous montrons la réponse de SynaLemma et la règle utilisée pour l'obtenir. Si c'est pertinent, un diagnostic préalable suit, puis le déploiement avec les spécialistes de l'équipe de développement.
