Is Autoformalization just a special case of semantic parsing

Stream: Machine Learning for Theorem Proving

[Xiyu Zhai]

I've seen papers like https://arxiv.org/pdf/2205.12615.pdf trying to use LLMs for "automatically translating from natural language mathematics to a formal language". Although it's exciting to see LLMs can do these things to a certain degree, I'm curious that whether this is actually a special case of semantic parsing. Semantic parsing has been studied for quite a long time in the setting where human interacts with computer through natural languages and I believe LLMs are not absolutely the best for every problems in semantic parsing. It would be great if anyone can share their opinions about this topic.

[Xiyu Zhai]

Semantic parsing is considered dead in NLP (at least one of my friends says so). However, I believe ideas in the field will be very helpful in autoformalizing maths.
With autoformalization, one can gain access to a much larger amount of data than just hand coding lean. And in the future, people might be able to formalize math without knowing lean at all, with a model for translating informal math statements into formal ones and a model for autocompleting the missing trivial steps. If too many steps are missing, the computer can ask the person to give more details. So the future of formalization could be 99% done in natural languages.

[Xiyu Zhai]

When I do lean, the constant pain is to remember how the rules are named in the mathlib. With more math being formalized, it's going to be more painful. So a natural language interface will be more and more desirable.

[Jason Rute]

I thought I recall that the best current semantic parsers are now also language models.

[Jason Rute]

Nonetheless, I think I certainly see value in a tighter connection between Lean (or whatever the system is) and the machine learning model. LeanAide is a nice example of this.

[Xiyu Zhai]

I would say LLM is a necessary part of semantic parsers, but I doubt that it should be the only part.

Given enough data and sufficient compute, llms can be scaled to do literally doing anything.

But for AI math in particular, there could be cheaper plans I guess.

But anyway, I feel like that just prompting ChatGPT should be easily surpassed by more domain specific methods. Let me try to see if this will work.

[Xiyu Zhai]

The current semantic parser tasks are kindof different from autoformalization. "SQL queries (Zhong et al., 2017), robotic commands (Artzi and Zettlemoyer, 2013), smart phone instructions (Quirk et al., 2015), and even general-purpose programming languages like Python (Yin and Neubig, 2017; Rabinovich et al., 2017) and Java" These are not the same as translating the stack project to Lean.

In mathematics, the subset of natural language we use is much smaller and ChatGPT can help translate user input into more unambiguous and commonly accepted form. But I wouldn't say this for things like robotic commands and SQL queries, where the input could be really wild.

[Xiyu Zhai]

Also there is a problem of verifiability. ChatGPT's output is not verifiable. User has to know lean to verify the correctness.

[Timo Carlin-Burns]

If the procedure has to convert "there exists a real number x such that ..." to ∃ x : ℝ, ..., isn't the step where it selected ℝ as the type of real numbers doing something beyond parsing? It feels more like definition lookup than parsing, since it depends on the ambient mathematical library.

[Xiyu Zhai]

It would be nice if things can be separated into two steps, parsing and library lookup

[Xiyu Zhai]

And another point is, parsing is taking an input and giving out an output. The output has to be in some format, so unavoidable it has to do some kind of lookup. We can use a commonly accepted logical formal language. Maybe Lean4 is changing too fast to be that kind of representation.

Personally I would suggest using annotated controlled natural language and then do some lookup or even more advanced handling to translate to Lean4

[Timo Carlin-Burns]

Actually in that particular example, ℝ is notation that happens to be defined as Real, so if you include the ℝ syntax in your notion of the target language, you could say that the translation to ∃ x : ℝ, ... is independent of mathematical library, since each library could each define the notation however it wanted

[Xiyu Zhai]

I believe there could be a "universal semantic parsing", such that autoformalization can be factored into the composition of this "universal semantic parsing" with other simple things like lookup, so that library development can be independently carried out.

[Xiyu Zhai]

I don't believe there is any intractable difficulty in autoformalization. And I believe if it's solved, then it will enhance Lean's experience dramatically.

[Xiyu Zhai]

The difficulty of mathematics is mostly about coming up with the right proof path. Formalizing it wouldn't be that nontrivial. I expect we could come up with much easier tools that basically doesn't require user to know anything but mathematics itself.

[Xiyu Zhai]

The existing tools like ChatGPT+Lean is far from perfect. From my point of view, this is quite a good opportunity actually. The problem is not intractable hard and it's a good chance to show that openai isn't going to win in every battlefield.

[Timo Carlin-Burns]

If your "universal semantic parsing" includes ℝ in its target language, won't it need to include every new mathematical structure as well? It seems like then it would cease to be universal shortly after being released

[Xiyu Zhai]

That's why it's quoted.

[Xiyu Zhai]

We could fix a goal, like proving Fermat's Last Theorem, and only care about related notions. Math is too developed to be tacked in one attempt.

[Dongwei Jiang]

@Xiyu Zhai I agree with you that autoformalization is essentially a type of semantic parsing. In our recent paper, we're converting 'natural language logical reasoning data' (a more traditional NLP task) into 'theorems in Lean,' which feels very much like semantic parsing

[Xiyu Zhai]

Great work, congrats! I'm going to develop a systematic approach with little human effort for autoformalizing Michael Atiyah's commutative algebra. Hope you guys don't scoop me.

[Bas Spitters]

There have been various earlier approaches combining theorem proving with NLP, e.g.
https://www.grammaticalframework.org/ (developed from agda)
Naproche
MOWGLI project: http://mowgli.cs.unibo.it/library/
Ganesalingam and Gowers, e.g. https://link.springer.com/book/10.1007/978-3-642-37012-0