Programme de recherche · version 1 · octobre 2026

Vers une IA embarquée déterministe et certifiable

Jean-René Denoual · EventCompute · chercheur indépendant, Bretagne

• 1. Introduction
• 2. Le socle
• 3. Le banc d’essai
• 4. La méthode
• 5. Expériences
• 6. Cartographie
• 7. Débouchés
• 8. Limites et suite
• Références

1. Introduction

Un même programme, lancé sur deux machines différentes, ne donne pas toujours le même résultat : les calculs en virgule flottante dépendent du processeur, du compilateur et de l’ordre des opérations. Pour la plupart des usages, l’écart est négligeable. Pour une IA embarquée dans un appareil, une machine ou un capteur, il pose une question de fond : comment prouver qu’un réseau, une fois réduit en précision et installé sur une puce, prend les mêmes décisions que le modèle d’origine ? Dans l’aéronautique, l’Agence de l’Union européenne pour la sécurité aérienne (EASA) demande déjà, dans ses lignes directrices sur l’IA, de vérifier que la réduction de précision et l’optimisation d’un modèle n’altèrent pas ses propriétés [11].

Ce programme part d’une exigence simple : un calcul ne compte que s’il peut être refait au bit près et vérifié par un tiers. Ses contributions sont les suivantes :

• un socle arithmétique normatif publié, ArithSpec, et quatre articles qui en tirent des certificats et des mesures de robustesse ;
• un banc d’essai d’apprentissage, déterministe et rejouable, et de premiers résultats ;
• une méthode de recherche dont seul un certificat valide les résultats, mise à l’épreuve sur des défis internationaux ;
• le projet d’une cartographie ouverte des calculs certifiés.

2. Le socle : ArithSpec et les certificats

ArithSpec est une spécification arithmétique pour réseaux de neurones à impulsions (calcul neuromorphique). Chacune de ses opérations est définie au bit près, avec son arrondi, sa saturation et des indicateurs qui signalent chaque anomalie au lieu de la masquer. Trois implémentations indépendantes, en C, en Python et en Rust, produisent la même empreinte de conformité sur des processeurs x86-64 et ARM [1] ; dans l’étude [5], un Raspberry Pi 5 reproduit au bit près les résultats obtenus sur un processeur x86-64.

Quatre articles en accès ouvert s’appuient sur ce socle :

• Certificat calculé à chaque pas de temps [2] : lorsqu’il est satisfait, et sous les hypothèses de l’article, il garantit qu’un réseau en virgule fixe émet exactement les mêmes impulsions que sa référence en virgule flottante. Sur 18 375 configurations, aucun faux positif n’a été observé et 74,17 % des configurations sont certifiées.
• Marges et précision réduite [3] : pendant l’entraînement testé, la marge interne diminue tandis que la marge de décision augmente.
• Robustesse au niveau des taux [4] : sur 18 375 configurations, 83,7 % conservent exactement le train d’impulsions et 99,8 % la décision.
• Quantification sur des connectomes [5] : étude exploratoire sur des réseaux instanciés à partir de connectomes publiés.

3. Le banc d’essai : un circuit d’apprentissage

Dans l’article [4], l’activité est propagée de façon déterministe dans des réseaux modélisés à partir du connectome de la drosophile publié par le consortium FlyWire [6], jusqu’au connectome complet de 139 255 neurones ; deux exécutions y donnent la même trace. Pour tester mes hypothèses sur l’apprentissage, j’utilise un circuit bien plus petit, modélisé à partir d’une partie de ce connectome.

Expérience. Le modèle apprend une première tâche, puis une seconde. On mesure ensuite sa performance sur la première. C’est la difficulté connue sous le nom d’oubli catastrophique : la plupart des réseaux de neurones perdent ce qu’ils savaient en apprenant autre chose.

