Elamur Research⌕
☰
home / papers / 2024 / LeanReasoner: Boosting Complex Logical Reasoning with Lean

LeanReasoner: Boosting Complex Logical Reasoning with Lean

Paper · 2024 · Dongwei Jiang, Marcio Fonseca and Shay B. Cohen

Summary

Large language models often fail at multi-step logical reasoning because they make unsupported or contradictory inferences. LeanReasoner addresses this by recasting each natural-language reasoning problem as theorems in the Lean theorem prover. An LLM (text-davinci-003 or GPT-4) acts as a formalizer that turns the context into Lean axioms. The question becomes two competing theorems, one asserting the claim and one negating it. Lean's compiler checks the syntax, and errors are fed back for one retry. A tactic generator based on ReProver, which pairs a DPR-style premise retriever with a seq2seq model, then builds proofs through proof search. A result interpreter maps the outcome to True, False or Unknown, where Unknown means neither theorem could be proven. Because ReProver is pre-trained on mathematical proofs, the approach can draw on Lean's large proof corpus. The system reaches state-of-the-art accuracy on FOLIO and comes close to the best result on ProofWriter, using fewer than 100 annotated in-domain examples per dataset. The work suggests that mathematical theorem-proving resources can support general logical reasoning in natural language.

Key points

  • The authors describe this as the first use of Lean, a tool usually reserved for mathematics, for natural-language logical reasoning. Lean's library contains over 100,000 theorems and about 1,000,000 lines of code.
  • The pipeline has four parts: a formalizer (GPT-3/GPT-4), a tactic generator (ReProver with a DPR-based retriever), a proof search procedure, and a result interpreter.
  • Pre-training on theorem-proving data gave a stronger solver than earlier symbolic approaches such as Logic-LM (Pyke) and SATLM (Z3). The authors also compare concise and intuitive styles of proof annotation.
  • The released resource contains 100 Lean-formalized ProofWriter problems and 27 FOLIO problems, together with their Lean proofs.
  • The method is weak on commonsense and world-knowledge tasks (MMLU, SummEdits), numeric math word problems, and TheoremQA. Constraint-style tasks like BigBench LogicalDeduction are better handled by CSP solvers.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓University of EdinburghEdinburgh · United Kingdom395 works · 81,691 citations🎓Johns Hopkins UniversityBaltimore · United States254 works · 106,461 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Dongwei Jiang, Marcio Fonseca and Shay B. Cohen. 2024. LeanReasoner: Boosting Complex Logical Reasoning with Lean. arXiv:2403.13312.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2403.13312 · arXiv 2403.13312

@misc{jiang2024leanreasoner,
  title = {{LeanReasoner: Boosting Complex Logical Reasoning with Lean}},
  author = {Dongwei Jiang, Marcio Fonseca and Shay B. Cohen},
  year = {2024},
  doi = {10.48550/arxiv.2403.13312},
  eprint = {2403.13312},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2403.13312}
}

References

