Would it be possible to involve a proof assistant in the process of training a LLM?

Question

LLMs like GPT-3 have been shown capable of outputting highly complex code. Sadly, actually using them to replace a programmer's job has two major caveats:

1. LLMs are notoriously bad at producing complex algorithms

2. It isn't possible to check whether the outputted code is correct

As such, while something like ChatGPT will easily translate between different syntaxes, and even produce useful code, that is limited, to an extent, to code it has already seen. Fortunately, the (2) problem already has a solution: a proof checker. Certain languages have these built in, including Lean, Coq, Agda, Idris and Kind. As an example, suppose you wrote the following prompt, asking for an algorithm in Agda:

Complete the following Agda function, which negates a boolean:

not : Bool -> Bool

A LLM could fill it incorrectly, as follows:

not : Bool -> Bool
not true  = true
not false = false

But the cool thing is, in a proof assistant, you're able to enrich the type arbitrarily, and turn it into a complete specification of the program you desire. As such, you could prevent the issue above as follows:

Complete the following Agda function:

not : (in : Bool) -> Sigma (out : Bool) (in != out)

This type demands that the implementation of not comes accompanied by a proof that the output is, indeed, different from the input. Suppose that we did that, and the Ai still produced an incorrect algorithm:

not : (in : Bool) -> Sigma Bool (λout -> in != out)
not true  = MkSigma true  <proof_here>
not false = MkSigma false <proof_here>

In that case, it wouldn't be able to fill the <proof_here> with a valid proof that the algorithm is correct, because it isn't. As such, we would be able to easily discard that answer, feed the AI an error message, and ask it to try again. We can repeat this process until it gets it right. Of course, this is a simple example, but you could make arbitrarily complex algorithm demands using the same technique. For example, the prompt below would demand a correct sorting algorithm:

Complete the following Agda function:

sort : (in : List Nat) -> Sigma (List Nat) (λ out -> IsSorted out & IsSame in out)

Once again, chances are it would produce the wrong solution, but we'd be able to automatically discard it and try again, until it gets it right. This leaves us with only the problem (1): LLMs are notoriously bad at coding. That is, even if we're able to discard the wrong output, something like current-version ChatGPT will probably never get anything sufficiently complex correct.

Now, that's not unsurprising: GPT wasn't trained to write proofs. As such, a natural solution would be to do so. But the amount of proofs written is very limited, compared to, say, the size of Wikipedia. We don't have enough data. But the cool thing is: we can actually make the AI itself generate the proofs it is trained on. It would work as follows:

1. Train the AI on publicly available proofs (Agda/Coq std-libs, for example)

2. Generate a random theorem and ask it to prove

3. If it gets the proof wrong, go back to 2

4. If it gets the proof right, train it on that proof, and go back to 1

By repeating this loop ad infinitum, we'd have both a growing body of proofs, and an AI that is increasingly more capable of proving complex theorems.

My questions are: is there substance to this approach? If so, has anyone tried it? Citations would be appreciated. If not, is there any clear reason I'm not aware of?

Answer 1

Your post has links with:

• An article by Stephen Wolfram [ https://writings.stephenwolfram.com/2023/01/wolframalpha-as-the-way-to-bring-computational-knowledge-superpowers-to-chatgpt/ ], stating that LLMs are not meant to manipulate symbolic knowledge, but could possibly interact with tools that do so like Wolfram|Alpha. This relates to your idea of interacting with proof assistants.
• A recent arXiv paper whose authors propose "Guiding Formal Theorem Provers with Informal Proofs" [ https://arxiv.org/abs/2210.12283 ]. This seems a necessary step for the approach you propose, but their results are not perfect yet.

Also, your idea has ties with various algorithms that combine learning and search (cf. AlphaZero, Self-improving theorem provers, ...[ https://duvenaud.github.io/learning-to-search/ ]). But then, should both the LLM and the proof assistant learn ?

I would be already happy with easier-to-use proof assistants, but doing maths is about both reasoning (as in proof assistants) and learning, so your approach is appealing.