Résultats. Le modèle conserve en partie la première tâche : sa performance reste au-dessus du hasard (environ 0,62 en moyenne sur une série d’étude de 12 individus simulés, contre 0,50 pour le hasard ; l’un d’eux reste sous le hasard), tout en baissant nettement par rapport au niveau atteint juste après le premier apprentissage. Sur les protocoles testés, ses décisions enregistrées se rejouent à l’identique, bit à bit, avec deux implémentations (Python et Rust). Après une interruption au milieu de la seconde tâche, la reprise depuis le point de sauvegarde redonne exactement le même état final (vérifié sur un cas test). Le protocole d’apprentissage est supervisé.

Frugalité. L’IA est conçue pour être frugale : tout le réseau est conservé, mais seule la partie nécessaire doit être activée à chaque instant. Le gain reste à mesurer.

Ce banc d’essai pourrait servir à d’autres équipes de recherche, dans d’autres domaines : simuler la propagation de l’activité dans un réseau entier, puis la rejouer pas à pas pour l’analyser.

4. La méthode

Dans la méthode de recherche, chaque hypothèse est testée par le calcul, et n’est retenue que si un certificat la prouve, c’est-à-dire si un programme indépendant de la recherche la vérifie. Des outils d’IA générative servent d’assistants. En développant ce projet, j’ai découvert qu’on pouvait l’adapter aux IA probabilistes d’une manière différente : c’est avec cette méthode que j’ai obtenu les résultats aux défis présentés ci-dessous. Chaque résultat certifié et chaque impasse y sont inscrits dans l’Atlas (§6).

Le fonctionnement interne de la méthode reste confidentiel. Ses résultats, eux, sont publics : un certificat se vérifie sans connaître la méthode qui l’a produit, comme une démonstration se vérifie sans connaître la personne qui l’a trouvée.

Moyens de calcul. Tout le travail tourne sur du matériel accessible : un PC de bureau (6 cœurs, 12 fils d’exécution, carte graphique NVIDIA RTX 3060 de 12 Go, processeur Intel Core i5, 32 Go de mémoire vive) ; un Raspberry Pi 5 et un microcontrôleur Raspberry Pi Pico, qui servent aussi à vérifier que le calcul reste identique d’une machine à l’autre ; et le serveur qui héberge ce site (4 processeurs virtuels), mis à contribution pour exploiter tout le calcul disponible. Ponctuellement, une instance de calcul de 32 processeurs virtuels a servi à étudier comment le calcul évolue avec la taille des problèmes.

5. Expériences : validation externe sur des défis internationaux

Pour mettre la méthode à l’épreuve, je l’ai appliquée à des défis scientifiques publics, choisis dans des domaines différents. Dans chacun, ce sont les organisateurs qui vérifient les solutions, avec leurs propres programmes. Les résultats ci-dessous sont donc validés par des tiers.

Positions relevées aux dates indiquées sur chaque page de défi ; elles peuvent avoir changé depuis.

Lecture. La même méthode produit des solutions acceptées par des arbitres indépendants dans quatre domaines distincts : la géométrie, la mécanique spatiale, les graphes et la théorie des nombres. Le détail de chaque résultat, avec sa source et sa date, figure sur la page Résultats.

6. L’Atlas : visualiser les problèmes et le monde de l’IA, et sa part ouverte

Une IA doit pouvoir visualiser les problèmes et le monde dans lequel elle évolue : l’Atlas est cette représentation, et celle sur laquelle je construis l’IA : elle s’enrichit de chaque résultat certifié et de chaque impasse, et les résultats aux défis ont été obtenus en les consignant ainsi. Ce n’est pas une boîte noire : chaque entrée porte son certificat, et comme tout se rejoue au bit près, l’effet d’une modification se mesure exactement. Je vise à étendre cette approche à un environnement visuel, pour des robots et des drones qui apprennent des conséquences de leurs actions. Tout calcul certifié une fois n’a plus besoin d’être refait. Je prépare un Atlas ouvert de ces calculs : chaque résultat avec son certificat, et les zones explorées, y compris celles qui n’ont rien donné. Elle permettra de ne jamais recalculer ce qui est prouvé, d’éviter les impasses déjà explorées, de repartir d’un résultat établi, de revérifier un résultat sans faire confiance, et de voir quels résultats dépendent les uns des autres. Détails →

