Welcome to
AI for Math Workshop @ ICML 2024
https://icml.cc/virtual/2024/workshop/29948
July 26th, 2024 @ Vienna, Austria (Hybrid).
WORKSHOP SUMMARY
Mathematical reasoning is one of the most advanced forms of human intelligence. Humans develop formal languages for rigorously describing mathematical problems and deriving mathematical knowledge. The machine learning community has endeavored to develop neural models with mathematical reasoning capabilities as humans. On the other hand, a shared vision in the community is that the models collaborate with humans for mathematical discoveries.
The goal of this workshop is to bring together researchers working on various domains to discuss the progress and the future of applying AI technologies to mathematics. As mathematics is fundamental for almost all modern sciences (including computer science), a vast range of related topics are also within our scope. To this end, this workshop focuses on several crucial yet underexplored problems. Specifically, we are expecting attendants from various backgrounds, institutions, and disciplines to discuss areas related to the following:
Autoformalization and reversed auto-informalization: How can we develop methods that improve the precision of the autoformalization process from natural language proof to formal proof, and as a dual process describing a formal proof in natural language?
Automated theorem proving: How do build consistent theorem proving? How do we relieve or solve the intermediate step errors in proving?
Automated theorem generation: Can neural models generate new and practically valid theorems? How do we take full advantage of such generated new theorems?
Code augmentation and auxiliary for mathematical reasoning: How can the handy and plentiful code data facilitate the models to conduct mathematical reasoning?
Formal verification and code generation: How can progress made in AI for Math help or be directly deployed to the field of formal verification? What are the common technical difficulties? How can AI systems be able to write provably correct code, given any (formal) specifications?
In addition to the problem areas above, we also welcome research work related to the following topics:
Measurement: How do we measure autoformalization?
Reasoning in related areas: neurosymbolic reasoning, program synthesis, logical reasoning.
Applications: Applying mathematical reasoning techniques to sciences, finance, education, etc.
Our workshop also includes three innovative challenges for related mathematical reasoning problems:
Challenge/Track 1: Autoformalization.
Challenge/Track 2: Automated theorem generation and proving.
Challenge/Track 3: Automated optimization problem-solving with code.
GLOBAL CHALLENGE ON AUTOMATED MATH REASONING
We publish three Challenges and invite researchers and practitioners around the world to investigate automated mathematical reasoning with the aid of formal language via large language model approaches. Please check the details on the Challenge page.
PROGRAM SCHEDULE
8:55-9:00 Opening Remarks
9:00-9:30 Invited Talk
9:30-10:00 Invited Talk
10:00-10:30 Invited Talk
10:30-11:00 Coffee Break
11:00-11:30 Poster Session (I)
11:30-12:00 Invited Talk
12:00-12:30 Invited Talk
12:30-13:00 Invited Talk
13:00-14:00 Lunch Break
14:00-14:45 Contributed Talks
14:45-15:15 Invited Talk
15:15-15:45 Invited Talk
15:45-16:30 Discussion Panel
16:30-17:00 Poster Session (II)
17:00-17:05 Closing Remarks
INVITED SPEAKERS & PANELISTS
Anima Anandkumar is Bren Professor at Caltech and Senior Director of AI Research at NVIDIA. She received her B.Tech from the Indian Institute of Technology Madras, and her Ph.D. from Cornell University. She did her postdoctoral research at MIT and an assistant professorship at the University of California Irvine. She has received several honors such as the IEEE fellowship, Alfred. P. Sloan Fellowship, NSF Career Award, and Faculty Fellowships from Microsoft, Google, Facebook, and Adobe. She is part of the World Economic Forum's Expert Network.
Kun Zhang is the Acting Chair of Machine Learning, Professor of Machine Learning, and Director of Center for Integrative Artificial Intelligence (CIAI). Zhang’s research interests lie in machine learning and artificial intelligence, especially in causal discovery and inference, causal representation learning, and machine learning under data heterogeneity. He aims to make causal learning and reasoning transparent in science, AI systems, and human society. On the application side, he is interested in biology, neuroscience, computer vision, computational finance, and climate analysis. His research has been motivated by real problems in healthcare, biology, neuroscience, computer vision, computational finance, and climate analysis.
M. Pawan Kumar is a research scientist at DeepMind. Prior to that, he was a faculty member in the Department of Engineering Science at the University of Oxford during 2015 – 2021, where he led the OVAL group which focused on the design and analysis of optimization algorithms for problems arising in computer vision and machine learning. During 2012 – 2015, he was a faculty member in the Center for Visual Computing at Ecole Centrale Paris.
Swarat Chaudhuri is a Professor of Computer Science and the director of the Trishul laboratory at UT Austin. His research lies at the interface of programming languages, formal methods, and machine learning. His aim as a researcher is to develop a new class of intelligent systems that are reliable, transparent, and secure by construction and can solve reasoning-intensive tasks beyond the scope of contemporary AI. He has received the 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.
Wenda Li is a lecturer in hybrid AI at the University of Edinburgh and a visiting research fellow at the University of Cambridge. Prior to this, I was a research associate and a PhD student working with Prof. Larry Paulson at the University of Cambridge. His research interests include machine learning for theorem proving, interactive theorem proving, verified symbolic computing, and mechanised mathematics.
Yilun Zhou currently works at Salesforce as a research scientist. He finished his Ph.D. degree at MIT Department of Electrical Engineering and Computer Science (EECS) working on model transparency and interpretability advised by Prof. Julie Shah. His long-term research goal is to enable trustworthy and responsible machine learning, and his recent research explores LLM-generated free-text self-explanations, their mathematical reasoning abilities, as well as evaluations, utilities and societal implications of model explanations in general.
Piotr Miłoś is an associate professor in the Polish Academy of Sciences and University of Warsaw, a team leader at Ideas Ncbr and a member of the ELLIS Society. He is interested in methods that can deliver robust decision-making capabilities in complex scenarios.
Albert Q. Jiang is a PhD student at the Cambridge Computer Laboratory, supervised by Professor Mateja Jamnik and Professor Wenda Li. He also part-time at Mistral AI. I’m a contributor to Mistral-7B-v0.1 and Mixtral-8x7B-v0.1. He studies how to learn abstract mathematical reasoning, with large (>20B) and small (<1B) language models.
WORKSHOP ORGANIZERS
Postdoctoral researcher at City University of Hong Kong
Associate professor at Sun Yat-sen University/MBZUAI
Research scientist at Huawei Noah's Ark Lab
Ph.D. candidate at UCLA
Assistant professor at Carnegie Mellon University
Professor at University Paris-Saclay; Director of research at Google Brain
Professor at Ecole des Ponts Paristech
Professor at Peking University
Postdoctoral researcher at the University of Oxford
Professor at the University of Cambridge
Principal researcher at Huawei Noah's Ark Lab
Associate professor at City University of Hong Kong
Wei Shi
Research scientist at Huawei Noah's Ark Lab
Xiongwei Han
Research scientist at Huawei Noah's Ark Lab