The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Here's the video of Joe and I playing around with Copilot (Github tool built on top of Codex, a code large language model that treats all code as text, and is agnostic to the particular language) inside of CompCert. I've gotten confirmation that CompCert is not in the training data. It's really fun. Check it out: https://youtu.be/jFL-ftywPiM

On the rest of the discussion, I think it's normal for folks to get defensive about the techniques behind our automation because it's our life and so on. I also think it's healthy to be skeptical, but open-minded. Being skeptical also means being skeptical of community norms from ML that are harmful and might make their way into our field more in the future by way of more cross-pollination, and that includes industrial secrecy, which I'm extremely critical of.

But I also know being too closed-minded and not paying attention to what's happening in industry will be a bad move for researchers in this area in the near future. I'd rather participate and try to get our community's values and insights represented as much as possible.

Also, no direct responses to your points, Josef, but I value your perspective here.

Talia

On Tue, Aug 24, 2021, 4:28 PM Josef Urban <josef.urban AT gmail.com> wrote:

My 5 cents:

1. Learning-guided proof search is not "mishmashing previous proofs". Good learning is about generalization, not memorization. And there are methods (and even whole fields) combining statistical/symbolic learning with semantics. 

2. Even relatively standard statistical ML combined with search can go from a few/short proofs to many/long proofs [1,2,3] (good luck with unguided ATPs/SMTs on the harder problems). Such reinforcement learning setups have already produced superhuman systems like AlphaGo/Zero.

3. TP/math is a fairly unique and interesting domain where more algorithmic and semantic learning should eventually show its merits over memorizing and purely statistical architectures. Already a symbol-independent GNN [4] (learning from structure only) beats (symbol/sequence-based) language models (transformers, RNNs) on some of our tasks. Especially if you are not allowing tricks such as "pretraining" on the whole internet/github - most likely containing something fairly similar to your test data.  

4. Tomas Mikolov who largely started the modern LM era does not think much of OpenAI's touting of GPT as the coming of AI. I think LM is a useful tool for some TP jobs and we need to explore it. I don't regret we started that [5,6], but the overclaims made about LM-for-TP by some people in the last year are over the top. I likely prevented quite some nonsense from being published in Quanta a year ago [7]. A GPT-based tool improving on TacticToe, Tactician or Enigma (or really just unguided Vampire) in a fair evaluation would be a good start.

5. The BigScience project [8] has been recently launched to train large ML models in open and transparent ways. It is a reaction to the number of issues that the AI company research has brought upon us. Jelle Piepenbrock and Bartosz Piotrowski have started a TP-oriented group within BigScience and everybody who wants to contribute is welcome. I also hope that the formal/reasoning community will demonstrate its unique reasoning/judgement capabilities and apply scientific rigor when dealing with these topics.

Josef

[1]: https://proceedings.neurips.cc/paper/2018/hash/55acf8539596d25624059980986aaa78-Abstract.html

[2]: https://doi.org/10.4230/LIPIcs.ITP.2019.34

[3]: https://github.com/ai4reason/ATP_Proofs/blob/master/75percent_announce.md

[4]: https://doi.org/10.3233/FAIA200244

[5]: https://doi.org/10.1007/978-3-030-53518-6_24

[6]: https://doi.org/10.29007/j5hd

[7]: https://sympa.inria.fr/sympa/arc/coq-club/2020-09/msg00017.html

[8]: https://venturebeat.com/2021/07/14/nlp-needs-to-be-open-500-researchers-are-trying-to-make-it-happen/

On Tue, Aug 24, 2021 at 4:13 PM Stefan Monnier <monnier AT iro.umontreal.ca> wrote:

> I think it's worth noting that OpenAI (the company that made Codex, the
> model behind Copilot) has an ongoing project on neural proof synthesis for
> Lean.  I think we will see some use of this in the near future.  For that
> week, I'm likely to invite someone at OpenAI to give a talk and demo the
> model if he's allowed. (Coq will get left behind from that effort, by the
> way, if nobody adds Coq proofs for their cross-language benchmarks; if
> interested in that effort, let me know.)

FWIW, as a professor, I'd feel ... awkward inviting presentations about
tools that include a sufficiently large amount of secret/proprietary
elements that one can't just go and reproduce it on your own.
It seems philosophically opposed to ideas such as "open access".


        Stefan