Workshop on AI and Reasoning

This workshop will bring together researchers at Chalmers and beyond to discuss new developments in AI and reasoning, such as large language models expanded with reasoning capabilities, and other methods for combining learning and reasoning.
<h2>Agenda</h2>
11.00 - 11.45 Mateja Jamnik: AI for Math: The Future of Collaborative Discovery &nbsp;(this is also a guest lecture in the Neuro-symbolic AI course - in room EC)
11.45 - 13.00 Lunch
All afternoon talks are in room EA: 13.00 - 13.30 Josef Urban: Some feedback loops in proving, guessing and learning&nbsp; 13.30 - 14.00 Vijay Ganesh: Auto-formalization via Joint Embeddings 14.00 - 14.30 Sidhartha Gadgil: Accuracy and Scaling for AI via Autoformalization
14.30 - 15.00 Fika&nbsp;
15.00 - 15.30 Natarjan Shankar: Title TBA 15.30 -16.00 Discussion on future directions in AI and reasoning

Mathematics is humanity’s most infinite frontier, and formalising and discovering new theorems has been painstakingly slow. Today, AI promises a paradigm shift. In this talk, I examine the technical breakthroughs AI brings to building an AI-human collaborative mathematician capable of genuine discovery. I discuss how human intuition and AI reasoning can work together to explore, conjecture, and solve mathematical problems. I then introduce AI methods that can extract informal human domain knowledge, formalise it, learn from it, tackle new problems, and rigorously verify solutions. I highlight how the scarcity of high-quality conjectures limits AI learning, and propose automated generation of progressively better conjectures to enhance AI reasoning. Ultimately, I argue that by centring the human in this partnership, we can build an AI-human mathematician that not only solves problems, but fundamentally expands how we explore and discover mathematics.

Human problem solvers often combine deductive reasoning and exploration with learning and pattern matching. In the recent years such combinations are also increasingly developed for building stronger automated theorem provers, SMT solvers and conjecturing and synthesis systems. The methods in this field include equipping the current deductive systems with efficient statistically learned guidance that controls the choice of the inference steps, using for example fast decision trees, graph neural networks, language models and their combinations. Learning and AI methods can also be used to automatically design new symbolic strategies for today’s ATPs and SMTs. This has the advantage of producing explainable ideas for steering the search space, which can be further taken up and modified by the systems' developers. I will also discuss several methods that try to directly synthesize reasoning objects such as instantiations and OEIS explanations, using various neural approaches. Perhaps the most interesting aspect of this research are the positive feedback loops between the proving, guessing and learning methods. I will show that some of them can today go quite far and create quite interesting solutions.

In recent years we have witnessed a symbiotic trend wherein LLMs are being combined with provers, solvers, and computer algebra systems, resulting in dramatic breakthroughs in AI for math. Following this trend, we have developed two lines of work in my research group. The first is the idea that "good" joint embeddings (JE) can dramatically improve the efficacy of LLM-based auto-formalization tools. We say that JEs are good if they respect the following invariant: semantically-equivalent formally-dissimilar objects (e.g., pairs of sematically-equivalent natural and formal language proofs) must be "close by" in the embedding space, and semantically inequivalent ones "far apart". We use such JE models as part of a successful RAG-based auto-formalization pipeline, demonstrating that such JEs are a critical AI-for-math technology. The second idea is Reinforcement Learning with Symbolic Feedback (RLSF), a class of techniques that addresses the LLM hallucination problem in contexts where we have access to rich symbolic feedback such math, physics, and code, demonstrating that they too are critical to the success of AI for math.&nbsp;
Brief Bio:
Dr. Vijay Ganesh is a professor of computer science at Georgia Tech and the associate director of the Institute for Data Engineering and Science (IDEaS), also at Georgia Tech. Additionally, he is a co-founder and steering committee member of the Centre for Mathematical AI at the Fields Institute, and an AI Fellow at the BSIA in Waterloo, Canada. Prior to joining Georgia Tech in 2023, Vijay was a professor at the University of Waterloo in Canada from 2012 to 2023, a co-director of the Waterloo AI Institute from 2021 to 2023, and a research scientist at the Massachusetts Institute of Technology from 2007 to 2012. Vijay completed his PhD in computer science from Stanford University in 2007.&nbsp; Vijay's primary area of research is the theory and practice of SAT/SMT solvers, and their application in AI, software engineering, security, mathematics, and physics. In this context he has led the development of many SAT/SMT solvers, most notably, STP, Z3str family of string solvers, AlphaZ3, MapleSAT, AlphaMapleSAT, and MathCheck. On the theoretical side, he works on topics in mathematical logic and proof complexity. More recently he has started working on AI problems that can be solved via combinations of automated reasoning and machine learning, notably the use of machine learning for efficient solvers and the use of solvers aimed at making AI more trustworthy, secure, and robust. For his research, Vijay has won over 35 awards, honors, and medals, including an ACM Impact Paper Award at ISSTA 2019, ACM Test of Time Award at CCS 2016, and a Ten-Year Most Influential Paper citation at DATE 2008.

