Seminar Details

Recent progress in LLMs has transformed text and code generation, yet models still falter on PDEs (partial differential equation) where correctness, constraints, and physical consequences are critical. This talk explores how formal LLM reasoning can advance symbolic PDE modeling. First, our PDE-Controller formalizes informal PDEs, synthesizes solver-ready code, and plans subgoals to tackle nonconvex control via interactions with external solvers. Second, our Lean Finder accelerates PDE formalization with a semantics-aware search engine for Lean/Mathlib that retrieves relevant theorems, outperforming GPT models and earning strong reception in the AI-for-math community. Together these efforts, our aim is to design a semantics-first LLM (large language model) that autoformalizes informal PDE problems into machine-checked specifications, synthesizes solver-ready code, and plans subgoals, closing the loop between formal analysis and LLM reasoning and surpassing human heuristics across diverse PDEs.