Translation *to* natural language

Stream: general

[Will Fourie]

Hi all, I haven't found any recent discussions on this that have not mostly ended up being focused on the reverse direction. How feasible would it be for there to be a program which could translate a tactics proof into natural language? Or in general translate expressions in lean into (semi-)natural language. How understandable could the results be?

It is just interesting to think that we have essentially a gigantic textbook here if it would be possible to make it readable. I guess each proof (each definition and theorem, too) may end up being unreasonably detailed and therefore in practice unreadable, but I am curious if anyone has tried and if so what the output ended up looking like?

It seems like committing to the lean library may be easier if you can see in natural language how the library has approached a particular topic.

[Patrick Massot]

We don't have this but some people (including me) are very much interested in making it happen.

[Will Fourie]

Great, I’ll keep my eye out for any developments then, thanks !

[Jireh Loreaux]

Can't Lean Chat just be run in reverse as a first approximation? @Jeremy Avigad I can't remember your student's name that implemented Lean Chat.

[Jason Rute]

:up: @Zhangir Azerbayev and @Edward Ayers

[Jason Rute]

@Will Fourie First, if you are not aware, you may want to subscribe to the #Machine Learning for Theorem Proving stream. As for formal-to-informal, while there isn't as much already written on this topic, I would say the same ideas as informal-to-formal apply. In particular, I see three main possibilities:

[Jason Rute]

1. rule based translation This is really hard to get right in either direction, but I think there is more possibility for success in the formal-to-informal direction. Indeed, while I would have to remind myself, there was some work done on this in maybe the early 2000s. (Freek Wiedijk's website is a great place to go to get a snapshot of that time period.) If I recall, there was works taking Mizar-style proofs and translating them to structured natural language with rules and also reducing the full formal proof to a proof sketch which is an outline of the full proof and is more human readable. Tom Hales as part of his formal abstract project (which never got off the ground) was interested in making a controlled natural language which was completely formal, but at the same time more human-readable. (I don't think however it focused on proofs nor was it meant to translate Lean into controlled natural language automatically.)

[Jason Rute]

2. machine learning translation There have been lots of works translating informal math to formal math, although until recently they weren't especially good. The problem was not that the methods were bad. There is a lot of work on translation of natural language. The problem was a lack of data. However, that is now as of a few months ago, starting to change. The big change is that folks have realized it is possible to use pre-trained large language models on code like Codex (which powers Github copilot) and use it for auto-formalization.

[Jason Rute]

The first paper in this area was https://arxiv.org/abs/2205.12615. The idea is simple: Give the model a few (3-5) examples of the type of translation you have in mind, and then ask it to complete in your example. That paper showed that the model was ok at both informal-to-formal ("auto-formalization") and formal-to-informal ("auto-informalization"). Actually it was much better at informalization. This work has inspired a lot more work on this area. @Zhangir Azerbayev and @Edward Ayers adapted this to Lean with the Lean chat plugin. (It just does auto-formalization last I checked, but that is just a design choice.) There are also two more papers in this area as of last week. See #Machine Learning for Theorem Proving > More papers on autoformalization.

[Jason Rute]

I should also mention that Codex-powered auto-(in)formalization is really easy to play with. Just get an OpenAI codex key, and try it out. To understand exactly how it works, you can look at the code in https://github.com/zhangir-azerbayev/lean-chat, but to be clear, once you construct your prompt with the 3-5 examples you can just play around with it in the Codex online website.

[Jason Rute]

3. human translation
Human translation is still the best approach so far. And the big challenge as I see it is just encouraging users to document their proofs and making tools to make it easier. These tools could be:

• Adding comments to the formal proof. Some comments (namely doc strings) will even show up on the #docs (e.g. docs#separate_convex_open_set).
• Using https://github.com/leanprover-community/format_lean or https://github.com/leanprover/LeanInk/blob/main/LeanInk/Annotation/Alectryon.lean to mix a Lean file with HTML/markup for a better display.
• Using the lean blueprint tool (see an example in Sphere Inversion project) to link latex proofs with Lean proofs to document an entire lean project.)

[Will Fourie]

