Aller au contenu

Situation

Ancrage contextuel et État de l’Art

Cette recherche étend plusieurs corpus de l’architecture neuromorphique et de l’arithmétique embarquée. Le tableau suivant consolide l’état de l’art, l’héritage scientifique du projet et la proposition de valeur strictement causale qui justifie la création de cette architecture.

Fondations Computationnelles

L’arithmétique entière à arrondi spécifié n’a rien d’inédit, et tant mieux : le terrain est solide. Le standard ISO/IEC TR 18037 normalise les types à virgule fixe en C. CMSIS-DSP travaille en Q15 et Q31 sur ARM depuis des années. SpiNNaker tourne en s16.15 depuis 2011, précisément pour obtenir de la reproductibilité. Et gemmlowp a déployé du calcul entier reproductible sur des milliards d’appareils.

Je pars de là. La question que je me suis posée n’était pas « comment faire du calcul entier », elle était : qu’est-ce qu’il me faudrait en plus pour qu’un tiers puisse vérifier mon résultat sans me faire confiance et sans acheter mon matériel ?

Travaux Ce qu’ils apportent Ce que je cherchais en plus
SpiNNaker L’échelle, le matériel spécialisé, une décennie d’usage réel et une communauté. Arithmétique déterministe de longue date. Une spécification que n’importe qui puisse implémenter sur du matériel générique, avec une empreinte publiée pour prouver sa conformité.
Loihi La plasticité sur puce et des mesures d’efficacité énergétique réelles, que je n’ai pas. Un comportement rejouable en dehors de la puce, pour qu’un contradicteur puisse refaire l’expérience chez lui.
gemmlowp, TFLite La preuve à grande échelle que l’entier reproductible est industriellement viable. Un journal des approximations opération par opération, et le cas impulsionnel, qui pose des problèmes différents.
NEST, Brian2, NEURON L’écosystème, la validation communautaire, la richesse des modèles neuronaux. Une équivalence bit-exacte entre moteur événementiel et moteur dense, là où le flottant impose de se contenter d’une équivalence numérique.
Vérification de réseaux quantifiés
CROWN, DeepPoly, Marabou
Un champ mature et outillé, avec des garanties formelles solides. Ma méthode descend de cette famille. L’adaptation de ces techniques au cas impulsionnel, où la grandeur à préserver est une décision de seuil, discrète, et non une sortie continue.
Connectomique par ordinateur
FlyWire et travaux associés
L’échelle, la fidélité biologique et des prédictions validées in vivo. Mon banc d’essai vient directement de leurs données. Un système qui apprenne de ce qu’il rencontre. C’est une question distincte de la fidélité de la reconstruction, et ils ne se la posent pas.

La case que j’occupe

Ce n’est pas l’arithmétique entière, qui existe partout. C’est une combinaison de quatre propriétés que j’ai réunies parce que j’en avais besoin ensemble : une spécification normative gelée, avec un numéro de version ; le signalement de chaque arrondi et de chaque saturation, opération par opération ; une sérialisation canonique ; et une empreinte de conformité publiée, qui permet à n’importe quelle implémentation tierce de se déclarer conforme et de le prouver.

Ce que ça produit est concret : un contradicteur télécharge la spécification, écrit son implémentation dans le langage qu’il veut, la fait tourner sur la machine qu’il veut, et compare une empreinte. Il n’a besoin ni de mon code, ni de mon matériel, ni de mon accord.

Ce que ça ouvre

Une spécification qu’on peut implémenter indépendamment devient un point de référence : quand deux systèmes divergent, elle dit lequel s’est écarté du contrat. C’est le rôle que je vise pour ce substrat, aux côtés des formats d’échange existants plutôt qu’en concurrence avec eux. Une passerelle vers l’un de ces formats est construite et passe ses tests de conformité.

Les comparaisons qui restent à faire

Elles sont un programme de travail, et plusieurs se feraient bien en collaboration.

1Évaluation croisée du critère de préservationcontre les outils de vérification de réseaux existants, sur un corpus communà mener
2Comparaison de performance sur matériel dédiédemanderait un protocole équitable entre matériel générique et neuromorphiqueà construire
3Antériorité en théorie des nombresune revue a identifié un recouvrement ; la affirmation d’originalité a été retiréefait

Un voisin que j’aurais manqué

Si un travail existant couvre déjà ce que je décris, la référence m’intéresse davantage qu’une confirmation. C’est le genre de message auquel je réponds en priorité.

M’écrire