dreamcoder

Stream: general

[mikey liu]

hi i've been playing with ATPs for a bit and just saw this paper called dreamcoder. it learns concepts by itself and is able to perform certain nontrivial tasks with just a few examples (sorting, painting specific images, etc.) it is also able to grow on its own so to speak by a process called dreaming, which i think is kinda like a more sophisticated 'exploratory play' in reinforcement learning. i felt like this might work very well with lean and other ATPs in general to further automate theorem proving. here's the link to the paper: https://arxiv.org/abs/2006.08381 and here's its github link (if you wanna install it search for 'singularity 2.5' and install that also): https://github.com/ellisk42/ec

[Jason Rute]

I’ve been meaning for a long time to write up something on this. I agree this paper has a lot of potential (so much that I feel if I start talking about all my ideas related to it that I won’t be able to stop :smile:).

[Jason Rute]

If I write something up it will be on the #Machine Learning for Theorem Proving steam.

[Jason Rute]

Also this might be a coincidence but Yannic Kilcher just made a video on this paper yesterday: https://m.youtube.com/watch?v=qtu0aSTDE2I

[Jason Rute]

Also Kevin Ellis (the lead author) has a video: https://m.youtube.com/watch?v=NYIeP1hns6A&feature=youtu.be

[Jason Rute]

@mikey liu have you been able to run it? If so how long does it take to train?

[Notification Bot]

This topic was moved by Scott Morrison to #Machine Learning for Theorem Proving > dreamcoder