Elamur Research⌕
☰
home / papers / 2022 / Peano: Learning Formal Mathematical Reasoning

Peano: Learning Formal Mathematical Reasoning

Paper · 2022 · Gabriel Poesia and Noah D. Goodman

Summary

Mainstream proof assistants like Lean, Coq and Isabelle allow infinitely many valid steps at each point, which complicates treating proof finding as search. Poesia and Goodman propose Peano, a dependently typed language whose environment always offers a finite set of actions. With it, they formalize axioms and exercises from five introductory algebra sections of Khan Academy, producing well-defined search tasks. An existing reinforcement learning method masters only the first two sections, because later solutions become too long to find by exploration. The authors add tactic induction: anti-unification extracts recurring patterns from the agent's own solutions and turns them into new higher-level actions. With this, the agent eventually solves every problem. When problems are ordered by dependencies among the learned tactics, the resulting sequence significantly agrees with Khan Academy's expert curriculum, and a second agent trained in that order learns faster. The work offers a computational account of how abstractions and curricula jointly drive mathematical learning and its transmission across generations.

Key points

  • Peano is a theorem-proving language built on dependent types (propositions as types, proofs as programs). Its search environment keeps the action space finite at every step.
  • Benchmark: 5 sections of the Khan Academy beginning-algebra curriculum, with axioms and exercises encoded in Peano. Agents start with no solving strategies beyond the axioms.
  • Tactic learning: the baseline RL agent stalls after the first two sections. Tactics induced via anti-unification are short straight-line programs that can call axioms or other tactics, and they let the agent eventually solve all problems.
  • Curriculum recovery: problems were seen in random order during training, yet the learned tactics imply an order that matches Khan Academy's significantly. "Second-generation" agents trained on this recovered order learn significantly faster.
  • Limitations and resources: Peano has no intermediate lemmas (lambda terms) and no backward reasoning, and its tactics cannot express loops or conditionals. Code, data and configs are available at github.com/gpoesia/peano.

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

🎓Stanford UniversityStanford · United States567 works · 335,190 citations

 Fields, topics and concepts

📚 Shelves 2The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 works

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

Cite

Cite as Gabriel Poesia and Noah D. Goodman. 2022. Peano: Learning Formal Mathematical Reasoning. arXiv:2211.15864.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.1098/rsta.2022.0044 · arXiv 2211.15864

@misc{poesia2022peano,
  title = {{Peano: Learning Formal Mathematical Reasoning}},
  author = {Gabriel Poesia and Noah D. Goodman},
  year = {2022},
  doi = {10.1098/rsta.2022.0044},
  eprint = {2211.15864},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1098/rsta.2022.0044}
}

References

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

  1. Thomas Anthony, Zheng Tian, and David Barber. Thinking fast and slow with deep learning and tree search. Advances in Neural Information Processing Systems, 30, 2017.
  2. Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, volume 97… — HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
  3. Yoshua Bengio, Jérôme Louradour, Ronan Collobert, and Jason Weston. Curriculum learning. In Proceedings of the 26th annual international conference on machine learning, pages 41–48, 2009.
  4. Kyunghyun Cho, Bart van Merriënboer, Dzmitry Bahdanau, and Yoshua Bengio. On the properties of neural machine translation: Encoder–decoder approaches. Syntax, Semantics and Structure in Statistical Translation, page 103, 2014. — On the Properties of Neural Machine Translation: Encoder-Decoder Approaches
  5. Simon Colton, Alan Bundy, and Toby Walsh. On the notion of interestingness in automated mathematical discovery. International Journal of Human-Computer Studies, 53(3):351–375, 2000. find
  6. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, 1962. find
  7. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM (JACM), 7(3):201–215, 1960. find
  8. Kevin Ellis, Catherine Wong, Maxwell Nye, Mathias Sablé-Meyer, Lucas Morales, Luke Hewitt, Luc Cary, Armando Solar-Lezama, and Joshua B Tenenbaum. Dreamcoder: Bootstrapping inductive program synthesis with wake-sleep library learning. In Proceedings of the 42nd acm sigplan international conference o… find
  9. William Timothy Gowers. – . . . - . 0000000 .......... find

Updated

This page in Markdown → https://md.research.elamur.ai/free/en/papers/poesia-2022-peano-learning-formal-mathematical-reasoning/