27 references, 19 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Tao Yu, Rui Zhang, Shafiq R. Joty, Alexander R. Fabbri, Wojciech Kryscinski, Xi Victoria Lin, Caiming Xiong, and Dragomir Radev. 2022b. FOLIO: natural language reasoning with first-order logic. CoRR.
  2. Fabian Gloeckle Baptiste Rozière, Jonas Gehring and et.al. 2023. Code llama: Open foundation models for code. CoRR, abs/2308.12950.
  3. Jianshu Chen. 2023. Learning language representations with logical inductive bias. In ICLR. OpenReview.net. find
  4. Joy He-Yueya, Gabriel Poesia, Rose E. Wang, and Noah D. Goodman. 2023. Solving math word problems by combining language models with symbolic solvers.
  5. Wenhu Chen, Ming Yin, Max Ku, Pan Lu, Yixin Wan, Xueguang Ma, Jianyu Xu, Xinyi Wang, and Tony Xia. 2023a. Theoremqa: A theorem-driven question answering dataset.
  6. Dan Hendrycks, Collin Burns, Steven Basart, Andy Zou, Mantas Mazeika, Dawn Song, and Jacob Steinhardt. 2020. Measuring massive multitask language understanding.
  7. Zeming Chen, Gail Weiss, Eric Mitchell, Asli Celikyilmaz, and Antoine Bosselut. 2023b. RECKON-ING: reasoning through dynamic knowledge encoding. CoRR, abs/2305.06349.
  8. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. Measuring Mathematical Problem Solving With the MATH Dataset. In NeurIPS, Menlo Park, Calif. AAAI Press.
  9. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. 2021. Training verifiers to solve math word problems.
  10. Vladimir Karpukhin, Barlas Oguz, Sewon Min, Patrick S. H. Lewis, Ledell Wu, Sergey Edunov, Danqi Chen, and Wen-tau Yih. 2020. Dense passage retrieval for open-domain question answering. In EMNLP.
  11. Philippe Laban, Wojciech Kryscinski, Divyansh Agarwal, Alexander R. Fabbri, Caiming Xiong, Shafiq Joty, and Chien-Sheng Wu. 2023. Llms as factual reasoners: Insights from existing benchmarks and beyond. find
  12. Antonia Creswell and Murray Shanahan. 2022. Faithful reasoning using large language models. CoRR, abs/2208.14271.
  13. Ishita Dasgupta, Andrew K. Lampinen, Stephanie C. Y. Chan, Antonia Creswell, Dharshan Kumaran, James L. McClelland, and Felix Hill. 2022. Language models show human-like content effects on reasoning. CoRR. find
  14. Guillaume Lample, Timothée Lacroix, Marie-Anne Lachaux, Aurélien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. 2022. Hypertree proof search for neural theorem proving. In NeurIPS.
  15. Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008. Z3: an efficient SMT solver. In TACAS. find
  16. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay V. Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. 2022. Solving quantitative reasoning problems with language models. In NeurIPS.
  17. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The lean theorem prover (system description). In CADE-2. find
  18. Hao Fu, Yao; Peng and Tushar Khot. 2022. How does gpt obtain its ability? tracing emergent abilities of language models to their sources. Yao Fu’s Notion. find
  19. Theo Olausson, Alex Gu, Benjamin Lipkin, Cedegao E. Zhang, Armando Solar-Lezama, Joshua B. Tenenbaum, and Roger Levy. 2023. LINC: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. In EMNLP.
  20. Yao Fu, Hao Peng, Ashish Sabharwal, Peter Clark, and Tushar Khot. 2023. Complexity-based prompting for multi-step reasoning. In ICLR. OpenReview.net.
  21. Nicolas Gontier, Siva Reddy, and Christopher Pal. 2022. Does entity abstraction help generative transformers reason? Trans. find
  22. OpenAI. 2023. GPT-4 technical report. CoRR.
  23. Liangming Pan, Alon Albalak, Xinyi Wang, and et.al. 2023. Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning.
  24. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. 2022a. Proof artifact co-training for theorem proving with language models. In ICLR.
  25. Gabriel Poesia, Kanishk Gandhi, Eric Zelikman, and Noah D. Goodman. 2023. Certified reasoning with language models. CoRR. find
  26. Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Luke Benson, Lucy Sun, Ekaterina Zubova, Yujie Qiao, Matthew Burtell, David Peng, Jonathan Fan, Yixin Liu, Brian Wong, Malcolm Sailor, Ansong Ni, Linyong Nan, Jungo Kasai, Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas… — Formal Mathematics Statement Curriculum Learning
  27. Stanislas Polu and Ilya Sutskever. 2020. Generative language modeling for automated theorem proving. CoRR, abs/2009.03393.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/jiang-2024-leanreasoner-boosting-complex-logical-reasoning/