Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.neural-vf

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/neural_vf.clj1 definitions, 3 theorems

AHoF D30 Neural Network Value Function: approximate the value function with a trainable neural network. The forward pass of a single linear-layer neuron (pre-activation) is the weighted sum of its inputs plus a bias: neuron w1 x1 w2 x2 b = w1*x1 + w2*x2 + b over exact nonnegative rationals (two inputs; the general neuron folds the weighted sum over all inputs). Proved native and axiom-free: the neuron pre-activation, and the guarantee that the pre-activation is at least the bias (b <= neuron) when the weighted inputs are nonnegative, so a nonnegative-weight layer never falls below its bias floor. The nonlinear activation (ReLU / tanh), the multi-layer composition, and gradient-descent training are executable concerns; the weights and bias are supplied rationals. What is proved here is the deterministic linear pre-activation. Requires nnrat/add, nnrat/multiply, nnrat/at-most, and the decidable nnrat order (all in the D63 checkpoint). Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.neural-vf` prints this classification.

neural-vf/neuron :
  (x₁ x₂ x₃ x₄ x₅ : ℚ≥0)
  → ℚ≥0

neural-vf/neuron-unfold :
  (w1 x1 w2 x2 b : ℚ≥0)
  → neural-vf/neuron w1 x1 w2 x2 b = w1 · x1 + w2 · x2 + b

neural-vf/neuron-example :
  → neural-vf/neuron 2 3 1 4 5 = 15

neural-vf/neuron-above-bias :
  → 5 ≤ neural-vf/neuron 2 3 1 4 5