[Agda] Agda and machine learning

[Warrick Macmillan]

Dear All,

I'm currently writing my Msc thesis on the topic of natural language <->
formal proof translation, using GF, and have been highly intrigued by the
dichotomy of a rule-based formalization approach as opposed to the
so-called Autoformalization scheme recently outlined by Szegedy [1].

Szegedy contends "that  in  the  coming  years  we  will  see  automated
systems to rival humans in general reasoning and the fastest path to
achieve this is by creating automated mathematical reasoning systems via
autoformalization."

He then poses the question : "Will we ever arrive at the point where an AI
agent can learn to do reasoning as well as the best humans in the world in
most established domains of mathematics?"

I see interpretations of this perspective varying from extreme optimism - a
new, reformulated Entscheidungsproblem whereby some "mechanical AI agent"
can decide the existence of a proof better than a human, and perhaps even a
priori formulate what to prove - to a highly cynical view that this is just
wishful thinking from another silicon valley technocrat.

I've heard, for instance, that Voevodsky wasn't very enthusiastic about
automated proving in gereral.  Thomas Hales says of Szegedy's group :
"Their ambitions are inspiring, the resources and research methodologies at
Google are grandiose, but I would not personally bet on their time
frame."[2]

As far as I'm aware, much of the (still) early work using machine learning
in proof search targets either satisfiability problems, which is somewhat
outside the interests of most type theorists[3],  or tactic-based languages
like HOL and Coq [4] where the learning of a proof isn't at the level of
constructing a term that could then be presented in a human legible format,
and large, fairly standard libraries already exist.

My appreciation of Agda is stays true to Martin-Löf's original vision of a
programming language in which one can write proofs.  I bring this up here
because it seems that using machine learning to produce Agda code doesn't
yet seem compatible with Szegedy's proposal - especiallty since it doesn't
yet have tactics.  Other writing in [1] dicuss various other aspects of
this space, yet Agda is hardly mentioned.

How do you see the upcoming role of machine learning in theorem proving,
formalization, and interactive proof development, with particular reference
to Agda?

Warrick


[1] A Promising Path Towards Autoformalization and General AI,
https://link.springer.com/chapter/10.1007/978-3-030-53518-6_1
[2] AN ARGUMENT FOR CONTROLLED NATURALLANGUAGES IN MATHEMATICS
https://jiggerwit.files.wordpress.com/2019/06/header.pdf
[3] Neural networks and the satisfiability problem
https://searchworks.stanford.edu/view/13250178
[4] HOList: AnEnvironment forMachineLearning ofHigher-OrderTheoremProving
https://arxiv.org/pdf/1904.03241.pdf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200923/4375a6b7/attachment.html>