Structure mlNeuralNetwork

signature mlNeuralNetwork =
sig

  include Abbrev

  type vect = real vector
  type mat = vect vector

  (* activation *)
  val idactiv : real -> real
  val didactiv : real -> real
  val tanh : real -> real
  val dtanh : real -> real

  (* neural network *)
  type layer = {a : real -> real, da : real -> real, w : mat}
  type nn = layer list
  type trainparam =
    {ncore: int, verbose: bool,
     learning_rate: real, batch_size: int, nepoch: int}
  val string_of_trainparam : trainparam -> string
  val trainparam_of_string : string -> trainparam
  type schedule = trainparam list
  val write_schedule : string -> schedule -> unit
  val read_schedule : string -> schedule

  type fpdata = {layer : layer, inv : vect, outv : vect, outnv : vect}
  type bpdata = {doutnv : vect, doutv : vect, dinv : vect, dw : mat}

  (* dimension *)
  val dimin_nn : nn -> int
  val dimout_nn : nn -> int

  (* weights randomly initialized *)
  val random_nn : (real -> real) * (real -> real) -> int list -> nn

  (* forward and backward pass *)
  val fp_nn : nn -> vect -> fpdata list
  val bp_nn : fpdata list -> vect -> bpdata list
  val bp_nn_doutnv : fpdata list -> vect -> bpdata list

  (* weight updates *)
  val update_nn : trainparam -> nn -> mat list -> nn
  val smult_dwl : real -> mat list -> mat list
  val sum_dwll : mat list list -> mat list
  val mean_square_error : vect -> real
  val average_loss : bpdata list list -> real

  (* input/output *)
  val enc_nn : nn -> HOLsexp_dtype.t
  val dec_nn : HOLsexp_dtype.t -> nn option
  val write_nn : string -> nn -> unit
  val read_nn : string -> nn
  val reall_to_string : real list -> string
  val string_to_reall : string -> real list
  val write_exl : string -> (real list * real list) list -> unit
  val read_exl : string -> (real list * real list) list

  (* interface *)
  val scale_real : real -> real
  val scale_out : real list -> vect
  val scale_ex : real list * real list -> vect * vect
  val descale_real : real -> real
  val descale_out : vect -> real list
  val infer_nn : nn -> real list -> real list
  val train_nn : trainparam -> nn -> (real list * real list) list -> nn


end

HOL 4, Kananaskis-14