Learning formal mathematical abstractions

Abstract: Mathematical abstractions are devices that enable general representations of many concrete mathematical objects at once: they include definitions, lemmas, proof strategies and algorithms. Typically, computer agents applied in formal mathematics are given a set of human-created abstractions (e.g., definitions, tactics, lemmas in Lean's mathematical library) and receive tasks that involve using and combining those (e.g., proving a given theorem). This talk will instead focus on our work on automatically learning the abstractions themselves. We'll first describe our initial work on this line on learning problem-solving tactics for Khan Academy algebra problems in a simple dependently-typed theorem proving environment. Then, we will use these principles to learn tactics in the Rocq (formerly Coq) theorem prover from existing corpora of human proofs. In both cases, tactic learning is operationalized by a symbolic compression procedure, a principle that has been fruitful in learning abstractions in the field of program synthesis. I'll end by briefly describing ongoing work on a compression-based library learning method for terms in Lean's type theory, and highlight several applications of this tool. In particular, compressing sets of theorem statements yields new mathematical definitions that help compactly rewrite the statements, whereas compressing proof terms gives rise to lemmas that shorten existing proofs.

machine learninglogic in computer sciencemathematical softwaresoftware engineeringlogic

Audience: researchers in the topic

Online logic seminar

Series comments: Description: Seminar on all areas of logic