1.1 A neural network model in acl2  (Page 3/8)

Besides modeling the structure of neural networks, we also model their input-output behavior. A valid input vector is a list of rational numbers, and is identified by the isListOfWeights function, so called because it is also a helper function for isNeuron. Like neurons, input vectors are lists of rational numbers. A single neuron functions by outputting the sum of products of each input value with the corresponding weight on the synapse it is transmitted through. The behavior is handled by forwardNeuron, which takes an input vector and neuron as input, and returns the weighted sum as output.

The value outputted from each individual neuron is then passed through an activation function, which is normally defined as any real-valued function. Once again, use of ACL2 restricts us to rational numbers. Although it is not a requirement, activation functions also commonly have a restricted range, usually [0,1] or [-1,1]. The three activation functions modeled herein share the range [-1,1]: threshold, piecewise, and rational sigmoid approximation.

The rationalsigmoid function was used because ACL2 does not support irrational numbers, and therefore does not support the more common full sigmoid function: (exp(x) - 1)/(exp(x) + 1) . The function presented here is a rational valued approximation of the sigmoid function using 2-2 Pade approximation (Boskovic 1997). This activation function does not meet the requirements of the basic universal approximation theorem, but additional work has shown that rational functions such as the one above do in fact satisfy the universal approximation property (Kainen 1994). Neither the threshold function nor piecewise function fulfill the universal approximation requirements, but are none-the-less common.

The activate function models the behavior of activation functions by applying forwardNeuron to the input vector and neuron, and then applying the appropriate activation function specified by a quoted symbol to the result. The activate function is used by the forwardLayer function, which models signal propagation through layers, and this function is in turn used by forwardNetwork, which models signal propagation through networks.

Structural swapping

One of the main focuses of this paper is to provide proofs of the effects that several simple structural transformations have on neural networks. Many functions are defined to perform these transformations, and one of the most widely used is swap. The swap function takes a list and two indices in the list, and returns a list with the values at those two positions swapped. To assure the correctness of swap, several theorems are proven about it: