Abstract: We will explore the potential for AI to accelerate mathematical research in various phases, except for experimental mathematics. This talk will include considering the accessibility and functionality of proof assistants, and discussing insights from Tim Gowers, Terence Tao, and others. We should also be able to look at some concrete examples. There will be time at the end for discussion.
Abstract: Scientific modeling and computation traditionally rely on structured mathematics and hand-designed algorithms. In this talk, I propose a new perspective: treating both modeling and computation as processes operating within the space of natural language. I will introduce two complementary approaches that realize this vision. The first uses symbolic learning based on tree structures to generate mathematical expressions, where modeling is performed by constructing symbolic trees and computation is governed by operator rules. The Finite Expression Method (FEX) exemplifies this approach by discovering interpretable, high-accuracy solutions to PDEs and physical systems. The second approach employs large language models (LLMs) for automatic code generation and reasoning to translate scientific problem descriptions into formal mathematical models and executable solvers to solve these problems. As an example, the OptimAI framework demonstrates how multi-agent LLM collaboration enables reliable end-to-end optimization problem modeling and solving. Together, these methods point toward a unified paradigm where symbolic and language models form the foundation for interpretable, scalable scientific discovery and computation.
Abstract: We will schedule two 20-minute talks per meeting to stay focused. The seminar will broaden its scope within AI and math, including concrete investigations, reporting on the state of the field's progress, history, philosophy, language, and even preparing for quals.
Abstract: Two 20 minute talks. The lack of creativity seen in ChatGPT is not due to the nature of AIs. Game-playing AIs like AlphaZero have an architecture that promotes creativity.
Abstract: Genomic sequences can be viewed not just as strings of nucleotides, but as objects with structure that can be learned from data. In this talk, we will explore how ideas from language modeling are being applied to genomes, with splice-site prediction as a concrete example.
The second talk is about measuring intelligence with ideas from AIT. Measuring intelligence for general AI is not simple. One approach is based on Algorithmic Information Theory, a set of ideas from the early days of AI, introduced by Ray Solomonoff (1960s) and developed for modern AI by Marcus Hutter (Google/Deep Mind). We will try to make it simple.
Abstract: Two 20 minute talks. The first talk is AI in Physics.
Our UMD physics department is currently discussing the impact and use of AI/LLMs in research and coursework. I will reflect on my own uses, discussions with students in my courses this past year, and discussions in the faculty committee devoted to this topic.
Abstract: Two 20 minute talks. The first is from P Resnik
Title: Large Language Models are Biased Because They are Large Language Models
I argue that harmful biases are an inevitable consequence arising from the design of any large language model as LLMs are currently formulated, all the way down to their mathematical formulation. To the extent that this is true, it suggests that the problem of harmful bias cannot be properly addressed without a serious reconsideration of AI driven by LLMs, going back to the foundational assumptions underlying their design. here are links to the relevant paper and to a short video. https://www.google.com/url?q=https://direct.mit.edu/coli/article/51/3/885/128621/Large-Language-Models-Are-Biased-Because-They-Are&sa=D&source=calendar&ust=1776713805261960&usg=AOvVaw2to4d8XjzLVNmr_IAi_3Ax
The second is from Maria Molina
Learning Without Labels: New Insights into Climate and Extremes
Abstract: Climate variability and weather extremes pose profound challenges for prediction, preparedness, and resilience. Traditional approaches often rely on predefined indices or supervised learning methods, which can overlook unexpected patterns or reinforce biases inherent in labeled datasets. This seminar explores how unsupervised learning techniques can uncover hidden patterns in high-dimensional climate data. I will highlight recent innovations that adapt established methods to reveal properties not captured by conventional architectures, offering new perspectives on modes of variability and extreme events. For instance, a knowledge-guided autoencoder can disentangle distinct Pacific climate modes with differing spectral signatures, while a custom hyperparameter search can optimize self-organizing maps to produce smooth, interpretable pathways among weather regimes. Together, these advances help uncover processes and mechanisms that may underlie established climate and weather phenomena. Ultimately, unsupervised learning provides a powerful lens for scientific discovery, with implications for understanding, prediction, and decision-making in a changing climate.
Abstract: Two 20 minute talks. The first is from Chris Metzler
A machine learning based approach to phase retrieval, with applications to seeing through and around obstacles.
The second talk is from Krishna Bodla
Title: "MCTS-Guided Test-Time Scaling for Verifiable Mathematical Reasoning"
Abstract: "Large language models (LLMs) have demonstrated impressive performance on isolated mathematical problems, yet they remain brittle on multi-step, olympiad-level reasoning tasks where an early error propagates irrecoverably through the entire solution chain. We propose a Monte Carlo Tree Search (MCTS) framework that reframes formal mathematical proof search as an iterative, self-correcting process operating entirely at test time requiring no additional model training or reinforcement learning fine-tuning. Our system uses an LLM to decompose the current proof state into a focused sub-goal one step at a time, treats each decomposition as a tree node, and employs a dual reward signal combining a critic LLM (process reward) with the Lean~4 formal verifier (outcome reward) to score and backpropagate node quality. An adaptive temperature schedule encourages diverse exploration early and focused exploitation as the search deepens. We benchmark this pipeline on MiniF2F, PutnamBench, and MathOlympiadBench using five prover models at 7B--32B scale."
4176 Campus Drive - William E. Kirwan Hall
College Park, MD 20742-4015
P: 301.405.5047 | F: 301.314.0827