Language Modeling for Formal Mathematics

By Markus Norman Rabe, Dennis Lee, Kshitij Bansal, Christian Szegedy. 2020

We examine whether language modeling applied to mathematical formulas enables logical reasoning. We suggest several logical reasoning tasks that can be used to evaluate language models trained on formal mathematical statements, such as type inference, suggesting missing assumptions and completing equalities. To train language models for formal mathematics, we propose a novel skip-tree task, which outperforms standard language modeling tasks on our reasoning benchmarks. We also analyze the models' ability to formulate new conjectures by measuring how often the predictions that do not fit the ground truth or any training data turn out to be true and useful statements.

Subfields: Large Language Models

Citations in the corpus

• Mathematical Capabilities of ChatGPT (2023, unknown): “Some of the ideas that we have used in this article, such as prompting with missing proofs, are echoed in [31] for formal mathematics.”