Towards abductivefunctional programming

Koko Muroya
Steven Cheung & Dan R. Ghica(University of Birmingham)
ML Family workshop (Oxford),
7 Sep.
2017
Muroya(U. B’ham.)Parameter tuning via
targeted abduction

Koko Muroya
Steven Cheung & Dan R. Ghica(University of Birmingham)
ML Family workshop (Oxford),
7 Sep.
2017
Muroya(U. B’ham.)A programming idiom for optimisation & ML
model

input

datause
model

train
model

outputupdated model3

Muroya (U. B’ham.)Example: parameter optimisation in TensorFlow
model# Build inference graph.
# Create and initialise variables W and b.
W = tf.Variable(...)
b = tf.Variable(...)
y = W * x_data + b #NOTE: Nothing actually computed here!

https://www.tensorflow.org/
https://github.com/sherrym/tf-tutorial
4

Muroya (U. B’ham.)Example: parameter optimisation in TensorFlow
model
W = tf.Variable(...)
b = tf.Variable(...)
y = W * x_data + b

input

use
modeloutput# Create a session.
sess = tf.Session()sess.run(init)
y_initial_values = sess.run(y)# Compute some y values

5

Muroya (U. B’ham.)Example: parameter optimisation in TensorFlow

W = tf.Variable(...
b = tf.Variable(...
y = W * x_data + b

model# Build training graph.
dataloss = tf.some_loss_function(y, y_data)# Create an operation that calculates loss.
tf.train.some_optimiser.minimize(loss)# Create an operation that minimizes loss.
init = tf.initialize_all_variables()train# Create an operation initializes variables.

model

sess = tf.Session()sess.run(init)# Perform training:for step in range(201):
sess.run(train)

updated model

6

Muroya (U. B’ham.)TensorFlow● shallow embedded DSL○ lack of integration with host language○ cannot use libraries in graphs○ difficult to debug / type graphs● imperative “variable” update

7

Muroya (U. B’ham.)TensorFlow● shallow embedded DSL○ lack of integration with host language○ cannot use libraries in graphs○ difficult to debug / type graphs● imperative parameter (“variable”) update

Proper functional language?
● simple & uniform programming language○ full integration with base language○ typed in ML-style○ well-defined operational semantics● funcional parameter update
8

Muroya (U. B’ham.)Key idea:Abductive reasoning

9

Muroya (U. B’ham.)Abductive inference: background● logical inferenceA○ deduction (specialisation)○ induction (generalisation)○ abduction (explanation)

A⇒B
B● previous applications○ abductive logic programming○ program verification (http://fbinfer.com/)10

Muroya (U. B’ham.)Abductive inference: background● logical inferenceA○ deduction (specialisation)○ induction (generalisation)○ abduction (explanation)

A⇒BB● previous applications○ abductive logic programming○ program verification (http://fbinfer.com/)11

Muroya (U. B’ham.)Abductive inference: background● logical inferenceA○ deduction (specialisation)○ induction (generalisation)○ abduction (explanation)

A⇒BB● previous applications○ abductive logic programming○ program verification (http://fbinfer.com/)12

Muroya (U. B’ham.)Abductive inference: our use● possible deductive rule for abduction“abduct” explanation P of A

in “targeted”
way

13

Muroya (U. B’ham.)“Parameter tuning via targeted abduction”
model
let m x = {2} * x + {3};;

use

train

outputupdated modelm 0;;

let f @ p = m inlet q = optimise p inf q;;

14

Muroya (U. B’ham.)“Parameter tuning via targeted abduction”
model
let m x = {2} * x + {3};;provisional constants(“targets”)

cf. definitive constants
0,1,2,...

15

Muroya (U. B’ham.)Parameter tuning via targeted abduction
model
let m x = {2} * x + {3};;useprovisional
constantsoutputm 0;;(* simply function application *)16

Muroya (U. B’ham.)“Parameter tuning via targeted abduction”
model
let m x = {2} * x + {3};;provisional
constants

train

abductivedecoupling

updated model

let f @ p = m in(* “decouple” model f and parameters p *)let q = optimise p in (* compute “better” parameter values *)Let m’ = f q in(* “improve” model using new parameters *)...

17

Muroya (U. B’ham.)Abductive decoupling: informal semantics
let m x = {2} * x + {3};;let f @ p = m inlet q = optimise p inf q;;

model with
provisional constants

val m = fun x -> {2} * x + {3}----------------------------------------------------------------val f = fun (p1,p2) -> fun x -> p1 * x + p2 parameterised model

parameter vector

val p = (2,3)

18

Muroya (U. B’ham.)Abductive decoupling: informal semantics
let m x = {2} * x + {3};;let f @ p = m inlet q = optimise p inf q;;model with
provisional constants

val m = fun x -> {2} * x + {3}----------------------------------------------------------------val f = fun (p1,p2) -> fun x -> p1 * x + p2 parameterised model

parameter vector

val p = (2,3)

abduction rule
19

Muroya (U. B’ham.)

Promoting provisional to definitive constants
let m x = {2} * x + {3};;let f @ p = m inlet q = p inf q;;model with
provisional constants

val m = fun x -> {2} * x + {3}----------------------------------------------------------------val f = fun (p1,p2) -> fun x -> p1 * x + p2 parameterised modelval p = (2,3)
parameter vector-----------------------------------------------------------------(trivially updated)parameter vector
result: model withdefinitive constants

val q = (2,3)- = fun x -> 2 * x + 320

Muroya (U. B’ham.)Parameter tuning via targeted abduction
model
let m x = {2} * x + {3};;useprovisional
constantstrain

outputupdated modelm 0;;

let f @ p = m inlet q = optimise p in
f q;;

abductive
decoupling
21

Muroya (U. B’ham.)Targeted abduction: syntax & types(fixed) field

opaque vector space,
representing

provisional
constant

abduction

let f@x = u in t

22

≡ (abd f@x -> t) u

Muroya (U. B’ham.)Targeted abduction: syntax & types(fixed) fieldprovisional
constant

opaque vector space,
representingabduction(* abduction of open terms *)let m x = {2} * x + n inlet f @ p = m in...

23

Muroya (U. B’ham.)Targeted abduction: opaque vectors● size determined dynamically● order of coordinates unknown○ … yet we want deterministic programs○ always point-free (no access to bases/coordinates)○ only symmetric operations (invariant over permutationof bases/coordinates)● possible in theory○ symmetric tensors● reasonable in practice○ not all, but most, optimisation algorithms
are symmetric24

Muroya (U. B’ham.)Targeted abduction: symmetric vector operations
standard vector operations

iterated vector operations

25

Muroya (U. B’ham.)Targeted abduction: example use
numerical gradient descentlet m x = {2} * x + {3};;let f @ p = m inlet q = grad_desc f p loss 0.001 in
f q;;(* least square on some reference data *)let loss f p = ...;;

folding over standard basis(* numerical gradient descent *)let grad_desc f p loss rate =let d = 0.001 in
let g e =let old = loss f p inlet new = loss f (p ⊞ (d ⊠ e)) in(((old - new) / d) * rate) ⊠ e ing |⊞ p;;
26

Muroya (U. B’ham.)Targeted abduction: syntax & types
only symmetric
operations
on vectors
opaque vector space,(fixed) field

representing

provisional
constantabduction

let f@x = u in t

27

≡ (abd f@x -> t) u

Muroya (U. B’ham.)Targeted abduction: operational semantics● provisional constants are linear!
let m x = {0} * x + {0};;vslet p = {0} in
let m x = p * x + p;;● graph rewriting semantics
○○
○
○
○
○

… based on Geometry of Interaction
http://www.cs.bham.ac.uk/~drg/goa/visualiser/
determinism
soundness of execution
safety of garbage-collection
call-by-value evaluation
28

Muroya (U. B’ham.)Conclusions● a fully-integrated language for parameter tuning○ abductive decoupling “abd”○ simply-typed + abduction rule
○ formal operational semantics
http://www.cs.bham.ac.uk/~drg/goa/visualiser/■ call-by-value■ determinism■ sound execution & safe garbage-collection● open problems○ actual ML compiler extension■ abduction is dynamic & complex■ … but not computationally dominant○ stochastical machinary29

Muroya (U. B’ham.)