Advanced LLM Agents is the UC Berkeley Spring 2025 sequel to the Fall 2024 LLM Agents MOOC on this site. Twelve lectures from January 27 through April 28, 2025, focused on advanced reasoning, formal mathematics, and verifiable code generation using Lean. The series was rebranded as Agentic AI MOOC for Fall 2025 onward. Co taught by Professor Dawn Song, Xinyun Chen of Google DeepMind, and Kaiyu Yang of Meta FAIR.
Advanced LLM Agents: What You’ll Learn
This is the advanced sequel to Post 05 on this site, the Berkeley LLM Agents MOOC F24. SP25 trades breadth for depth. The Fall 2024 course was a survey of foundations, frameworks, enterprise, robotics, RAG, and multi agent. Spring 2025 drops the breadth and goes deep on two domains, inference time reasoning and post training, and formal mathematics with theorem proving and verifiable code generation.
The course is explicit about the prerequisite. The SP25 page states directly, this course is built upon the fundamentals from the Fall 2024 LLM Agents MOOC. If you have not done F24, do it first.
Advanced LLM Agents: The Twelve SP25 Lectures
- Jan 27. Inference Time Techniques for LLM Reasoning, Xinyun Chen, Google DeepMind.
- Feb 3. Learning to reason with LLMs, Jason Weston, Meta.
- Feb 10. On Reasoning, Memory, and Planning of Language Agents, Yu Su, Ohio State.
- Feb 24. Open Training Recipes for Reasoning in Language Models, Hanna Hajishirzi, UW.
- Mar 3. Coding Agents and AI for Vulnerability Detection, Charles Sutton, Google DeepMind.
- Mar 10. Multimodal Autonomous AI Agents, Ruslan Salakhutdinov, CMU and Meta.
- Mar 17. Multimodal Agents From Perception to Action, Caiming Xiong, Salesforce AI Research.
- Mar 31. AlphaProof when reinforcement learning meets formal mathematics, Thomas Hubert, Google DeepMind.
- Apr 7. Language models for autoformalization and theorem proving, Kaiyu Yang, Meta FAIR.
- Apr 14. Bridging Informal and Formal Mathematical Reasoning, Sean Welleck, CMU.
- Apr 21. Abstraction and Discovery with Large Language Model Agents, Swarat Chaudhuri, UT Austin.
- Apr 28. Towards building safe and secure agentic AI, Dawn Song, UC Berkeley.
The Lean Labs
SP25 has two labs, down from F24’s three. Both labs use Lean for verifiable code generation. The course description is explicit, there are two labs to give students experience with verificable code generation agents using Lean. Students must pass both labs to receive credit towards the Mastery Tier Certificate.
The Lean emphasis is the differentiator from F24. If you want to build agents that write code with mathematical correctness guarantees, this is the only free course we know of that teaches it.
Prerequisites
Berkeley upper division CS level. Solid ML and DL foundations. Comfort with LLM papers. For the formal math track, lectures 8 through 11, familiarity with Lean or other theorem provers helps. The two labs use Lean explicitly.
The F24 MOOC on this site is effectively a prerequisite. SP25 does not reteach foundations. A learner skipping F24 will find lectures 8 through 11 especially steep.
AgentX Competition
The SP25 hackathon is called AgentX, with two tracks. The Entrepreneurship Track wants a working MVP, pitch deck of at most twenty slides, and a three minute demo video. Up to forty thousand dollars in cash plus sponsor credits from Groq, Hugging Face, Lambda, Mistral, Auth0, Writer, and Google Gemini 2.0 Flash. The Research Track wants a seven to eight page scientific paper plus video plus GitHub repo. Demo Day was August 2, 2025, in person at the Agentic AI Summit at UC Berkeley.
Run a Lean Lab Locally
git clone https://github.com/rdi-berkeley/llm-agents-mooc.git
# Lab starter code is in Google Drive, linked from the SP25 Labs section
# Requires Lean 4 and elanA Worked Example, Lecture 8 AlphaProof in Depth
Thomas Hubert’s March 31 lecture covers AlphaProof, the DeepMind system that achieved silver medal level on the International Mathematical Olympiad. The system trains on formally stated mathematical problems in Lean, uses reinforcement learning to improve proof search, and combines a language model with a formal verifier. The lecture covers the architecture, the training data, and what worked versus what did not. For anyone interested in agents that reason formally, this is the canonical reference.
Advanced LLM Agents: Common Mistakes to Avoid
- Skipping F24 first. SP25 assumes F24. The formal math lectures will be incomprehensible without the foundations.
- Treating the Lean labs as optional. The Mastery tier requires passing both labs. Without them you stop at Trailblazer.
- Expecting robotics or enterprise content. SP25 dropped both. If you need them, do F24 instead.
- Confusing SP25 with Fall 2025 Agentic AI MOOC. The series was rebranded. Fall 2025 at
agenticai-learning.org/f25is the next iteration after SP25.
Advanced LLM Agents: Best Practices
- Do F24 on this site first. The ordering is non negotiable for SP25.
- Install Lean 4 and elan before Lecture 8. The labs assume you have a working Lean environment.
- Pair with the F24 course on this site for the foundations SP25 assumes.
- Read the AlphaProof paper before Lecture 8. The lecture is dense and the paper is the canonical reference.
- Submit to AgentX if you want the Ninja or Legendary tier. The competition is the path.
Advanced LLM Agents: Frequently Asked Questions
Is SP25 still free?
Yes. All materials public on the Berkeley RDI site and YouTube.
Is F24 a prerequisite?
Effectively yes. The course states this directly.
Does SP25 still issue certificates?
Yes. Same five tier structure as F24. Mastery requires the two Lean labs.
How is SP25 different from F24?
SP25 drops breadth, goes deep on reasoning and formal math. F24 is the survey, SP25 is the deep sequel.
What is Lean?
Lean is a functional programming language and theorem prover. The two SP25 labs use it for verifiable code generation.
Is there a Fall 2025 iteration?
Yes, rebranded as Agentic AI MOOC at agenticai-learning.org/f25.
Advanced LLM Agents SP25 is the formal math sequel to F24. Pair with F24 for the full Berkeley arc.