Le socle
ArithSpec et documents déposés
Deux exécutions d’un même programme, sur deux machines différentes, ne donnent 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 vérifier un calcul, il faut d’abord pouvoir le refaire à l’identique.
ArithSpec fixe ce résultat. C’est une spécification arithmétique normative : chaque opération est définie au bit près, avec son arrondi, sa saturation et des indicateurs qui signalent chaque approximation au lieu de la masquer. Selon le dépôt, trois implémentations indépendantes (C, Python et Rust) produisent la même empreinte SHA-256 de conformité sur processeurs x86-64 et aarch64.
La spécification
TitreA Normative Arithmetic Substrate for Bit-Exact Spiking Neural Networks
Publié13 juin 2026, Zenodo, accès ouvert, licence CC BY 4.0
Quatre articles
Publiés le 2 août 2026 sur Zenodo, en accès ouvert, licence CC BY 4.0, chacun avec ses données et un fichier d’empreintes pour contrôler les pièces.
APer-Tick Certification of Spike-Exact Fixed-Point Spiking Neural Networks. Un certificat calculé à chaque pas de temps garantit, sous des hypothèses écrites dans l’article, qu’un réseau en virgule fixe émet exactement les mêmes impulsions que le réseau de référence en virgule flottante. Sur 18 375 configurations testées, aucune configuration certifiée n’a divergé (aucun faux positif observé) ; 74,17 % des configurations sont certifiées. DOI 10.5281/zenodo.21749446
BInternal Margins Collapse, Decision Margins Grow: Why Trained Spiking Networks Tolerate Low Precision. Deux marges évoluent en sens contraire pendant l’entraînement testé : la marge interne diminue, la marge de décision augmente. Elles répondent à des questions différentes. DOI 10.5281/zenodo.21750036
DRate-Level Robustness in Deterministic Spiking Networks: When Spike-Train Fidelity Overstates Observed Functional Fragility. La fidélité impulsion par impulsion surestime la fragilité observée ; sur 18 375 configurations, 83,7 % conservent exactement le train d’impulsions et 99,8 % la décision. DOI 10.5281/zenodo.21750042
ERate-Level Robustness under Quantization in Connectome-Instantiated LIF Models. Étude exploratoire de la robustesse observée sous quantification, sur des réseaux instanciés à partir de connectomes publiés. DOI 10.5281/zenodo.21750053
Limites
Ces cinq documents sont des prépublications : ils ne sont pas relus par des pairs. La preuve du certificat de l’article A est rédigée à la main et n’est pas vérifiée par machine ; elle porte sur des neurones de type LIF dans un périmètre d’hypothèses écrit dans l’article. L’article E est exploratoire. Les versions corrigées, s’il y en a, paraissent comme nouvelles versions sur Zenodo ; l’historique reste consultable.
