Vellum
A Scalable Framework for AI-Aided Formal Reasoning
The Project
The Vellum project builds an open-source framework, where large language models (LLMs) act as planners and interface with multiple interactive theorem-provers (ITPs) and automated solvers, with a view to streamlining mathematical exploration and proving. By interfacing with diverse types of solvers and tools, Vellum facilitates large-scale, AI-aided formal reasoning, which in turn will simplify the automatic formalization of natural language statements and significantly lower the barriers to entry in mathematical reasoning research.
The Team
Swarat Chaudhuri is a Professor of Computer Science at UT Austin and a Research Scientist at Google Deepmind. His research brings together ideas from automated reasoning, machine learning, and programming languages with the goal of creating capable AI systems that are also reliable, transparent, and secure by construction. Dr. Chaudhuri received a bachelor's degree in computer science from the Indian Institute of Technology, Kharagpur, in 2001, and a doctoral degree in computer science from the University of Pennsylvania in 2007. He is a 2025 Guggenheim Fellow and has received an NSF CAREER award, the ACM SIGPLAN John Reynolds Dissertation award, the Morris and Dorothy Rubinoff Dissertation award from the University of Pennsylvania, Meta and Google Research awards, and several ACM SIGPLAN and SIGSOFT distinguished paper awards. Dr. Chaudhuri has served on the program committees of all the main conferences in machine learning, formal methods, and programming languages and was a Program Chair for CAV 2016 and ICLR 2024.
Dawn Song is a Professor in Computer Science at UC Berkeley and Co-Director of Berkeley Center for Responsible Decentralized Intelligence. Her research interest lies in AI and deep learning, security and privacy, and decentralization technology. She is the recipient of various awards including the MacArthur Fellowship, the Guggenheim Fellowship, the NSF CAREER Award, the Alfred P. Sloan Research Fellowship, the MIT Technology Review TR-35 Award, ACM SIGSAC Outstanding Innovation Award, and more than 10 Test-of-Time Awards and Best Paper Awards from top conferences in Computer Security and Deep Learning. She has been recognized as Most Influential Scholar (AMiner Award), for being the most cited scholar in computer security. She is an ACM Fellow and an IEEE Fellow. She is an Elected Member of American Academy of Arts and Sciences. She obtained her Ph.D. degree from UC Berkeley. She is also a serial entrepreneur and has been named on the Female Founder 100 List by Inc. and Wired25 List of Innovators.
Jingxuan He is a Postdoctoral Researcher at UC Berkeley. His research broadly spans computer security, machine learning, and programming languages, with a recent focus on enhancing the safety and reliability of AI-generated software programs. He earned his Ph.D. from ETH Zurich, where he received the ETH medal for outstanding doctoral thesis. He was also a recipient of the ACM CCS 2023 distinguished paper award.
Zhe Ye is a PhD student at UC Berkeley and Berkeley RDI. His research interests include LLM assisted formal verification, formal specification synthesis, and computer security. He has authored various papers in relevant areas, some of which have been accepted by top-tier conferences like IEEE S&P and ISSTA.
Amitayush Thakur is a Ph.D. student at UT Austin, working at the intersection of “AI for Mathematics” and “AI for Code”. He is interested in automated mathematical reasoning through LLMs and its implication in fully verified program synthesis essential for generating industry-grade code from AI. He is the lead creator of Copra, an agentic framework for formal theorem-proving. Before joining UT, he worked as Software Engineer at Microsoft, and before that as a research intern at Microsoft Research.
George Tsoukalas is a PhD student at UT Austin, working on research in neurosymbolic techniques for automated mathematical reasoning and program synthesis. He led the creation of PutnamBench, a frontier AI-for-math benchmark that received a Best Paper award at the ICML 2024 AI for Math Workshop. He also contributed to COPRA, an agentic LLM-based approach for formal theorem-proving.