Formal Reasoning and Program Synthesis

 This is a discussion between Christian Szegedy of Google Research and the gang at Machine Learning Street Talk.  It covers a lot of ground. 

One area is whether we can use neural net systems to auto-formalize the methodology of practicing and utilizing mathematics.  Wolfram research is jumping up and down at this point, saying 'hey guys, we already did that' (the auto-formalize part).

Another area is discussion about Transformers and how they work.  Hot topic. Perhaps over-hyped in my humble opinion (ai lemmings running towards a transformer cliff), but that's for another post.

I'm not sure what i think about this notion of neural networks 'running programs'. Tim's comments at the very beginning about neural networks being systems that interpolate on a lower dimensional manifold get's to the exact heart of how they work.  If someone writes a program to implement a radial basis function interpolator, do we really care about the program, or just the function it is interpolating?  

But we all need to keep an open mind, and there are lot's of interesting things to learn listening to this discussion.

Certainly the notion that we have been programming computers essentially the dame way since the 1950's is pretty spot on. Please give us better ways to do this task.


1:  Another reason why we have a special holiday every year at HTC that celebrates Jurgen Schmidhuber and his various contributions to the field.

2: Ok, reasoning in latent embedded space. I need to think about that more.


Popular posts from this blog

Simulating the Universe with Machine Learning

CycleGAN: a GAN architecture for learning unpaired image to image transformations

Pix2Pix: a GAN architecture for image to image transformation