Lean for Neural Networks

Stream: lean4

[Mr Proof]

I have been working a lot with neural networks including using Pytorch, Tensorflow and Onnxruntime.

It strikes me that those languages essentially have their own implementation of dependent types. (Albeit a very basic one.) It also occurs to me that a language such as Lean would be an excellent language to express neural network models.

As an example, a neural network can basically be thought of as a function that takes one or more inputs of certain types (a number type plus a shape) and returns one or more outputs of certain types. What is more, that type of the output is dependent on the type of the input.

A typical example might have inputs of type float16[batch,channels,width,height], int64[batch, ids] and return some output e.g. float16[batch,f(width,height,ids)] where f is some function. Thus they are types with various parameters (shapes) which are named (incorrectly) as tensors types.

I have been playing around implementing my own type theory, and found it works quite well with importing multi-dimensional arrays, in this way. (I don't actually define what a float16 actually is, I just leave as an undefined object of type Type). One could indeed define a type such as int(n) where is it like a Fin but the values are between ±2^n and it also includes ±∞. It is less clear to me how one would mathematically define a float32 or float16 or whether they need to be defined at all.

As another example, if you consider the convolution operator for a neural network, the output type (shape) depends on the types (shapes) of the input tensor and the kernel size.

BTW the multi-dimensional arrays here are a lot different from tensors you find in math and physics which tend to have the same dimension on each index, rather these are rectangular arrays. Multidimensional arrays have lots of other uses, e.g. graphics, simulation, and lots of other things.

Well, all this say that this might be an interesting avenue to explore, and that multidimensional arrays (especially if GPU accelerated) would be an interesting use for the Lean language.

Thanks for listening:grinning_face_with_smiling_eyes:

Addendum: For back propagation, this is essentially just partial differentiation with the chain rule, which could also be automated in Lean.

[Jason Rute]

Yes, multidimensional arrays/tensors in neural networks are a great example of where dependent types would be helpful. See @Tomas Skrivan’s SciLean for a project which I think aims in this direction.

[Jason Rute]

I think Jax is interesting also since it also aims to be fully functional, so one day I could imagine something like a Jax interface in Lean, but maybe that is asking too much. :smile:

[Jason Rute]

And finally, you might also be interested in categorical deep learning which aims to combine category theory (and type theory) with deep learning theory (based on the success of geometric deep learning).

[Tyler Josephson ⚛️]

You may like this paper, which shared a similar vision:

http://proceedings.mlr.press/v70/selsam17a/selsam17a.pdf

[Tomas Skrivan]

Here I describe my attempt at neural networks in Lean https://lecopivo.github.io/scientific-computing-lean/working-with-arrays/tensor-operations.html unfortunately I have not managed to train it yet.

[Quinn]

@Alok Singh

[Alok Singh]

Quinn said:

Alok Singh

i’ve been streaming this at youtube.com/@therevaloksingh, like https://www.youtube.com/live/_efcMao8_50?si=Y9rYHbgfDB68yvbd

code at https://github.com/pimpale/llm.lean