The Coq mailing list

[Josef Urban <josef.urban AT gmail.com>]

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