Fantastic! Thank you, I’ve subscribed to the stream and will definitely give codex a look. The human translation links looks helpful too, at least for when I am writing

[Zhangir Azerbayev]

Few-shot informalization with Codex is much better than formalization. I've done systematic evaluations of Codex's formalization/informalization capabilities on undergraduate-level math (soon to be public), and informalization accuracy is >50%.

Lean chat could be easily extended to also do informalization. I'll talk to @Edward Ayers and see if we have time to implement this. Alternatively, anyone who has front-end development can open a PR themselves, the code is public.

Something else you might be interested is this mathlib doc-gen PR by myself and @Rob Lewis . It adds a drop-down to every theorem in the mathlib docs that contains a Codex informalization. Here is a link to the experimental build. Some of the examples are really impressive. @Rob Lewis is there still interest in getting this over the line?

[Michael Stoll]

I've looked at the file number_theory.legendre_symbol.quadratic_reciprocity and found that in many cases, the informal description is slightly off. Some things I have noticed are

• p % 4 ≠ 3 (for p a prime) gets translated into $p \equiv 1 \bmod 4$, even though p = 2 is not excluded.
• Coercions are not picked up. E.g., a condition (a : zmod p) ≠ 0 appears as $a \neq 0$.
• Sometimes, an assumption that a prime p is odd is sneaked in, even though it is not there.
• Truncated division is rendered as division (as in $(-1)^{p/2}$).
• Notation for the Legendre symbol varies ($\left(\frac{a}{p}\right)$, $(a/p)$, $(a|p)$, the Legendre symbol $a$ mod $p$).
• Sometimes, the interpretation/definition of the symbol in terms of quadratic (non-)residues is used instead of the symbol.

A fairly typical example showing several of these points:

theorem zmod.legendre_sym_eq_neg_one_iff_not_one (p : ℕ) [fact (nat.prime p)] {a : ℤ} (ha : ↑a ≠ 0) :
zmod.legendre_sym p a = -1 ↔ ¬zmod.legendre_sym p a = 1

Informal translation:
Let $p$ be a prime and let $a$ be an integer such that $a \neq 0$. Then $a$ is a quadratic residue modulo $p$ if and only if $a$ is not a quadratic non-residue modulo $p$.

[Michael Stoll]

An example I don't really know how to fix:

theorem zmod.legendre_sym_hom_apply (p : ℕ) [fact (nat.prime p)] (a : ℤ) :
⇑(zmod.legendre_sym_hom p) a = zmod.legendre_sym p a

Let $p$ be a prime. Then the Legendre symbol is a homomorphism from $\mathbb{Z}/p\mathbb{Z}$ to $\mathbb{Z}/2\mathbb{Z}$.

[Michael Stoll]

One reason could be that Codex "remembers" various versions of the informal statements that it has seen, which are close to, but not completely equivalent to the mathlib versions. E.g., because the mathlib version includes 2, but the textbook versions are usually for odd primes...

[Michael Stoll]

Statements like the following that do not really have mathematical content seem to be especially bad for this kind of translation.

theorem mul_char.to_fun_eq_coe {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') :
χ.to_monoid_hom.to_fun = ⇑χ

"Let $R$ be a commutative monoid and let $R'$ be a commutative monoid with zero. Let $\chi:R\to R'$ be a multiplicative character. Then $\chi$ is a monoid homomorphism if and only if $\chi(1)=1$."

But then it probably does not really make sense to try to give an informal description of this kind of boilerplate...

[Jason Rute]

@Zhangir Azerbayev probability.martingale doesn't have translations. Don't know if this means they are still being generated or if this is a bug, but just wanted to let you know.

[Jason Rute]

But, I agree it is very impressive!

[Jason Rute]

I also agree with Michael that it makes some really confusing choices where it just tries to state the well-known mathematical theorem that it thinks is closest to the content in this theorem even if they are really about very different main ideas. When it is right, it seems amazing, but when it is wrong it can be really confusing because it's translation is a true fact often, and it concerns most of the ideas in the theorem, so it is very believable, even if it isn't helpful at all. Good thing you add the disclaimer. :smile: