Abstract: Recent progress in Large Language Models (LLMs) has transformed text and code generation, yet models still falter on scientific reasoning where correctness, constraints, and physical consequences are critical. This talk explores how formal LLM reasoning can advance symbolic scientific modeling. First, our PDE-Controller formalizes informal PDEs (Partial Differential Equations), synthesizes solver-ready code, and plans subgoals to tackle nonconvex control via interactions with external solvers. Second, our Lean Finder accelerates scientific formalization via a semantics-aware search engine for Lean/Mathlib that retrieves relevant theorems, outperforming GPT models and gaining significant traction in the AI-for-math community. Through these efforts, we aim to design a semantics-first LLM that autoformalizes informal scientific problems into machine-checked specifications and synthesizes solver-ready code. This closes the loop between formal analysis and LLM reasoning, ultimately surpassing human heuristics for scientific discovery.
Bio: Dr. Wuyang Chen is a tenure-track Assistant Professor in Computing Science at Simon Fraser University. He is also a visiting research scientist at Microsoft. Previously, he was a postdoctoral researcher in Statistics at the University of California, Berkeley, advised by Professor Michael Mahoney. He obtained his Ph.D. in Electrical and Computer Engineering from the University of Texas at Austin in 2023, advised by Professor Atlas Wang. Dr. Chen's research focuses on integrating AI methods with physical knowledge, scientific machine learning, and theoretical understanding of deep networks. Dr. Chen has published papers at CVPR, ECCV, ICLR, ICML, NeurIPS, and other top conferences. Dr. Chen's research has been recognized by the US NSF newsletter, two Doctoral Dissertation Awards from INNS and iSchools, AAAI New Faculty Highlights, and NVIDIA Academic Grant Award. Dr. Chen also hosted and co-organized many conference workshops at NeurIPS, ICLR, CVPR.
Location: NCS 120