|
|
Speaker:Title: Neural Theorem Proving in Lean using Proof Artifact Co-training and Language ModelsVenue: virtualSpeaker: Jason Rute, CIBO Technologies Title: Neural Theorem Proving in Lean using Proof Artifact Co-training and Language Models Abstract: Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specialists to be built. This is particularly challenging when applying large Transformer language models to tactic prediction, because the scaling of performance with respect to model size is quickly disrupted in the data-scarce, easily-overfitted regime. We propose PACT ({\bf P}roof {\bf A}rtifact {\bf C}o-{\bf T}raining), a general methodology for extracting abundant self-supervised data from kernel-level proof terms for co-training alongside the usual tactic prediction objective. We apply this methodology to Lean, an interactive proof… |
|
Speaker:Title: A Mathematical LanguageVenue: VirtualSpeaker: Thomas Hales, Univ. of Pittsburgh Dept. of Mathematics Title: A Mathematical Language Abstract: A controlled natural language for mathematics is an artificial language that is designed in an explicit way with precise computer-readable syntax and semantics. It is based on a single natural language (which for us is English) and can be broadly understood by mathematically literate English speakers. This talk will describe the design of a controlled natural language for mathematics that has been influenced by the Lean theorem prover, by TeX, and by earlier controlled natural languages. The semantics are provided by dependent type theory. |
|
|
|
|
Speaker:Title: AI and Theorem ProvingVenue: virtualSpeaker: Josef Urban, Czech Technical University Title: AI and Theorem Proving Abstract: The talk will discuss the main approaches that combine machine learning with automated theorem proving and automated formalization. This includes learning to choose relevant facts for “hammer” systems, guiding the proof search of tableaux and superposition automated provers by interleaving learning and proving (reinforcement learning) over large ITP libraries, guiding the application of tactics in interactive tactical systems, and various forms of lemmatization and conjecturing. I will also show some demos of the systems, and discuss autoformalization approaches such as learning probabilistic grammars from aligned informal/formal corpora, combining them with semantic pruning, and using neural methods to learn direct translation from Latex to formal mathematics. |
|
|
|
|
|
|
|
|