New paper: Use Lean to help with natural language reasoning

Stream: Machine Learning for Theorem Proving

[Dongwei Jiang]

This is not particularly related to mathematical theorem proving but still quite relevant to ML and Lean so I will just share it here (feel free to move it to other streams if needed). In our new work, we have shown that Lean can help with natural language reasoning!

This works by formalizing natural language logical problems into Lean code (examples here) and then proving/disproving the resulting theorm (with LeanDoJo) to get an answer. The help of Lean comes in two ways:
1 Within Lean's framework, there can be no invalid statement, so there can be no hallucination during the reasoning process
2 By fine-tuning on ReProver that is pre-trained with mathlib3, we're effectively leveraging the reasoning nuggets learned through training on theorem-proving data to help with natural language reasoning. This is another piece of evidence showing teaching LLMs to do math can help with logic and reasoning in general.

Many thanks to people in this forum who graciously offered me help (through replies and emails), especially @Jason Rute, @Albert Jiang and @Stanislas Polu !