-
Notifications
You must be signed in to change notification settings - Fork 38
Natural Language to Mathematics
Siddhartha Gadgil edited this page Dec 10, 2019
·
2 revisions
Our goal is to extract from typical mathematical prose, which is a mixture of natural language and formulas, and generate appropriate formal mathematics. The final could be a formal proof system or just a numerical library.
- Natural language and machine learning tools have become very powerful, and are used in many contexts. For mathematics, however, there is great potential in using the extremely structured nature of mathematics together with these generic tools.
- Most obviously, if there is an error in parsing, the result is most likely to not be valid mathematics, so one can try to modify the first result till it becomes valid.
- Further, that statements in the literature are usually not just valid statements but actually true gives plenty of feedback, allowing for unsupervised learning.
- The Stanford parser is used on the prose to obtain constituency parsed trees, i.e., representing sentences as their constituents.
- Various patterns are matched against this, including hard-coded ones and ones that are data.
- The result is a possible parse into a target language.
- The target language may vary, but must belong to an appropriate class - more precisely type-class.
The target language has to admit the following structure on its expressions
- We have operations corresponding to:
- function application
$f(x)$ . - lambda definitions
$(x: A) \mapsto y$ , with$x$ ,$A$ and$y$ all expressions. - (dependent) function types.
- function application
- We have expressions corresponding to
- pair types, including dependent pairs, and associated pair, inclusion and projection maps.
- universes (possibly just ignoring them).
- We can parse tokens into a predefined vocabulary, and have rules for enlarging this by definitions.
- As we are using propositions as types, the above operations and expressions will have many cases if the final implementation is not HoTT.
- The intent is that one can use the formula parsing to drop down to code to do things that are not supported in natural language, for instance new inductive types in homotopy type theory.
- The parsed expressions to be assembled can be sent over a wire.