Welcome to #Machine learning and theorem proving reading group.

For the next reading group (Monday 12:00, FC22) we'll be discussing:

"Learning Heuristics for Automated Reasoning through Reinforcement Learning"

https://arxiv.org/pdf/1807.08058.pdf

Kind regards,

Reinforcement learning algorithms have shown to often find and exploit subtle implementation errors in the environment, instead of solving the intended problem. While testing and manual inspection of the results is a feasible approach for board games and Atari games, it is neither possible nor sufficient in large-scale formal reasoning - a solver run is simply too large to inspect manually and even tiny mistake can invalidate the result. In order to ensure correctness, we need an environment with the ability to produce formal proofs, and check the proofs by an independent tool.

Interesting!

@Yiannos @Angeliki Koutsoukou Argyraki

Yeah, claim without source though.

Please feel free to make paper suggestions for the reading group in this stream.

Fair enough.

For next time: "Understanding Deep Learning requires rethinking generalisation" by Zhang et al

https://arxiv.org/abs/1611.03530

@Lawrence Paulson @Angeliki Koutsoukou Argyraki @Yiannos

Not clear at all what can be learnt from this preprint wrt to interactive theorem proving.

@Anthony Bordg The paper might lean towards learning theory but I agree with Angeliki that it's useful in introducing the "internals" of deep learning. Do you have any papers you'd like the group to discuss?

The point of our weekly meetings is to discuss what we have done and where we are headed. Even where we have discussed machine learning papers, it's been in the context of our own ideas and plans as opposed to simply the paper itself. It's important to know what others have done when making our own plans.

The project tasks have three distinct threads of work: one connected with mathematics, one connected with machine learning and one connected with computer algebra and related algorithms. For a while our focus was almost entirely on mathematics. It may be that we have gone too far the other way, allowing machine learning to push aside the other goals. That's also wrong. Possibly the right approach is to set aside two meetings a month (the first and third say) for machine learning and the other two or three meetings for mathematics. And nobody should feel obliged to attend a meeting if they aren't interested in the topic being discussed at the time.

Last updated: Dec 07 2023 at 16:21 UTC