Autoformalization with Large Language Models - IPAM at UCLA
Offered By: Institute for Pure & Applied Mathematics (IPAM) via YouTube
Course Description
Overview
Explore the cutting-edge field of autoformalization with large language models in this 55-minute conference talk by Tony Wu from Google. Delve into the process of automatically translating natural language mathematics into formal specifications and proofs, and discover how this technology could revolutionize formal verification, program synthesis, and artificial intelligence. Examine the intuition behind autoformalization, learn about model translation and two-shot training techniques, and analyze failure cases and takeaways. Investigate translational proofs, formal sketches, and benchmark results through practical examples, including an alarm proof. Gain valuable insights into the future prospects of autoformalization and its potential impact on advancing mathematical research and artificial intelligence capabilities.
Syllabus
Introduction
What is a parameter
Intuition
Autoformalization
Model Translation
TwoShot Training
Failure Case
Takeaways
Translational Proof
Formal Sketch
Results
Benchmark
Examples
Alarm Proof
Taught by
Institute for Pure & Applied Mathematics (IPAM)
Related Courses
Introduction to Artificial IntelligenceStanford University via Udacity Probabilistic Graphical Models 1: Representation
Stanford University via Coursera Artificial Intelligence for Robotics
Stanford University via Udacity Computer Vision: The Fundamentals
University of California, Berkeley via Coursera Learning from Data (Introductory Machine Learning course)
California Institute of Technology via Independent