Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: applied category theory

Topic: ML/ATP

(=_=) (Apr 05 2020 at 16:32):

So now that @Jules Hedges has asked the Twitter hivemind about machine learning (ML) applied to automated theorem proving (ATP), I thought I'd make a new topic in #applied category theory to discuss. @Bruno Gavranovic

Has anyone tried to make a machine learning architecture for theorem proving, where a "generator" deep neural network, trained on a dataset of existing human-written proofs, interacts with an existing symbolic proof checker (eg. the Coq kernel)?

- julesh (@_julesh_)

(=_=) (Apr 05 2020 at 16:34):

Guillermo pointed out this early paper by Christian Szegedy et co.

@_julesh_ I've seen many works on that vein. This is one of the earliest https://arxiv.org/abs/1606.04442

- Guillermo Valle (@guillefix)

(=_=) (Apr 05 2020 at 16:35):

Another paper by Szegedy et co in 2017 uses Mizar.

(=_=) (Apr 05 2020 at 16:38):

This paper (Proverbot9001) from UCSD uses Coq.

Reid Barton (Apr 05 2020 at 16:41):

On the Lean theorem prover Zulip instance we have a stream dedicated to this topic. I'm not sure what will happen if I post a link, but I'll try anyways:
https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning.20for.20Theorem.20Proving

(=_=) (Apr 05 2020 at 16:43):

Reid Barton said:

On the Lean theorem prover Zulip instance we have a stream dedicated to this topic. I'm not sure what will happen if I post a link, but I'll try anyways:
https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning.20for.20Theorem.20Proving

Thanks! Looks like I'd have to get on board then.

(=_=) (Apr 05 2020 at 16:55):

This topic in that stream is good: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning.20for.20Theorem.20Proving/topic/Paper.3A.20Tactic.20Learning.20and.20Proving.20for.20the.20Coq.20Proof.20Assista

(=_=) (Apr 05 2020 at 16:57):

So there are now three ML bots for Coq:

• Proverbot9001 (which I linked to above)
• CoqGym/ASTactic
• TacticToe for Coq (this doesn't actually use neural networks, but k-nearest neighbour)

(=_=) (Apr 05 2020 at 17:02):

I guess it might be interesting to see what we can learn by using CT to study those machine learning architectures.