LeanAide translation: Natural language to Lean 3

Stream: general

[Anand Rao]

We also have a version of the LeanAide tool for Lean 3. It is hosted at this repository: https://github.com/0art0/lean3-statement-translation-tool. Here is a demonstration of the tool in action:

leanaide_demo.gif

A video with more details: leanaide_demo.mkv

Instructions for trying out and using the tool are mentioned in the Quickstart section of the README file. Suggestions and contributions to the code are welcome. The tool will be maintained until we eventually switch to Lean 4 entirely. Feedback on the tool will also be highly appreciated.

[Jason Rute]

How does this differ in scope, method, tooling, or quality of results from LeanChat (repo) (discussed in #Machine Learning for Theorem Proving > A chat interface for formalizing theorem statements and #Machine Learning for Theorem Proving > Lean Chat is publicly available)

[Jason Rute]

I think like LeanChat you are also translating statements only, right?

[Jason Rute]

Your tool looks to be more integrated into Lean, correct? In particular, you can dynamically choose a prompt I think, but I'd have to remind myself of the details.

[Jason Rute]

And it checks that the result elaborates, which LeanChat doesn't do, right?

[Jason Rute]

But unlike LeanChat, it doesn't have a way to provide back any forth feedback to the model, at least in right now, correct/

[Anand Rao]

Yes, that's correct. The main difference with Lean Chat is the prompting strategy we use - input-dependent prompting instead of fixed-shot prompting. We have mined mathlib for Lean theorems and their corresponding doc-strings, and the Python code running on our server allows us to use sentence similarity to fetch statements from this database related to the sentence we want to translate.

We have observed in our experiments that the combination of input-dependent prompting and filtering by elaboration pushes up the number of successful translations to more than half. These experiments were done on a dataset consisting of single sentence, doc-string like statements at the undergraduate level.

We also use Lean to pick up declarations from the same file that have doc-strings and append them to the prompt. This, in principle, allows the model to formalise concepts that were not in mathlib during its training, or even at the time we mined mathlib for the doc-strings. This is one of the reasons we have chosen to integrate our UI into Lean, as you mentioned.

We are currently focused on just theorem translation, but we may expand to definition translation too in the next few months. Since we pick up declarations from the focused file, users can (implicitly) add to the prompt by adding theorems with doc-strings to the file in which they are working. We do not have a mechanism for back-and-forth feedback like Lean Chat, but our modifications also reduce the need for it (at least for the kinds of statements that we experimented on). We observed that passing the type-checking filter is a good proxy for actually being a valid Lean translation (though being type-correct may be less suitable as a proxy for multi-line statements or statements involving complicated formulae).

[Siddhartha Gadgil]

One additional point to the above (though this is stronger in the Lean 4 interface) we feel that integrating with the editor is more ergonomic, quite a bit like copilot. In the Lean 4 interface, the user types a comment and this can be translated, with the comment becoming a doc-string.

But as Anand said, the biggest difference is input-dependent prompting and filtering completions by elaboration. We also do a bit of auto-correction.