Porting other ITP proofs to Lean

Stream: Machine Learning for Theorem Proving

[Tung Tran]

Reposted from #new members

Hello everyone! I've been looking into autoformalization with natural language processing (NLP), and it seems the task has some promising tracks shown in Qingxiang Wang’s works but is generally not feasible yet. From what I’m getting, the main problem is the context holes, which are “easy to understand/derive" by readers.

So I think we could instead start with a simpler task, namely porting proofs from other ITPs, e.g. Isabelle, to Lean. This should be more feasible since contexts in ITPs are mostly explicit. We could think of the problem input as some Lean statement (manual input), and the statement’s proof to the goal but in Isabelle. The output will be the statement’s proof in Lean.

As in Jesse Han’s PACT paper, we saw the usefulness of GPTs in providing Lean proof. We can further integrate Isabelle proof embedding into such a network to increase the proof success rate, and hopefully, it will realistically help with porting. This should also be possible as GPT is known to work well even when integrated with image embeddings.

It might be a stretch, but if this works well enough, the network can be the exploration guidance module in Szegedy’s A Promising Path Towards Autoformalization and General Artificial Intelligence.

So what do you think about the idea? I'm still new to everything, so please do correct me if I said something wrong.

[Kunhao Zheng]

(deleted)

[Jason Rute]

@Tung Tran I've been meaning to respond to your post for a while. I think you are exploring the right ideas, but there are also a lot of "devil in the details" issues. What you propose is a sort of ITP translation which is a well researched topic, but also a difficult area.

[Jason Rute]

One way to translate from one ITP A to another B is to (1) align the logics (by starting with an ITP A with a weaker logic than B, or by adding axioms to B to make it stronger than A), (2) get the kernel level proofs from ITP A, and (3) automatically translate them into proofs of ITP B. For example, @Mario Carneiro translated all of MetaMath's set.mm into Lean. (#general > Prime number theorem in lean) The catch (and this is huge!) is that the translation is a mess:

1. The resulting Lean proofs are computer generated and don't look anything like idiomatic Lean.
2. Every Metamath definition is duplicated. For example, there are now two definitions of natural numbers, the translated MM definition and the Lean definition.
3. There is no obvious way to check which definitions align, and proving they align is labor intensive and subtle. (You can show that the MM definitions for natural number and Lean satisfy the same uniqueness property, namely they are initial. This doesn't show they are equal, since in Lean, isomorphic types are rarely provably equal, but it does allow you to carefully transfer a set.mm theorem about the MM natural numbers and it's operations, to a theorem just using the Lean the natural numbers and it's operations. For example, Mario did this with Dirichlet's theorem, giving a verified version in pure Lean---albiet with an ugly auto-translated MM proof.)
4. Many definitions only partially align. For example, it is possible different definitions of subtraction handle dividing by 0 differently. Different definitions of limit might use very different notation and parameters. (Lean's limits use filters.) Groups are handled very differently in various ITPs. This makes aligning even more challenging, and prevents say putting MM's Prime Number Theorem into a statement of pure Lean.

[Jason Rute]

What about on the black-box ML side of things, like you propose? Just throwing Isabelle training data into GPT-f would likely help GPT-f's ability to construct Lean theorems, but of course it is good to test this (and it brings up a bunch of questions about if such a system is auto-translating or just learning better representations through more similar data). A more targeted strategy like you propose would also be interesting, and I encourage you too look at Unsupervised Translation of Programming Languages which uses unsupervised translation methods to translate C++ to Python and Python to C++. It creates pretty good, idiomatic translations of simple functions. But note it doesn't create translations of projects. In particular, the functions are all "self contained" in that they only refer to other standard library functions in C++ and Python. However, in ITPs, it is likely if one is trying to translate a theorem A in Isabelle, then A also probably depends on other lemmas and definitions which need to be translated. Definitions are (for all the same reasons in auto-translation) very difficult to translate idiomatically since concepts don't perfectly align. Also, it isn't necessarily clear when a lemma or definition needs to be translated verse it already existing in some form in the library.

[Jason Rute]

Of course, these challenges are just that: challenges. Hopefully, well designed ML systems can come along and help solve them. I've been saying for a while (and you can find my musings here on Zulip) that this task is one ripe for ML to help solve.

[Jason Rute]

Also see: https://www.sciencedirect.com/science/article/pii/S0747717118300348