Learning Formal Reasoning
Gabriel Poesia
Abstract: Formal systems, such as type theories, provide general foundations for representing mathematics and computation, with increasing adoption in the formalization of research-level mathematical results, as well as for implementing and verifying critical real-world software. However, their flexibility comes at a cost: most key problems in these systems, like finding proofs, are computationally undecidable. Nonetheless, humans routinely solve novel mathematical problems, write new programs and prove them correct. Crucially, we leverage our ability to learn, developing increasingly better heuristics and abstractions for our domains of interest. We do so even without specific goals other than making interesting discoveries.
In this talk, I’ll present my research addressing fundamental challenges arising in learning formal reasoning. First, I’ll show how reinforcement learning and abstraction learning combined enable an agent to master sections from the Khan Academy algebra curriculum, and even reconstruct the human-designed curriculum using its learned abstractions, despite seeing problems in a random order. Then, I’ll present my work on open-ended learning for theorem proving, where an agent learns from self-generated conjectures, bootstrapping its ability to prove human-written theorems despite only training on proofs it found by itself. Along the way, I’ll present methods for interfacing symbolic and neural systems, with applications to program generation and verification, and discuss standing challenges in developing self-improving reasoning machines.
Speaker Bio: Gabriel Poesia is a PhD student at Stanford University in the Computation and Cognition Lab. His research is centered on learning formal reasoning, interfacing dependent type theory, language models, reinforcement learning and intrinsically motivated learning, with work at the intersection of all these ares recognized with an Oral presentation at NeurIPS 2024. His research has been supported by the Stanford Interdisciplinary Graduate Fellowship.