Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization

arXiv:2403.18120v1 Announce Type: cross
Abstract: Large language models (LLM), such as Google's Minerva and OpenAI's GPT families, are becoming increasingly capable of solving mathematical quantitative reasoning problems. However, they still make unjustified logical and computational errors in their reasoning steps and answers. In this paper, we leverage the fact that if the training corpus of LLMs contained sufficiently many examples of formal mathematics (e.g. in Isabelle, a formal theorem proving environment), they can be prompted to translate i.e. autoformalize informal …

arxiv cs.ai cs.cl cs.lg llm quantitative reasoning trust type verify