Peano: learning formal mathematical reasoning

7Citations
Citations of this article
39Readers
Mendeley users who have this article in their library.
Get full text

Abstract

General mathematical reasoning is computationally undecidable, but humans routinely solve new problems. Moreover, discoveries developed over centuries are taught to subsequent generations quickly. What structure enables this, and how might that inform automated mathematical reasoning? We posit that central to both puzzles is the structure of procedural abstractions underlying mathematics. We explore this idea in a case study on five sections of beginning algebra on the Khan Academy platform. To define a computational foundation, we introduce Peano, a theorem-proving environment where the set of valid actions at any point is finite. We use Peano to formalize introductory algebra problems and axioms, obtaining well-defined search problems. We observe existing reinforcement learning methods for symbolic reasoning to be insufficient to solve harder problems. Adding the ability to induce reusable abstractions ('tactics') from its own solutions allows an agent to make steady progress, solving all problems. Furthermore, these abstractions induce an order to the problems, seen at random during training. The recovered order has significant agreement with the expert-designed Khan Academy curriculum, and second-generation agents trained on the recovered curriculum learn significantly faster. These results illustrate the synergistic role of abstractions and curricula in the cultural transmission of mathematics. This article is part of a discussion meeting issue 'Cognitive artificial intelligence'.

Cite

CITATION STYLE

APA

Poesia, G., & Goodman, N. D. (2023). Peano: learning formal mathematical reasoning. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 381(2251). https://doi.org/10.1098/rsta.2022.0044

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free