# SynaLemma : des réponses d'IA vérifiables sur les données de l'entreprise · SynaLinks > https://synalinks.com/ Des réponses d'IA vérifiables # Une démo d'IA peut convaincre. Mais la réponse est-elle juste ? 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. [Réserver une démo de SynaLemma](https://calendar.app.google/RMMAPbHYroAgiokb7) [Comment fonctionne SynaLemma](/synalemma) 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. SynaLemma usine 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. @SupplierExposure ✓ vérifiée ``` ## 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); ``` * vérifiée formellement avant enregistrement * exécutée sur Suppliers, Parts, BillOfMaterials Données fictives d'une usine, à titre d'illustration. La règle est du vrai code Synalog. Équipe basée dans l'Union européenne Sur des serveurs internes, avec le modèle de langage choisi Bâti sur nos composants open source sous licence Apache-2.0 Le problème ## La même question. Trois agents IA. Trois réponses différentes. 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 Exemple fictif, à titre d'illustration : une question, trois requêtes plausibles. 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. FichiersBase SQLTableursSavoir métier Les données restent là où elles sont SynaLemma 1. Chercher une définition 2. Écrire une règle 3. La vérifier formellement 4. L'exécuter sur les tables 5. Répondre en citant la règle Une réponse vérifiable * Le chiffre * La règle utilisée * Lisible par les équipes * Réutilisable La règle reste disponible Ce qui change ## Le modèle de langage comprend la question. Le moteur logique calcule la réponse. 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. Systèmes où raisonne le modèle de langage SynaLemma Qui raisonne Le modèle de langage, dans un texte impossible à rejouer Un moteur logique, avec des règles lisibles et réexécutables Piste d'audit Un récit de ce que le modèle dit avoir fait Une chaîne de règles nommées, jusqu'aux lignes sources Liens entre tables Des jointures souvent réécrites à chaque question Un graphe de connaissances extrait des tables existantes, sans base graphe Évolution d'une définition Souvent introuvable : quel prompt valait au trimestre dernier ? Chaque changement est un commit Git, avec auteur et date, et peut être annulé Sens d'un indicateur Réestimé à chaque question Écrit une fois, en règle nommée, réutilisée par tous Avant la réponse Pas de contrôle systématique Vérification formelle, puis exécution sur les vraies tables En cas d'erreur Un chiffre faux, souvent sans avertissement La règle est refusée avec le motif, ou une condition de contrôle (assertion) montre les lignes qui ne la respectent pas Deux fois la même question Deux réponses qui peuvent différer Une fois la règle écrite : à données égales, le même résultat, quel que soit le modèle branché Systèmes existants Souvent une nouvelle chaîne de traitement et une copie des données Interrogation directe des bases déjà en place La centième question Le même raisonnement, repayé en tokens Une règle qui existe déjà, exécutée en SQL Ce que cela apporte ## Des réponses plausibles aux résultats vérifiables. 01 · Fiabilité ### Des résultats fondés sur les données existantes 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. 02 · Traçabilité ### De la réponse à la donnée source 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. 03 · Vérification formelle ### Des erreurs détectées avant et après l'exécution 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. 04 · Efficacité ### Aucune copie supplémentaire de la base 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. Un exemple ## Voici à quoi ressemble une règle vérifiable. 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. * En tête figurent les conditions de contrôle : ce qui doit toujours être vrai, en notation mathématique. Ici : une ligne par fournisseur, et jamais plus de livraisons en retard que de livraisons au total. * En dessous, la règle décrit comment le résultat se calcule à partir des commandes d'achat. * Si les données contredisent une condition de contrôle, SynaLemma montre les lignes en cause au lieu d'afficher un taux faux. * La définition est un fichier texte dans le dépôt Git de l'organisation, relu comme n'importe quel autre code. Une définition, telle qu'elle est enregistrée usine/rules/SupplierDeliveries.l Copier ``` --- 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. Comment ça marche ## Trois étapes, de la base de données à une réponse vérifiée. 1. 1 ### Connecter les sources de données 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é. 2. 2 ### Poser une question 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. 3. 3 ### Conserver la connaissance 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. [SynaLemma en détail](/synalemma) [Réserver une démo](https://calendar.app.google/RMMAPbHYroAgiokb7) Accompagnement ## Un déploiement avec les spécialistes de l'équipe de développement. 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 : * Établir chaque définition avec les personnes qui répondent du chiffre. * Déterminer quelles données connecter, ce que veut dire chaque colonne et ce qui manque. * Vérifier techniquement chaque règle, en connaissant à la fois la logique et le métier. * Garder tout le travail dans la couche de connaissances du client, sans système sur mesure à côté. * Assurer la recherche, la maintenance et l'évolution du système, couvertes par la licence et l'accompagnement. [En savoir plus sur le déploiement](/services) Pourquoi SynaLinks ## Développé en interne, du framework d'agents au moteur logique. 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. * **1,4 k** étoiles GitHub * **1 k** téléchargements PyPI par mois * **Apache-2.0** composants open source La plateforme ### SynaLemma 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 SynaLemma](/synalemma) L'agent ### Synalinks Le 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 GitHub](https://github.com/SynaLinks/synalinks) La logique ### Synalog Un 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 GitHub](https://github.com/SynaLinks/synalog) La couche de connaissances ### Semantic Layers Le 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 GitHub](https://github.com/SynaLinks/semantic-layers) Le 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 source](/open-source) Pour qui ## Pour les organisations qui doivent pouvoir se fier à leurs chiffres. Quand un chiffre faux peut provoquer un arrêt de production ou un audit raté, _l'origine de chaque chiffre_ doit être établie. ### Industrie et production 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. ### Secteurs réglementés 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. ### Équipes au pilote IA enlisé 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. Commencer ## SynaLemma à l'œuvre sur une vraie question métier. 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. [Réserver une démo de SynaLemma](https://calendar.app.google/RMMAPbHYroAgiokb7) [En savoir plus sur le déploiement](/services)