[Agda] Agda and machine learning

[mechvel at scico.botik.ru]

On 2020-09-23 19:35, Warrick Macmillan wrote:
> 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?"
> 

In the chess game this is done - with exception of a few number of 
positions which
are better solved by the human best players than by a program.
The result is clear: because grandmasters like to consult with a program 
when analyzing a
chess position. A chess program is really a great authority for them.
This is after 60 years of developing chess programs.

With mathematics it is different. Currently no mathematician would 
consult with a program:
"What is a way to prove the theorem T? To apply induction by n? Or to 
apply the method
of projections modulo the ideals I, J ... ?  Or to represent the thing 
as linear operators
and to apply the linear representation theory? Or to try to reduce T to 
the theorem of implicit
function? ...
".
Nothing of this sort happens - so far.
Currently, provers can only solve the problems like the following.

(1) A very simple problems. For example, to prove  reverse (reverse xs) 
== xs
     for a list xs,
     or to prove that _*_ in unary system for natural numbers is 
commutative
     (m * n == n * n).
     Not more complex than this.

(2) Concrete problems for which humans have designed a general algorithm 
for solution.
     For example, to solve a linear system (large systems are often 
difficult to solve).

The point (2) is similar to the fact that some machines can run 1 mile 
must faster than a human.

Example I.
Consider a program for _+_ for binary numbers in  Data.Nat.Bin
in the standard Agda library.
I do not think that any currently existing prover can prove 
associativity for this _+_:
"forall x y z ((x + y) + z == x + (y + z))".

The same is with

Example II. Prove that merge sorting is equivalent to sorting by 
insertion:
             forall xs (mergeSort xs == sortByInsertion xs).

There are millions of such simple problems.

I think, a powerful provers will be designed for algebra within about 20 
- 40 years,
the ones that will be able to solve problems more complex than (I) and 
(II).


> 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?

It is possible to write provers (tactics) as applied libraries for Agda.
For example, the unfailing Knuth-Bendix completion procedure.
A programmer will set in one's program a call for such a procedure 
instead
of inventing and placing in the program a lengthy proof for some 
equalities.

But it will be difficult to predict how expensive will be type-check for 
such program
(I expect so it is in the Coq system).

Regards,

------
Sergei