ucb_agentic_ai

Lecture 09: Language Models for Autoformalization and Theorem Proving

Link to lecture recording on YouTube

Date: 2025-04-07

Speaker: Kaiyu Yang 杨凯峪

Speaker’s social profile: Website / Google Scholar / GitHub / LinkedIn / X (Twitter)

Education:

Work:

Notes

AI arms race: leading companies release a new model every few months, and at the center is math and coding

Why math and coding?

Math and coding problems are deeply connected

Two main techniques to train LLMs to solve math problems:

[Incomplete, work in progress]

References