La plupart des systèmes d'agents laissent le modèle de langage raisonner et vous demandent de faire confiance au résultat. SynaLemma confie ce travail à un moteur logique. Le modèle écrit une règle ; le moteur la vérifie, calcule la réponse dans votre propre base et vous montre chaque étape.
Conçu par SynaLinks, une équipe d'ingénieurs IA issus du CNRS qui en ont écrit chaque couche, du moteur logique à l'agent.
Quels vélos s'arrêtent si Shenzhen VoltPack fait défaut ?
Les quatre : Urban S1, Cargo C2, Trekking T3 et Folding F1. Chacun utilise l'un des deux packs batterie, et les deux packs intègrent la carte de gestion 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);
Prenons une question simple : quel est le stock disponible d'un composant ? Chaque agent écrit un SQL valide et renvoie un chiffre différent, parce que chacun a dû deviner ce que « disponible » veut dire. Le stock réservé compte-t-il ? Les commandes en cours ? Quel site, à quelle date ? Votre usine a tranché ces points depuis longtemps, mais l'agent n'a aucun moyen de le savoir.
Rien ne signale l'erreur. L'agent donne 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 a le même problème, puisqu'il devine les mêmes définitions.
| Agent | Décide que le stock disponible est… | Réponse |
|---|---|---|
| Premier | ce qui est en stock | 1 240 |
| Deuxième | le stock, moins ce qui est réservé aux ordres de fabrication | 870 |
| Troisième | le stock moins le réservé, plus les commandes d'achat non reçues | 2 070 |
Les agents ont besoin de vos définitions, écrites une fois sous une forme qu'une machine est obligée d'appliquer et qu'une personne peut relire. SynaLemma construit cette couche et la tient à jour.
Quand un agent « explique son raisonnement », vous lisez un texte que le modèle a généré après coup. Ce texte n'est pas un enregistrement de la façon dont la réponse a été calculée, et l'auditer n'apprend pas grand-chose. Dans SynaLemma, le modèle traduit votre question en règle, et un moteur logique calcule la réponse à partir de cette règle, en étapes que vous pouvez rejouer.
Chaque règle est exécutée sur vos 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 vos serveurs, avec le modèle de votre choix, et l'assistante est limitée à ce que permet le rôle de la personne qui demande.
Le moteur logique fait chaque inférence, et chacune peut être réexécutée.
Chaque réponse cite ses règles, jusqu'à la ligne d'où vient un chiffre. Vos é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 est un commit qui 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 passe un vérificateur formel avant toute génération de SQL, et plus de quinze classes d'erreurs sont refusées, avec le motif du refus. Vous énoncez ensuite ce qu'un résultat doit toujours respecter, en logique du premier ordre, et le moteur cherche des contre-exemples dans vos données. Quand une règle change, tout ce qui en dépend est signalé jusqu'à sa prochaine exécution. Quand vous changez de modèle, les règles restent les mêmes.
Pas d'ETL, pas de second entrepôt, pas de base graphe à acheter.
Les règles se compilent en SQL et s'exécutent dans la base que vous avez déjà, sur des tables qui gardent leurs vrais noms : vos systèmes historiques sont couverts sans projet de migration. Une définition est établie une fois puis réutilisée, ce qui évite de payer à nouveau les tokens qu'un modèle dépenserait à la retrouver. SynaLemma fonctionne aussi avec des modèles ouverts sur votre propre matériel.
Chaque réponse renvoie à une définition comme celle-ci. Elle est assez courte pour que le responsable du chiffre la lise, et assez précise pour qu'une machine la vérifie.
---
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 industrielle. Les énoncés sont écrits dans la notation de l'assistant de preuve Lean et confrontés à vos données. Un énoncé tient quand la recherche d'un contre-exemple ne renvoie rien. C'est un contrôle des données que vous avez ; il ne prouve rien sur des données que le système n'a pas vues.
Connectez SynaLemma à la base que vous exploitez déjà (PostgreSQL, BigQuery, Databricks, Trino, Presto, DuckDB, SQLite) ou déposez vos fichiers (CSV, Excel, JSON, JSONL, Parquet). Les bases sont interrogées sur place : les tables gardent leurs vrais noms et rien n'est migré.
Lemma, l'assistante, cherche d'abord une définition qui existe déjà. S'il n'y en a pas, elle écrit une nouvelle règle, la vérifie et l'exécute sur vos données. Elle ne répond qu'ensuite, en citant la règle.
La règle est enregistrée avec un nom et une description. La question suivante s'appuie dessus, et vos équipes peuvent la relire, la corriger ou la verrouiller.
Nous l'avons constaté : l'outil seul ne suffit pas, surtout quand une entreprise n'a pas d'expertise IA en interne. Un ou plusieurs ingénieurs dédiés, selon la taille de votre projet, issus de l'équipe qui construit SynaLemma, travaillent donc aux côtés de vos équipes, avec un rôle défini, dans la plateforme.
La plupart des produits d'IA associent le modèle d'un autre au framework d'un autre. Nous avons écrit le framework sur lequel tourne l'agent, le moteur logique qui vérifie ses règles, le format qui conserve la connaissance, et le produit qui réunit les trois. Peu d'équipes ont construit chaque couche entre la base de données et le modèle. Parce que nous l'avons fait, les pièces sont conçues pour s'ajuster, et nous pouvons vous dire précisément ce que fait le système et où sont ses limites.
Le produit qu'utilisent vos équipes. Il fait tourner les trois moteurs sur vos données et y ajoute l'assistante, l'éditeur de règles, le graphe de dépendances, les rôles, et Slack ou Teams. Un produit commercial, sous licence payante, déployé sur votre infrastructure.
Découvrir SynaLemmaLe framework avec lequel l'assistante est construite. Il contraint les sorties à respecter un schéma, donne aux agents des outils et un bac à sable embarqué, et optimise les instructions sur des résultats mesurés, sans toucher aux poids du modèle. Développé sous la supervision de François Chollet, l'auteur de Keras. Open source, Apache-2.0.
Voir sur GitHubUn langage logique doté d'un vérificateur formel, écrit en Rust et compilé vers sept dialectes SQL. Ce qu'un résultat doit respecter s'énonce en proposition Lean, la notation de l'assistant de preuve Lean, et se vérifie sur vos données. Open source, Apache-2.0.
Voir sur GitHubLe format dans lequel sont conservées vos définitions, avec un fichier lisible par concept ou par règle dans un dépôt git. L'historique de votre raisonnement se relit et s'audite comme du code, et une couche s'installe depuis un dépôt git. Open source, Apache-2.0.
Voir sur GitHubLe modèle traduit et le moteur logique raisonne. C'est cette séparation qui rend le raisonnement auditable et le modèle remplaçable.
Voir les moteurs open sourceQuand un chiffre faux peut provoquer un arrêt de production ou un audit raté, il faut savoir d'où vient chaque chiffre.
Équipes 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 qui les assistent.
Santé, aéronautique, énergie, finance. Chaque chiffre remonte à une règle et aux tables qu'elle a lues, ce que demande un auditeur.
La démonstration a marché, mais personne n'a voulu signer. SynaLemma donne à ceux qui doivent valider des règles qu'ils peuvent lire et vérifier.
La démo dure trente minutes et elle est gratuite. Venez avec une question sur laquelle vos équipes ne sont pas d'accord : nous vous montrons la réponse de SynaLemma et la règle qu'il a utilisée. Si c'est pertinent, un audit de préparation suit, puis des ingénieurs dédiés travaillent avec vos équipes.
