Rewriting Logic using Strategies for Neural
Networks: an Implementation in Maude
Résumé
Introduction
Conclusion
Section 2 :Maude
Cet article propose une nouvelle méthode pour modéliser les réseaux neuronaux en utilisant la réécriture logique.
Le modèle proposé utilise une architecture de réseau multicouche à propagation avant(forward-propagation multilayer network)
En s'appuyant sur des modèles existants de parallélisme et de concurrence implémentés en réécriture logique( tels que les réseaux de Petri, les automates cellulaires, les machines de Turing parallèles, les systèmes de transitions étiquetées, etc.)
les auteurs combinent des opérations de représentation appropriées(pour organiser les données, telles que le codage et la transformation des données d'entrée, les poids synaptiques, etc. )avec la disponibilité de stratégies (sont utilisées pour guider l'application des règles de réécriture logique, en déterminant l'ordre d'application des règles et en optimisant le processus de réécriture pour atteindre les objectifs du modèle. )
. Cette combinaison vise à améliorer la performance et l'applicabilité de l'algorithme de rétropropagation classique dans le contexte de la réécriture logique appliquée aux réseaux neuronaux.
Un exemple de diagnostic du glaucome est présenté pour démontrer l'efficacité du modèle
Les résultats expérimentaux montrent que le modèle est performant et pratique.
Mots-clés : Réseaux neuronaux, réécriture logique, Maude, stratégies, exécutabilité.
La logique de réécriture est une logique de changement concurrent qui peut traiter naturellement les états et les calculs concurrents hautement non déterministes. Elle présente de bonnes propriétés en tant que cadre sémantique flexible et général pour donner une sémantique à un large éventail de langages et de modèles de concurrence.
la logique de réécriture a été proposée comme un cadre unificateur dans lequel de nombreux modèles de concurrence peuvent être représentés, tels que les systèmes de transition étiquetés, la programmation orientée objet concurrente ou CCS,
Les réseaux neuronaux artificiels sont un autre modèle important de calcul parallèle.
Objectif :combler le manque de correspondance concrète entre la logique de réécriture et les réseaux neuronaux.
Les auteurs proposent une représentation des réseaux neuronaux en utilisant la logique de réécriture, en prenant en compte à la fois l'évaluation des motifs par le réseau et l'apprentissage nécessaire pour obtenir de bonnes performances.
Pour ce faire, ils utilisent Maude, un système exécutable basé sur la logique de réécriture.
Maude est un langage et un système performant qui prend en charge à la fois le calcul équationnel et le calcul de la logique de réécriture pour une large gamme d'applications.
Prend également en charge le calcul de la logique de réécriture.
Mathématiquement, une règle de réécriture a la forme l: t → t' si Cond avec t, t' sont des termes du même type pouvant contenir des variables.
Une règle de réécriture mathématique dans Maude décrit une transition locale concurrentielle dans un système, où une substitution d'état peut être remplacée par un nouvel état local.(chaque fois qu'une instance de substitution σ(t) est trouvée, une transition locale de ce fragment d'état vers le nouvel état local σ(t'))
Maude est une extension de Maude qui offre une algèbre de module avancée avec des modules paramétrés, des opérations de composition de modules et une syntaxe spéciale pour les spécifications orientées objet. Ces fonctionnalités orientées objet sont utilisées dans la spécification des réseaux neuronaux.
2.1 Object oriented modules
Les modules orientés objet dans Maude permettent de représenter les objets et leurs états.
Un objet dans un état donné est représenté sous la forme d'un terme < O : C | a1 : v1, ..., an : vn >, où O est le nom de l'objet, appartenant à un ensemble Oid d'identifiants d'objets, C est sa classe, les ai sont les noms des attributs de l'objet, et les vi sont leurs valeurs correspondantes. Les messages sont définis par l'utilisateur pour chaque application.
Dans un système orienté objet concurrent, l'état concurrent, appelé configuration, est structuré comme un multiset composé d'objets et de messages.
L'évolution de cet état se fait par réécriture concurrente en utilisant des règles qui décrivent les effets des événements de communication entre objets et messages.
Les règles de réécriture spécifient de manière déclarative le comportement associé aux messages. La forme générale de ces règles est la suivante :
où k, p, q ≥ 0, les Ms sont des expressions de messages, i1, ..., ik sont des nombres différents parmi les originaux 1, ..., m, et Cond est une condition de règle. Le résultat de l'application d'une règle de réécriture est que les messages M1, ..., Mn disparaissent ; l'état et éventuellement la classe des objets Oi1, ..., Oik peuvent changer ; tous les autres objets Oj disparaissent ; de nouveaux objets Q1, ..., Qp sont créés ; et de nouveaux messages sont générés.
2.2 Maude’s strategy language
Le langage de stratégie de Maude permet de contrôler l'application des règles de réécriture aux termes en logique de réécriture.
Il offre des moyens de garantir que le processus de réécriture se déroule de manière souhaitée et termine correctement, même si les règles de réécriture peuvent être non convergentes et non terminantes.
Les stratégies sont définies dans un module séparé et sont exécutées à l'aide de commandes spéciales.
Les stratégies de Maude peuvent être de différents types
Le constante "idle"
Le constante "fail"
Réussissent toujours
Echouent toujours
Les stratégies de base
Appliquer une règle à un terme donné, avec la possibilité de spécifier une substitution pour les variables de la règle.
Les combinateurs de stratégie permettent de composer des stratégies de base pour créer des stratégies plus complexes.
Parmi ces combinateurs, on trouve la concaténation (;), l'union (|), l'itération (* pour 0 ou plusieurs itérations, + pour 1 ou plusieurs itérations, et ! pour une itération "répéter jusqu'à la fin"). Il existe également un combinateur "si-alors-sinon" généralisé où le premier argument est également une stratégie. Le langage propose également un combinateur "matchrew" qui divise un terme en sous-termes et spécifie comment ces sous-termes doivent être réécrits. La récursion est possible en donnant un nom à une expression de stratégie et en utilisant ce nom dans l'expression de stratégie elle-même ou dans d'autres stratégies associées.
Dans l'implémentation discutée dans l'article, l'utilisation complète et complexe du langage de stratégie de Maude n'est pas nécessaire.
Les stratégies sont exprimées en combinant l'application de règles spécifiques, éventuellement instanciées, avec la concaténation et l'itération "répéter jusqu'à la fin". Un combinateur étendu appelé "one(S)" a été introduit pour des raisons d'efficacité. Lorsqu'il est utilisé sur un terme, ce combinateur renvoie l'une des solutions possibles obtenues en appliquant la stratégie S au terme. Ainsi, une approche simplifiée et optimisée est adoptée pour contrôler le processus de réécriture.
Combler = Résoudre une incomplétude entre deux domaines
Section 3 Multilayer perceptrons
Les perceptrons multicouches (ou réseaux de neurones multicouches)
Sont des réseaux neuronaux qui utilisent des couches intermédiaires de nœuds pour traiter les informations entre les entrées et les sorties.
Chaque nœud dans le réseau est associé à une sortie, et les connexions entre les nœuds ont des poids qui déterminent leur influence. Chaque nœud a également un seuil d'activation, et une fonction de transfert est utilisée pour calculer l'activation du nœud en fonction de ses entrées.
Les couches intermédiaires sont entièrement connectées, ce qui signifie que chaque nœud de la couche reçoit des entrées de tous les nœuds de la couche précédente et transmet ses résultats à tous les nœuds de la couche suivante. Les nœuds au sein de chaque couche ont la même fonction de transfert, qui est généralement une fonction sigmoïde permettant de produire une sortie continue entre 0 et 1.
3.1 The backpropagation algorithm
Un algorithme permettant d'ajuster les poids.
Il utilise une méthode de descente de gradient pour minimiser l'erreur quadratique moyenne entre les sorties réelles du perceptron et les sorties désirées.
Section 4: Implementing the multilayer perceptron
La spécification d'un perceptron à trois couches en Maude
la conception d'une stratégie d'évaluation et d'entraînement
Pour avoir un réseau en fonctionnement, nous devons spécifier le nombre de couches, les neurones dans chaque couche, les poids de toutes les connexions, ainsi que les motifs d'entrée qui, en général, seront multiples.
Bien que la représentation orientée objet soit très pratique pour spécifier leur comportement, il est clair qu'introduire toutes ces données directement sous cette forme serait très fastidieux.
Par conséquent, nous avons décidé d'utiliser des matrices et des vecteurs de valeurs pour spécifier les seuils et les poids, Et de définir des équations et des règles pour les transformer en représentation orientée objet.
Le cœur de notre représentation des perceptrons en Maude tourne autour de la définition de deux classes pour représenter les neurones et les synapses en tant qu'objets individuels :
class Neuron | x : Float, t : Float, st : Nat .
Chaque objet de neurone transporte sa valeur d'activation actuelle x, en fonction de son seuil t, et un attribut st qui sera utilisé pour déterminer si le neurone a déjà été activé ou non
class Link | w : Float, st : Nat .
les objets de lien stockent leur poids numérique et contiennent un attribut st pour indiquer si une valeur a déjà transité à travers eux ou non
Un réseau est donc une "soupe" (un multi-ensemble) de neurones et de liens.
Exemple
Supposons que nous ayons un neurone avec une valeur de seuil t = 0.5. La fonction d'activation utilisée est la fonction sigmoïde, qui renvoie des valeurs dans la plage [0, 1].
Au départ, la valeur d'activation x du neurone est initialement définie à 0.
Un stimulus est envoyé au neurone, et son activation est calculée en utilisant la fonction d'activation sigmoïde.
Si la valeur d'activation obtenue est supérieure au seuil t (0.5 dans notre cas), alors le neurone est considéré comme activé et l'attribut st est mis à une valeur indiquant qu'il a été activé.
Sinon, si la valeur d'activation est inférieure ou égale au seuil t, le neurone n'est pas activé et l'attribut st indique qu'il est toujours en attente d'entrée.
Par la suite, d'autres stimuli peuvent être envoyés au neurone et son activation mise à jour en fonction du nouveau stimulus et du seuil.
Par exemple, si un stimulus donné entraîne une activation de 0.8, qui est supérieure au seuil de 0.5, alors le neurone est considéré comme activé et l'attribut st est mis à une valeur indiquant qu'il a été activé.
Les neurones et les liens sont identifiés par un nom. Nous définissons deux opérations qui prennent des nombres naturels en tant qu'arguments et renvoient un identifiant d'objet : pour les neurones, les nombres correspondent à la couche et à la position au sein de la couche ; pour les liens, les nombres correspondent à la couche de sortie et aux positions respectives au sein de chaque couche des neurones connectés.
op neuron : Nat Nat -> Oid .
Pour créer un objet de neurone dans la deuxième couche à la position 3, nous utilisons l'opération neuron(2, 3), qui renverra un identifiant d'objet unique pour ce neurone.
Exemple :op neuron : Nat Nat -> Oid .
eq neuron(2, 3) = NeuronObj123 .
Dans cet exemple, NeuronObj123 est l'identifiant d'objet unique pour le neurone dans la deuxième couche à la position 3.
op link : Nat Nat Nat -> Oid .
Pour créer un objet de lien qui connecte un neurone dans la première couche à un neurone dans la deuxième couche, à la position 2 dans la première couche et à la position 1 dans la deuxième couche, nous utilisons l'opération link(1, 2, 1), qui renverra un identifiant d'objet unique pour ce lien.
Exemple: op link : Nat Nat Nat -> Oid .
eq link(1, 2, 1) = LinkObj121 .
Dans cet exemple, LinkObj121 est l'identifiant d'objet unique pour le lien entre le neurone dans la première couche à la position 2 et le neurone dans la deuxième couche à la position 1.
click to edit
Dans l'exemple eq link(1, 2, 1) = LinkObj121, les nombres 1, 2 et 1 correspondent aux arguments de l'opération link. Voici comment ils sont interprétés :
Le premier 1 indique que le lien provient de la première couche.
Le 2 indique la position du neurone dans la première couche à partir duquel le lien se connecte.
Le dernier 1 indique la position du neurone dans la deuxième couche auquel le lien est connecté.
La deuxième couche n'est pas explicitement mentionnée dans l'opération link. Cependant, la signification de la position 2 dans la première couche et la position 1 dans la deuxième couche est implicite pour indiquer la connexion entre ces deux neurones.
En résumé, l'opération link(1, 2, 1) crée un lien entre un neurone de la première couche à la position 2 et un neurone de la deuxième couche à la position 1.
click to edit
s
Les règles fournies décrivent l'évaluation du réseau. Les règles "feedForward" et "sigmoid" sont appliquées de manière répétée pour effectuer l'évaluation. Voici une explication de ce que font ces règles :
Règle "feedForward" :
click to edit
Cette règle calcule la somme pondérée des entrées d'un neurone et met à jour la valeur d'activation (x) et l'état de déclenchement (st) des neurones et des liens impliqués.
Le motif de règle "<neuron(L, I) : Neuron | x:X1, st:1>" correspond à un neurone "neuron(L, I)" avec une valeur d'activation X1 et un état de déclenchement 1.
Le motif de règle "<link(s L, I, J) : Link | w:W, st:0>" correspond à un lien "link(s L, I, J)" avec un poids W et un état de déclenchement 0.
Le motif de règle "<neuron(s L, J) : Neuron | x:X2, st:0>" correspond à un neurone "neuron(s L, J)" avec une valeur d'activation X2 et un état de déclenchement 0.
Lorsque ces motifs sont correspondants, la règle met à jour la valeur d'activation et l'état de déclenchement des neurones et du lien impliqués dans le calcul.
La configuration résultante après l'application de la règle est "<neuron(L, I) : Neuron | x:X1, st:1> <link(s L, I, J) : Link | w:W, st:1> <neuron(s L, J) : Neuron | x:(X2 + (X1 * W)), st:0>".
Règle "sigmoid" :
click to edit
Cette règle applique la fonction sigmoïde ("sig") à l'entrée nette d'un neurone et met à jour sa valeur d'activation et son état de déclenchement.
Le motif de règle "<neuron(L, I) : Neuron | x:X, t:T, st:0>" correspond à un neurone "neuron(L, I)" avec une valeur d'activation X, un seuil T et un état de déclenchement 0.
Lorsque ce motif est correspondant, la règle applique la fonction sigmoïde à l'entrée nette et met à jour la valeur d'activation et l'état de déclenchement du neurone.
La configuration résultante après l'application de la règle est "<neuron(L, I) : Neuron | x:syg(-(X, T), L), st:1>".
Ces règles font partie du processus d'évaluation du réseau et sont utilisées pour propager les signaux d'entrée à travers le réseau, calculer les activations et mettre à jour l'état de déclenchement des neurones et des liens.
L'évaluation d'un perceptron commence par l'obtention d'un motif d'entrée grâce à la règle "nextPattern", qui est guidée par le message "netStatus". Un message de la forme "netStatus(N0, 0, 0, N1)" signifie que le N0-ème motif doit être considéré, suivi des motifs suivants jusqu'au N1-ème.
La règle "nextPattern"
Lorsque le motif de message "netStatus(N, N1, N2, N0)" est correspondant, la règle incrémente le numéro du motif en cours (s N) et applique les règles d'insertion des motifs d'entrée et de sortie correspondants.
La règle met également à jour les indices pour indiquer les prochains motifs à considérer.
Si N est inférieur à N0, la règle est appliquée.
Avant de commencer le processus de feedforward, les valeurs des neurones dans la couche d'entrée et les poids correspondants sont réinitialisés. Ensuite, la règle "introducePattern" insère le motif d'entrée dans les neurones de la couche d'entrée et les supprime de la configuration.
Une fois que nous avons terminé l'évaluation de tous les motifs, nous calculons l'erreur et marquons l'objet net(N) courant comme étant terminé.
La règle "introducePattern" :
La règle "computeError" :
Lorsque le motif "<neuron(0, I) : Neuron | x:X, st:0>" correspond à un neurone de la couche d'entrée avec une valeur d'activation X et un état de déclenchement 0, et que le motif "inputPattern(N, I, X0)" correspond à un motif d'entrée avec un numéro de motif N, un indice I et une valeur X0, la règle met à jour la valeur d'activation du neurone avec X0 et l'état de déclenchement à 1.
Lorsque le motif "<net(N0) : Net | e:E, st:0>" correspond à un objet net avec une erreur E et un état de déclenchement 0, et que le motif "<neuron(2, I) : Neuron | x:X0, st:1>" correspond à un neurone de la couche de sortie avec une valeur d'activation X0 et un état de déclenchement 1, et que le motif "outputPattern(N, I, X1, 0)" correspond à un motif de sortie avec un numéro de motif N, un indice I, une valeur X1 et un état de déclenchement 0, la règle met à jour l'erreur en fonction de la différence entre X1 et X0.
L'état de déclenchement du neurone de la couche de sortie est également mis à jour.
Ces règles sont utilisées dans le processus d'évaluation du perceptron pour traiter les motifs d'entrée, effectuer le feedforward, calculer l'erreur et marquer l'objet net comme étant terminé.
4.1 Backpropagation in Maude
confrontés à la tâche de former le réseau
Pour cela, nous devons ajouter des informations supplémentaires aux neurones et aux liens, à savoir les termes d'erreur δj et les poids ajustés ωkij (t+1).
Puisque l'évaluation fait partie de la rétropropagation, nous définissons les sous-classes NeuronTR et LinkTR, qui héritent respectivement des classes Neuron et Link, mais avec un attribut supplémentaire pour stocker les informations supplémentaires.
Les nouvelles classes sont définies comme suit :
click to edit
class LinkTR | w+1 : Float .
subclass LinkTR < Link .
class NeuronTR | dt : Float .
subclass NeuronTR < Neuron .
Il est important de noter que les règles d'évaluation du réseau s'appliquent également à ces nouveaux objets ; les nouveaux attributs sont simplement ignorés. La prochaine étape consiste à calculer les termes d'erreur avant d'ajuster les poids. Le calcul de ces δj dépend de la couche sur laquelle nous travaillons, qu'il s'agisse de la couche de sortie ou des couches cachées.
click to edit
Pour la couche de sortie, la règle correspondante est assez simple
rl [delta2] : outputPattern(N, I, D, 1)
< neuron(2, I) : NeuronTR | x : X , dt : DT , st : 2 >
=> < neuron(2, I) : NeuronTR | x : X ,
dt : (X ((-(1.0, X)) (-(D, X))) ) , st : 3 > .
Cette règle indique que si nous avons un motif de sortie avec le numéro N, l'indice I et la valeur D, et que nous avons un objet NeuronTR correspondant dans la couche de sortie avec une valeur d'activation X, un terme d'erreur DT et un état de déclenchement 2, alors nous mettons à jour le terme d'erreur DT en utilisant la formule spécifique à la couche de sortie.
Cette règle de calcul des termes d'erreur est essentielle pour la rétropropagation, qui est utilisée pour ajuster les poids du réseau lors de l'apprentissage.
Le cas des autres couches est un peu plus complexe et est divisé en trois phases : la règle delta1A initialise dt à zéro, delta1B s'occupe de calculer la somme des poids multipliés par le terme d'erreur correspondant, et delta1C calcule le produit final. Encore une fois, dans toutes ces règles, l'attribut d'état st est mis à jour en conséquence.
La règle delta1B :
click to edit
rl [delta1B] : < neuron(1, J) : Neuron | dt : DT1, st : 2 >
< link(2, J, K):Link | w:W, st:2 > < neuron(2, K):Neuron | dt:DT2, st:2 >
=> < neuron(1, J) : Neuron | dt : (DT1 + (DT2 * W)), st : 2 >
< link(2, J, K):Link | w:W, st:3 > < neuron(2, K):Neuron | dt:DT2, st:2 > .
Cette règle indique que si nous avons un neurone dans une couche cachée avec l'indice J et le terme d'erreur DT1, et que nous avons un lien correspondant reliant ce neurone à un neurone de la couche de sortie avec le poids W et le terme d'erreur DT2, alors nous mettons à jour le terme d'erreur DT1 en ajoutant la multiplication du terme d'erreur DT2 par le poids W.
La règle link1 :
click to edit
rl [link1] : < neuron(0, I) : Neuron | x : X1, st : 1 >
< link(1, I, J) : Link | w : W, w+1 : W1, st : 1 >
< neuron(1, J) : Neuron | dt : DT, st : 3 >
=> < neuron(0, I) : Neuron | x : X1, st : 1 >
< link(1, I, J) : Link | w : W, w+1 : (W + (eta (DT X1))), st : 3 >
< neuron(1, J) : Neuron | dt : DT, st : 3 > .
Cette règle indique que si nous avons un neurone dans la couche d'entrée avec l'indice I, la valeur d'activation X1 et l'état de déclenchement 1, et que nous avons un lien correspondant reliant ce neurone à un neurone dans une couche cachée avec le poids W, le poids ajusté W1 et le terme d'erreur DT, alors nous mettons à jour le poids en remplaçant W par (W + (eta (DT X1))), où eta est un facteur d'apprentissage.
click to edit
4.2 Running the perceptron: evaluation and training
L'exécution du perceptron se divise en deux parties : l'évaluation et l'entraînement.
Pour contrôler l'ordre d'application des règles dans la spécification et simuler l'évaluation des motifs, nous utilisons des stratégies.
La stratégie principale "feedForwardStrat"
prend un nombre naturel en argument et l'applique à une configuration (c'est-à-dire un perceptron). Elle choisit une couche L' et applique la règle "feedForward" de manière aléatoire et aussi longtemps qu'elle est activée, afin de calculer la somme pondérée des valeurs associées à chaque neurone de la couche. Une fois que toutes les sommes ont été calculées, elle applique la fonction sigmoïde à chacune d'entre elles en utilisant la règle "sygmoid", encore une fois de manière aléatoire et aussi longtemps qu'elle est activée.
strat feedForwardStrat : Nat @ Configuration .
sd feedForwardStrat(L’) := one(feedForward[L<-L’])!; one(sygmoid[L<-s L’])!.
Il existe également deux stratégies auxiliaires
La stratégie "inputPatternStrat"
. La stratégie "computeOutput"
s'occupe de rendre les motifs successifs disponibles et de réinitialiser les attributs appropriés des neurones et des liens.
est utilisée pour calculer l'erreur une fois qu'un motif a été évalué.
Régles
strat inputPatternStrat : @ Configuration .
sd inputPatternStrat :=
one(resetNeuron) ! ; one(resetLink) ! ; one(nextPattern) .
strat computeOutput : @ Configuration .
sd computeOutput := one(computeError) ! ; setNet .
Ces stratégies permettent de contrôler l'ordre d'application des règles lors de l'évaluation et de l'entraînement du perceptron. En ajustant les paramètres des stratégies, pour définir le comportement spécifique de modèle de perceptron.
La stratégie d'évaluation "evaluateANN"
combine toutes les stratégies précédentes pour évaluer un motif. Elle insère le prochain motif, calcule les valeurs des neurones dans les couches cachées et de sortie, puis retourne l'erreur.
Code
strat evaluateANN : @ Configuration .
sd evaluateANN := inputPatternStrat ; feedForwardStrat(0) ;
feedForwardStrat(1) ; computeOutput .
Pour forcer l'évaluation des M premiers motifs par le perceptron multicouche, vous pouvez exécuter la commande suivante :
(srew ann netStatus(0, 0, 0, M) using one(evaluateANN) ! .)
Dans cette commande, les motifs d'entrée appropriés doivent avoir été définis et "ann" doit être une expression de la forme :
Code
neuronGeneration(0, input0, threshold0, 0)
neuronGeneration(1, input1, threshold1, 0)
linkGeneration(1, link1, 0, 0)
neuronGeneration(2, input2, threshold2, 0)
linkGeneration(2, link2, 0, 0)
De manière similaire à l'évaluation, nous devons définir une stratégie appropriée pour l'entraînement du perceptron. Une fois que la sortie associée à un motif a été calculée, nous devons ensuite calculer les termes d'erreur, les utiliser pour obtenir les poids ajustés, et les transférer à l'attribut approprié. Cela peut être facilement réalisé en appliquant les règles définies dans la section précédente dans le bon ordre.
Code
strat backpropagateANN : @ Configuration .
sd backpropagateANN := one(delta2) ! ; one(link2) ! ;
one(delta1A) ! ; one(delta1B) ! ; one(delta1C) ! ; one(link1) ! ;
one(switchLink) ! .
Enfin, l'entraînement d'un réseau consiste à évaluer un motif avec la stratégie "evaluateANN", puis à ajuster les poids en conséquence avec la stratégie "backpropagateANN".
strat stratANN : @ Configuration .
sd stratANN := evaluateANN ; backpropagateANN .
Ainsi, en utilisant la stratégie "stratANN", vous pouvez effectuer l'évaluation et l'entraînement du perceptron multicouche.
5 Example: Diagnosis of glaucoma
Dans le contexte du diagnostic du glaucome, un système utilisant des réseaux neuronaux a été proposé pour intégrer l'analyse des fibres nerveuses de la rétine à partir de l'étude de la polarimétrie laser à balayage (NFAII;GDx), de la périmétrie et des données cliniques. Dans ce travail, le perceptron multicouche résultant a été développé à l'aide de MatLab.
Les auteurs ont utilisé les données de ce projet comme base de test pour spécifier l'algorithme de rétropropagation dans Maude. Les résultats obtenus étaient équivalents à ceux de l'implémentation MatLab, avec un taux de réussite de 100%. Cependant, le temps d'exécution de leur implémentation en Maude était nettement plus lent, ce qui les a incités à optimiser leur code.
Pour optimiser le code, ils ont simplifié autant que possible les règles en exploitant l'exécution d'équations de Maude, qui est plus rapide que l'exécution de règles et évite les branchements. Ils illustrent cette technique d'optimisation avec la règle "feedForward". Dans la version optimisée, la règle est simplifiée en une équation :
Code
rl [feedForward] : C => feedForward(C) .
op feedForward : Configuration -> Configuration .
eq feedForward(C < neuron(L, I) : Neuron | x : X1, st : 1 >
< link(s L, I, J) : Link | w : W, st : 0 >
< neuron(s L, J) : Neuron | x : X2, st : 0 >)
= feedForward(C < neuron(L, I) : Neuron | >
< link(s L, I, J) : Link | w : W, st : 1 >
< neuron(s L, J) : Neuron | x : (X2 + (X1 * W)) >) .
eq feedForward(C) = C [owise] .
Cette version optimisée de "feedForward" simplifie le calcul en mettant à jour directement la valeur de "x" dans le neurone en fonction de la somme pondérée des entrées.
Les stratégies d'évaluation et d'entraînement ont également été modifiées en conséquence, puisque le combinateur "!" n'était plus nécessaire. La spécification résultante est moins naturelle mais plus efficace en termes de temps d'exécution.