AI systems have shown impressive capabilities in Mathematical reasoning, including a Gold medal score at the IMO, and have become genuinely helpful in mathematical research. However, they still have related limitations: Accuracy, Autonomy and Scalability. As mathematical proofs need to be completely correct, even a small chance of error in a step translates to a high chance of error in a large proof. This limits the possibility of systems working at length autonomously as all the work after the first error may have no value. This also limits scaling as human checking of proofs becomes the bottleneck. An approach we (and many other groups) are taking to mitigate these is to use a formal proof system to check proofs - the Lean Prover in our case, and to use Autoformalization to bridge between natural language and formal mathematics. We aim to facilitate both formalization in Lean and mathematicians working in no-code environments with AI and Lean used indirectly. Our tools are developed incrementally and are designed to be extensible, so that they should be of some use even at early stages and hopefully become more useful over time, ideally able to be fully autonomous eventually.&nbsp; I will discuss the design and implementation of these tools.

<h2>Location</h2>
EDIT building: <a rel="noopener" href="https://maps.chalmers.se/#ec631799-6bfa-4995-95e3-efe03c13ad70" target="_blank" title="Chalmers Maps" data-anchor="#ec631799-6bfa-4995-95e3-efe03c13ad70">Room EC</a> before lunch, then <a rel="noopener" href="https://maps.chalmers.se/#b9c89c7c-b553-488c-b09e-d2c41f5e6259" target="_blank" title="Chalmers Maps" data-anchor="#b9c89c7c-b553-488c-b09e-d2c41f5e6259">room EA</a>.

Chair rosa

Large Language Models for Mathematics and Software

Large language models, such as Chat-GPT, have demonstrated remarkable abilities to understand and generate human language. This theme explores their potential to contribute to mathematical reasoning and software creation, extending beyond traditional methods and potentially uncovering novel approaches and solutions.

Information and Communications technology

Data Science and AI 2

Chalmers Maps

Registration

Workshop

News

Calendar

Notifications

Chalmers researchers who can comment on the Nobel Prizes

Chalmers expertise relating to the war in Ukraine

Antimicrobial resistance (AMR)

Electro mobility

Find the expert

Press and media

Follow Chalmers on social media

A Big Congratulations to a Vigorous 120-Year-Old

Chalmers Annual Ceremony – A New Tradition

Chalmers’ stance of not allowing political manifestations on campus revoked

No political manifestations on Chalmers campus

Support due to the escalating conflict in the Middle East

”Chalmers condemns violence against students in Iran”

IVA's 100 list: 'Chalmers technology in the service of humanity'

War in Ukraine: "Democracy and free expression must be protected"

New battery investment demands cutting edge skills

Urgent to coordinate Sweden's e-infrastructure

International collaborations and academic freedom

Sweden needs independent universities and university colleges

Sweden’s system for research funding is defective

The aim of all our efforts

We are all deeply moved when senseless violence strikes a school environment

The STEM Strategy – A Welcome Initiative Where Chalmers Plays a Significant Role

Is there room for an even bolder research policy?

Reflections from a Rising India

The engineer is there where the future is shaped

Hard times for American universities affect us all

The Optimist Dalén, a Role Model in the Spirit of William Chalmers

Donations Can Provide Independence and Long-Term Strength

How Free Should a University Really Be?

The Electrification of Transport Is a Tidal Wave

Conversations That Make a Difference

President’s perspective: Three reforms for Chalmers and for Sweden

Vera Sandberg – the chalmerist who became Sweden’s first female engineer

“I truly could not have said it better myself”

President’s perspective

A great university

A great place to live

Meet some of your forerunners

Energy

Materials Science

Transport

Urban and regional environments

Health Engineering

Production

Information and Communication Technology

Nanoscience

Basic Science

Ocean

Space Technology

Our offer

Assistant professor positions

Verapodden

Architecture and Civil Engineering

Bachelor’s thesis Chemistry and Chemical Engineering

Chemistry and Chemical Engineering

Communication and Learning in Science

Computer Science and Engineering

Electrical Engineering

Industrial and Materials Science

Life Sciences

Mathematical Sciences

Mechanics and Maritime Sciences

Microtechnology and Nanoscience

Physics

Space, Earth and Environment

Technology Management and Economics

Presentation of master thesis

Team Smart Campus

Team Smart Uni

Team 10xIndividual

Team Data Exploit

Team Education

Team Upskill

Team AI-based feedback

Explorative AI projects 2025

In focus: antimicrobial resistance (AMR)

In focus: electro mobility

Subjects in focus

Current

Conferences

Choose subject

In order to play this video you must open your cookie settings and allow external media cookies.

In order to use basic functions like page navigation and access secure areas of the website, you must open your cookie settings and allow necessary cookies.

In order to use this service you must open your cookie settings and allow external services cookies.

To help us understand how visitors interact with the website you must open your cookie settings and allow statistics cookies.

Course syllabus for

Subject

Each academic year contains different courses

See programme page at universityadmissions.se

Educational area

Permissible substitutions of compulsory courses

To see your programme syllabus – select the academic year in which you started the programme.

[en: page.studyprogrammepage.syllabusesview.coursesdescription]

Current

AI for reasoning in formal mathematics

Overview

Agenda

Abstracts

Mateja Jamnik: AI for Math: The Future of Collaborative Discovery

Josef Urban: Some feedback loops in proving, guessing and learning

Vijay Ganesh: Auto-formalization via Joint Embeddings

Siddharta Gadgil: Accuracy and Scaling for AI via Autoformalization

Location

CHAIR Theme: Large Language Models for Mathematics and Software