Certification par tick de réseaux impulsionnels en virgule fixe à trains de spikes exacts

Pourquoi cette question compte

Vous avez un réseau de neurones qui fonctionne. Vous l’avez entraîné sur un ordinateur puissant, en virgule flottante — le mode de calcul par défaut des machines de laboratoire. Maintenant vous voulez le mettre dans un objet : un capteur, une prothèse, un drone, un implant. Ces objets n’ont pas de virgule flottante, ou pas assez de puissance pour se le permettre. Ils calculent en entiers.

Question simple, conséquences lourdes : le réseau embarqué se comporte-t-il comme celui que vous avez validé ? S’il diverge, ne serait-ce qu’un peu, votre validation ne vaut plus rien — vous avez certifié un système, vous en déployez un autre. Dans une prothèse ou un système critique, ce n’est pas un détail académique.

La réponse habituelle est : « exécutez les deux versions et comparez ». C’est lent, c’est cher, et surtout ça ne dit rien des millions de situations que vous n’avez pas testées. Ce travail propose autre chose : une garantie calculée à l’avance, qui couvre toutes les entrées d’un coup, ou qui refuse honnêtement de se prononcer.

Ce qu’une réponse utile doit garantir

Avant de proposer une méthode, le papier fixe la barre. Une réponse vraiment utile doit satisfaire trois exigences, et c’est à cette aune qu’il faut juger tout ce qui suit :

Retenez la troisième : elle reviendra à la fin, et c’est elle qui sépare un vrai certificat d’un simple prédicteur.

La formule du certificat

Pour chaque neurone i et chaque pas de temps t, on note E_i(t) une borne supérieure de l’écart entre potentiel flottant et potentiel entier, et m_i(t) la marge réelle — la distance du potentiel au seuil θ. Le certificat est le pire rapport des deux, sur toute la simulation :

Sous quelles hypothèses

Une garantie n’a de valeur que si son domaine est énoncé. Le certificat est prouvé exactement sous ces cinq conditions — ni plus, ni moins :

Le modèle d’erreur en neuf termes

D’où vient l’incertitude E_i(t) ? Elle s’accumule pas à pas, à partir de sources identifiées. C’est le cœur technique du papier : sept termes qui ajoutent de l’erreur, et deux règles de mise à jour d’état. Le terme n° 6 est celui qui change tout — vous verrez pourquoi plus bas.

L’esquisse de preuve

Le raisonnement est une récurrence sur le temps. Si toutes les décisions jusqu’au pas t−1 concordent entre les deux versions, alors elles partagent exactement le même historique — donc la somme de fan-in porte sur le même ensemble de neurones pré-synaptiques, et E_i(t) est une borne supérieure valide. Si de plus la marge dépasse l’incertitude pour tout neurone actif, le potentiel entier est nécessairement du même côté du seuil que le potentiel flottant. La décision ne peut pas basculer.

C’est cette récurrence qui rend le certificat global : R_cert > 1 affirme qu’aucune décision ne bascule nulle part, à aucun instant. Retenez bien ce mécanisme — c’est lui qui, plus loin, explique aussi pourquoi la méthode échoue pour les comptages d’impulsions.

Le résultat, montré directement

Voici la figure la plus importante du papier — celle qui porte toute la revendication. On prend les 18 375 configurations, on calcule le certificat de chacune, et on les range selon la vérité : celles qui sont réellement bit-exactes en vert, celles qui divergent en rose. Puis on regarde où tombe le seuil de certification.

C’est aussi frappant que simple : la revendication « zéro faux positif » n’est pas un chiffre dans un tableau, c’est une absence visible — le vide à droite de la ligne, du côté rose.

La matrice de décision

Le même résultat, sous forme comptable. On croise ce que le certificat dit avec ce qui est vrai :

Lecture : précision 1,000 (tout ce qui est certifié est exact), spécificité 1,000 (aucune divergence certifiée), rappel 0,886 (on reconnaît 88,6 % des cas exacts). La couverture — la part du corpus qu’on garantit — est de 74,17 %. Le revers : 1 758 configurations pourtant bit-exactes ne sont pas certifiées. Le certificat est prudent ; face au doute, il se tait plutôt que de risquer une erreur.

Le certificat s’étale sur une plage énorme : sa médiane est à 12,4, son quantile 95 à 5 256. Autrement dit, la plupart des configurations certifiées ne sont pas « juste au-dessus » du seuil — elles sont très largement au-dessus. La marge de sécurité est confortable là où elle existe.

Est-ce stable ?

Un résultat qui ne tient que sur une graine chanceuse ne vaut rien. On vérifie donc que la solidité ne dépend ni du tirage aléatoire, ni de l’architecture du réseau.

Même chose par architecture : AUC de 0,9925 à 0,9972, couverture de 71,27 % à 75,71 %, et toujours aucun faux positif. La garantie ne dépend pas de quel réseau vous certifiez — seulement de combien il vous en certifie.

L’ingrédient décisif