7. Débouchés visés

Vision : une autre intelligence artificielle. Les grands modèles de langage sont probabilistes et gourmands en calcul ; ils ne suffisent pas seuls là où une décision doit être prouvée, rejouée et certifiée. Ce programme construit une IA d’une autre nature : déterministe et apprenante, qui ne retient que ce qu’un certificat prouve. Elle vise cinq voies : l’IA embarquée, l’identité des agents, la certification, l’audit et, en recherche parallèle, l’interaction avec les modèles de langage ; soit, en particulier : des agents d’IA fiables, la certification, et l’IA embarquée dans des robots, des drones et des machines autonomes.

• IA embarquée certifiable : prouver qu’un réseau en précision réduite, installé sur une puce, prend les mêmes décisions que le modèle d’origine.
• IA certifiable : des systèmes d’IA dont chaque décision peut être vérifiée par un tiers.
• Interaction avec les modèles de langage (recherche parallèle) : un cadre d’exécution contrôlé, une mémoire et une vérification rejouable autour de propositions probabilistes.
• Identité vérifiable des agents d’IA : une histoire que l’on peut rejouer à l’identique.
• Expertise après incident : rejouer exactement une décision passée pour comprendre ce qui s’est produit.
• Science reproductible et vérification pour les arbitres de classements scientifiques.

8. Limites et suite

• Les documents déposés sont des prépublications, non relues par des pairs.
• L’IA embarquée est au stade du prototype, au banc d’essai ; elle n’a pas encore été démontrée sur une tâche réelle.
• Les positions dans les classements sont datées et peuvent être reprises.
• Aucune forme de cognition ni de compréhension n’est revendiquée ; le banc d’essai ne prétend pas reproduire le fonctionnement de la mouche.
• Prochaines étapes : démontrer le prototype sur une tâche réelle, publier un premier Atlas, mesurer la frugalité, puis étendre la méthode à l’interaction avec les modèles de langage.

Références

1. J.-R. Denoual, A Normative Arithmetic Substrate for Bit-Exact Spiking Neural Networks (ArithSpec), Zenodo, 2026. DOI 10.5281/zenodo.20723008
2. J.-R. Denoual, Per-Tick Certification of Spike-Exact Fixed-Point Spiking Neural Networks, Zenodo, 2026. DOI 10.5281/zenodo.21749446
3. J.-R. Denoual, Internal Margins Collapse, Decision Margins Grow: Why Trained Spiking Networks Tolerate Low Precision, Zenodo, 2026. DOI 10.5281/zenodo.21750036
4. J.-R. Denoual, Rate-Level Robustness in Deterministic Spiking Networks: When Spike-Train Fidelity Overstates Observed Functional Fragility, Zenodo, 2026. DOI 10.5281/zenodo.21750042
5. J.-R. Denoual, Rate-Level Robustness under Quantization in Connectome-Instantiated LIF Models, Zenodo, 2026. DOI 10.5281/zenodo.21750053
6. S. Dorkenwald et al., « Neuronal wiring diagram of an adult brain », Nature 634, 2024 ; P. Schlegel et al., « Whole-brain annotation and multi-connectome cell typing of Drosophila », Nature 634, 2024 ; données FlyWire, version 783, utilisées à des fins de recherche selon leurs conditions d’utilisation. codex.flywire.ai (consulté le 07/10/2026)
7. E. Specht, table Packomania « csqv ». packomania.com (consulté le 04/10/2026)
8. Agence spatiale européenne, défi SpOC 4, plateforme ESA Optimize. github.com/esa/SpOC4 (consulté le 04/10/2026)
9. FlyWire Codex, défi Max Quasi-Cliques. codex.flywire.ai (consulté le 07/10/2026)
10. IBM Research, Ponder This, septembre 2026. research.ibm.com (consulté le 11/10/2026)
11. EASA, Artificial Intelligence Concept Paper, Issue 02, mars 2024. easa.europa.eu (consulté le 03/10/2026)