From autoformalization to automated porting?

Stream: new members

[Tung Tran]

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.

[Johan Commelin]

Welcome! I don't know much about AI. But I'll just point out that there is an entire stream dedicated to #Machine Learning for Theorem Proving.

[Arthur Paulino]

Also #lean-gptf

[Tung Tran]

Woah I didn't know about the streams, thank you!

[Sigma]

An approach which isn't machine learning based would be MMT, at uniformal.github.io, though admittedly I don't know as much about it as I would like.