NEURO-SYMBOLIQUE
Le modèle propose.
L’IA neuro-symbolique réunit deux formes d’intelligence : un qui lit et écrit comme une personne, et un qui raisonne comme un mathématicien. Cette page explique les deux, ce qu’est un moteur de vérification formelle automatisée, et où chacun se trouve exactement dans Ironproof.
ARCHITECTURE
01 — Deux formes d’intelligence
L’une apprend par l’exemple. L’autre suit les règles jusqu’au bout.
Chacune est forte là où l’autre est faible. C’est toute la raison de les combiner.
Le modèle de langage
Apprend des motifs à partir d’immenses quantités de texte. Il comprend une demande floue, écrit du code, résume un contrat, s’adapte à ce qu’il n’a jamais vu.
- Fort pour
- Le langage, l’ambiguïté, la vitesse, l’étendue.
- Faible pour
- Les garanties. Il est probabiliste : il peut se tromper avec assurance, et on peut le faire changer d’avis.
Le solveur
Travaille sur des règles exactes écrites en logique. Devant une règle et un système, il examine tous les cas possibles — pas un échantillon — et rend une réponse que n’importe qui peut revérifier.
- Fort pour
- La certitude. Sa réponse vaut pour tous les cas de la classe examinée.
- Faible pour
- Lire le monde. Il lui faut une question déjà écrite avec précision.
02 — Neuro-symbolique
Laissez le modèle créer.
Un système neuro-symbolique place chaque partie là où elle est fiable. Le côté neuronal s’occupe du langage : il propose une action, une traduction, une réponse candidate. Le côté symbolique la confronte à des règles fixées d’avance, et seul le côté symbolique peut dire oui.
L’ordre compte. Un modèle qui en note un autre reste un modèle — on peut l’influencer, le convaincre, ou il peut simplement se tromper. Un solveur ne se laisse pas convaincre : soit la règle tient dans tous les cas, soit il rend le cas exact où elle casse.
L’intelligence sans preuve est une supposition. La preuve sans intelligence ne quitte jamais le labo. Ensemble, elles livrent.
03 — Le moteur
Ce qu’est un moteur de vérification formelle automatisée.
La vérification formelle, c’est prouver par les mathématiques qu’un système respecte une règle — pour toutes les entrées, pas seulement celles qu’on a testées. Pendant des décennies, il fallait des spécialistes qui écrivaient les preuves à la main ; c’est pourquoi elle est restée dans l’aérospatial, les puces et la cryptographie.
Automatisée veut dire que le moteur fait ce travail lui-même. Nous utilisons Z3 et son moteur Spacer : on lui donne la règle et le système, et il cherche une preuve — y compris l’invariant inductif, la propriété qui reste vraie à chaque étape — ou un contre-exemple. Aucun mathématicien dans la boucle. Un solveur peut rendre trois sortes de réponse :
Aucun cas ne viole la règle.
Pas « nous n’en avons pas trouvé ». Le solveur montre qu’il ne peut pas en exister — le mot technique est UNSAT, insatisfaisable.
Voici le cas exact.
Les entrées, l’état, l’étape où la règle tombe. Assez concret pour le rejouer et corriger.
Pas tranché.
Certaines questions sont trop difficiles à fermer dans le temps donné. Indécis n’est pas un succès, et un système honnête ne le compte jamais comme tel.
04 — Comment tout s’assemble dans Ironproof
D’une action proposée à une preuve entre vos mains.
Un seul moteur, les mêmes étapes sur chaque surface. Le modèle ne peut apparaître qu’à la première.
- 01 · PROPOSER
Un agent IA demande à agir
Un remboursement, un paiement, un accès, un déploiement. La demande peut venir d’un modèle — c’est la partie neuronale, et c’est là que naissent les erreurs et les manipulations.
- 02 · COMPILER
Votre règle devient logique
Votre politique est compilée une seule fois vers la forme que lit le solveur et celle qu’applique l’exécution. Un seul compilateur, pour que les deux ne puissent pas diverger en silence.
- 03 · PROUVER
Le moteur tranche
Le solveur prouve que la règle tient sur les séquences d’actions, ou rend le contre-exemple. À l’exécution, chaque action est confrontée à cette même règle compilée, et rien ne s’exécute sans décision favorable.
- 04 · REVÉRIFIER
Ne pas faire confiance à la recherche
L’invariant trouvé par le solveur est revérifié dans un solveur neuf avant tout scellement. Trouver une preuve et la vérifier restent séparés, exprès.
- 05 · SCELLER
Registre post-quantique
La décision et sa preuve sont chaînées par hachage et signées Ed25519 et ML-DSA-65 (FIPS 204). Toute modification ultérieure se détecte.
- 06 · VÉRIFIER
Hors ligne, sans nous
Votre auditeur revérifie le registre scellé avec un vérificateur indépendant, sans jamais contacter Ironproof.
05 — Où se trouve le modèle, exactement
Sur le chemin de décision,
Le chemin de production qui autorise l’action d’un agent n’appelle aucun modèle de langage. Dans notre tribunal de recherche, un modèle peut lire la demande et donner son avis sur l’intention — cet avis est consigné dans le registre scellé et n’est jamais compté. La même demande, dans le même état, sous la même politique, reçoit le même verdict, que le modèle soit d’accord, en désaccord ou injoignable.
La décision elle-même se prend en évaluant vos règles, et ce raccourci est autorisé par un théorème vérifié en Lean 4 : décider par évaluation et décider par le solveur donnent la même réponse pour toute politique et toute action. Le côté neuronal apporte la compréhension. Le côté symbolique garde le dernier mot.
06 — Ce qu’il ne fait pas
Les limites, dites d’entrée de jeu.
Une preuve ne vaut que la règle.
Le moteur prouve que votre système respecte la règle écrite. Que cette règle dise ce que vous vouliez dire est une question humaine — c’est aujourd’hui la partie la plus difficile du travail, et nous la faisons avec vous.
Prouvé dans une classe, pas partout.
Chaque preuve couvre une classe d’actions et de règles énoncée avec précision. Hors de cette classe, elle ne dit rien — et le registre en déclare la frontière.
Nous ne rendons pas le modèle sûr.
Un modèle compromis ou confus peut encore demander la mauvaise chose. Nous faisons en sorte qu’il ne puisse pas l’obtenir si la règle ne le permet pas. Durcir le modèle lui-même est un autre travail.
07 — Lexique
Les mots, en une ligne chacun.
- Un modèle qui apprend des motifs à partir de données. Les modèles de langage en sont.
- Un calcul sur des règles et une logique explicites, dont chaque étape se vérifie.
- Un système qui combine les deux, chacun là où il est fiable.
- Une preuve mathématique qu’un système respecte une règle pour toute entrée.
- Le moteur qui décide si une formule logique peut être satisfaite. Z3 en est un.
- « Insatisfaisable » : aucun cas ne viole la règle. La réponse sur laquelle repose une preuve.
- Un cas concret où la règle tombe.
- Une propriété vraie au départ et préservée par chaque étape — donc vraie pour toujours.
- Une signature conçue pour rester infalsifiable même face aux futurs ordinateurs quantiques.
NEURO-SYMBOLIQUE
Voyez le moteur sur l’un de vos processus
Choisissez une action que prennent vos agents. Nous écrivons la règle avec vous, nous la prouvons, et nous vous remettons le registre.