NaturalProver: Grounded Mathematical Proof Generation with Language Models. (arXiv:2205.12910v1 [cs.CL])

Theorem proving in natural mathematical language - the mixture of symbolic
and natural language used by humans - plays a central role in mathematical
advances and education, and tests aspects of reasoning that are core to
intelligence. Yet it has remained underexplored with modern generative models.
We study large-scale language models on two new generation tasks: suggesting
the next step in a mathematical proof, and full proof generation. Naively
applying language models to these problems yields proofs riddled with
hallucinations …

arxiv generation language language models