LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

CMSA Room G10 CMSA, 20 Garden Street, Cambridge, MA, United States

https://youtu.be/u-pkmdkQoMU New Technologies in Mathematics Seminar Speaker: Alex Gu, MIT Dept. of EE&CS Title: LeanDojo: Theorem Proving with Retrieval-Augmented Language Models Abstract: Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. However, existing methods are difficult to reproduce or build on, due to private code, data, and large compute […]

Physics of Language Models: Knowledge Storage, Extraction, and Manipulation

CMSA Room G10 CMSA, 20 Garden Street, Cambridge, MA, United States

https://youtu.be/M25cbX5do8Y New Technologies in Mathematics Seminar Speaker: Yuanzhi Li, CMU Dept. of Machine Learning and Microsoft Research Title: Physics of Language Models: Knowledge Storage, Extraction, and Manipulation Abstract: Large language models (LLMs) can memorize a massive amount of knowledge during pre-training, but can they effectively use this knowledge at inference time? In this work, we show several striking […]

Llemma: an open language model for mathematics

CMSA Room G10 CMSA, 20 Garden Street, Cambridge, MA, United States

https://youtu.be/bRHb-MVExJ4 New Technologies in Mathematics Seminar Speaker: Sean Welleck, CMU, Language Technologies Institute Title: Llemma: an open language model for mathematics Abstract: We present Llemma: 7 billion and 34 billion parameter language models for mathematics. The Llemma models are initialized with Code Llama weights, then trained on the Proof-Pile II, a 55 billion token dataset of […]

Mathematics in Science: Perspectives and Prospects

Harvard Science Center 1 Oxford Street, Cambridge, MA

Mathematics in Science: Perspectives and Prospects A showcase of mathematics in interaction with physics, computer science, biology, and beyond. October 27–28, 2023 Location: Harvard University Science Center Hall D & via Zoom. Directions and Recommended Lodging Youtube Playlist   Speakers Nima Arkani-Hamed (IAS) Constantinos Daskalakis (MIT) Alison Etheridge (Oxford) Mike Freedman (Harvard CMSA) Greg Moore (Rutgers) […]

Peano: Learning Formal Mathematical Reasoning Without Human Data

CMSA Room G10 CMSA, 20 Garden Street, Cambridge, MA, United States

https://youtu.be/a2S_-pl6onM New Technologies in Mathematics Seminar Speaker: Gabriel Poesia, Dept. of Computer Science, Stanford University Title: Peano: Learning Formal Mathematical Reasoning Without Human Data Abstract: Peano is a theorem proving environment in which a computational agent can start tabula rasa in a new domain, learn to solve problems through curiosity-driven exploration, and create its own higher level […]

On the Power of Forward pass through Transformer Architectures

CMSA Room G10 CMSA, 20 Garden Street, Cambridge, MA, United States

https://youtu.be/JYt-ldZ3DqM New Technologies in Mathematics Seminar Speaker: Abhishek Panigrahi, Dept. of Computer Science, Princeton University Title: On the Power of Forward pass through Transformer Architectures Abstract: Highly trained transformers are capable of interesting computations as they infer for an input. The exact mechanism that these models use during forward passes is an interesting area of […]

Approaches to the formalization of differential geometry

CMSA Room G10 CMSA, 20 Garden Street, Cambridge, MA, United States

https://youtu.be/oiOpudgC0J4 New Technologies in Mathematics Seminar Speaker: Heather Macbeth, Fordham University Title: Approaches to the formalization of differential geometry Abstract: In the last five years, there has been early work on the computer formalization of differential geometry. I will survey the projects I am aware of. I will also describe two projects of my own, […]

What Algorithms can Transformers Learn? A Study in Length Generalization

CMSA Room G10 CMSA, 20 Garden Street, Cambridge, MA, United States

New Technologies in Mathematics Seminar Speaker: Preetum Nakkiran, Apple Title: What Algorithms can Transformers Learn? A Study in Length Generalization Abstract: Large language models exhibit many surprising “out-of-distribution” generalization abilities, yet also struggle to solve certain simple tasks like decimal addition. To clarify the scope of Transformers' out-of-distribution generalization, we isolate this behavior in a […]

Computers and mathematics in partial differential equations: New developments and challenges

CMSA Room G10 CMSA, 20 Garden Street, Cambridge, MA, United States

https://youtu.be/JB2WqmpmTgk New Technologies in Mathematics Seminar Speaker: Javier Gomez Serrano, Brown University Title: Computers and mathematics in partial differential equations: new developments and challenges Abstract: In this talk I will address the interaction between traditional and more modern mathematics and how computers have helped over the last decade providing rigorous (computer-assisted) proofs in the context […]

LILO: Learning Interpretable Libraries by Compressing and Documenting Code

CMSA Room G10 CMSA, 20 Garden Street, Cambridge, MA, United States

https://youtu.be/ZDMRN0Iyp28 New Technologies in Mathematics Seminar Speaker: Gabe Grand, MIT CSAIL and Dept. of EE&CS Title: LILO: Learning Interpretable Libraries by Compressing and Documenting Code Abstract: While large language models (LLMs) now excel at code generation, a key aspect of software development is the art of refactoring: consolidating code into libraries of reusable and readable programs. […]

Solving olympiad geometry without human demonstrations

Virtual

https://youtu.be/eZbYSOpga2U New Technologies in Mathematics Seminar Speaker: Trieu H. Trinh, Google Deepmind and NYU Dept. of Computer Science Title: Solving olympiad geometry without human demonstrations Abstract: Proving mathematical theorems at the olympiad level represents a notable milestone in human-level automated reasoning, owing to their reputed difficulty among the world’s best talents in pre-university mathematics. Current […]