Voici le résultat le plus instructif du papier, et c’est un résultat négatif. Il concerne le terme n° 6 du modèle d’erreur : le fan-in synaptique.

Que se passe-t-il si on l’oublie ? Une enveloppe qui borne chaque neurone isolément, sans compter l’erreur qui arrive par les synapses, certifie à tort 1 898 configurations qui divergent en réalité. Elle est non seulement imparfaite : elle est dangereuse, parce qu’un certificat qui ment une fois ne certifie plus rien.

Le tableau ci-dessous compare quatre façons de noter le même corpus. Il résume tout l’enjeu :

Où la divergence se cache

Question naturelle : qu’est-ce qui fait diverger un réseau ? La réponse est nette, et ce n’est pas l’architecture.

L’épreuve du feu

Un certificat ne se juge pas sur les cas faciles. On a donc construit 520 configurations conçues pour le piéger : synchronisation maximale des synapses, saturation, seuils pile sur une frontière d’arrondi, poids poussés aux limites, décharge dès le premier instant, mémoire très longue près du seuil.

Deux lignes racontent quelque chose. Les 160 configurations « à un demi-cran du seuil » sont toutes réellement bit-exactes — et aucune n’est certifiée. Le certificat y est maximalement prudent : il n’a pas tort, il est silencieux, et cette ligne mesure le prix de sa prudence. La ligne « mémoire longue près du seuil » est la seule où de vraies divergences existent (11 sur 30) : le certificat en certifie 17, dont aucune divergente.

La distinction cruciale : sur 520 pièges, 460 sont dans le domaine du théorème et 0 le mettent en défaut. Les 60 cas saturants sont hors hypothèse H3 : le critère y dépasse 1 sans divergence observée, mais ce n’est pas une certification par le théorème. Le domaine où une preuve s’applique et le domaine où l’on a observé un bon comportement sont deux choses différentes, et ce site ne les confond jamais.

Là où la méthode échoue

Le sous-titre du papier est « et pourquoi la même technique échoue pour les comptages ». Voici la frontière exacte de la technique, et pourquoi elle passe précisément là.

L’idée séduisante serait d’étendre le certificat des instants d’impulsion au simple nombre d’impulsions. On pourrait accepter que les impulsions se décalent un peu, tant que leur compte reste identique. Mais la borne par-neurone qui marchait pour les instants devient non saine pour les comptages : elle est violée sur 2 660 des 18 375 configurations.

Pourquoi cet échec ? Il remonte directement à la récurrence de la preuve. La borne d’un neurone suppose qu’il reçoit le même signal entrant dans les deux versions. C’est vrai tant que rien n’a divergé. Mais dès qu’un seul neurone diverge, cette hypothèse tombe pour tous les neurones en aval — et leurs bornes ne veulent plus rien dire.

La certification locale, neurone par neurone, n’est pas fermée sous la causalité du réseau : une divergence locale peut invalider les bornes de tous les neurones qu’elle peut atteindre.

Il existe bien une borne saine pour les comptages — mais elle est vide de sens. Sur 193 configurations dont l’erreur de comptage réelle est exactement zéro, cette borne « sûre » certifie encore une erreur possible de 4 807 en moyenne. Elle a raison, techniquement, et elle est inutile. Le papier la présente pour ce qu’elle est — un repli universel après perte de synchronisation — et jamais comme un certificat de taux.

Trois exigences emboîtées

Ce diagnostic ouvre une structure élégante. Sur ce corpus, trois niveaux d’exigence s’emboîtent, du plus strict au plus lâche :

Deux nuances d’honnêteté statistique, que le papier tient à préciser. La coquille externe de 88 configurations à corrélation parfaite mais comptages inégaux n’est pas une anomalie : une corrélation de 1 signifie « relation affine », pas « vecteurs égaux ». Et deux configurations montrent une corrélation négative — signalées comme une décorrélation de régime réelle, non diagnostiquée, plutôt qu’écartées comme du bruit.

Certifier la décision, pas l’impulsion

Pour une tâche de classification, exiger que toutes les impulsions coïncident est plus strict que nécessaire. Ce qui compte vraiment, c’est que la classe gagnante reste la même. On peut donc mesurer directement la survie de la décision.

Le piège, c’est l’exigence n° 3 du début. Ce prédicteur de décision a besoin, pour être calculé, de connaître l’erreur réelle de chaque sortie — ce qui exige d’avoir déjà exécuté la version entière. Il est donc post-exécution : excellent, mais ce n’est pas un certificat a priori. L’appeler « certificat » violerait la règle qu’on s’est fixée.

Périmètre et Limitations

Reproductibilité algorithmique

rcert_pertick_sweep_v2.jsonl   041394d161497d0c   (18 375 lignes brutes)
rcert_analysis_v2.json         91e864d4b1a88a7a   (analyse principale)
rcert_adversarial_summary.json 7ccfa73c94467e35   (les 520 pièges)
driver du sweep                9fcf5b3661c32213   (script de mesure)
cœur de simulation gelé        21332f7d25e1c15f

sha256sum -c SHA256SUMS.txt