DSdselsam·Jul 11, 2017
> The specification is a lot smaller than the code, and so it's easier to read and manually verify that it's correct.
>> How is that the case in this specific example? It looks a lot harder to check for correctness.
Author here.
Here is the specification for the stochastic backpropagation algorithm:
https://github.com/dselsam/certigrad/blob/master/src/certigr...
The preconditions do not need to be inspected carefully because we prove that the models of interest satisfy them (example: https://github.com/dselsam/certigrad/blob/master/src/certigr...)
Here is the part of the specification that needs to be inspected carefully:
https://github.com/dselsam/certigrad/blob/master/src/certigr...
The syntax may seem strange to those unfamiliar with Lean, and a few of the functions involved may not be self-explanatory without reading their definitions
Read the rest
, but the statement is conceptually simple: the stochastic backpropagation algorithm correctly computes unbiased estimates of the gradient of the expected loss.
It is subjective, but I personally think that this specification is vastly easier to understand and to check for correctness than the actual implementation of the stochastic backpropagation algorithm.