Date/Time : 28 Apr 2025 14:00
Venue : S17 #04-04 (SR3)
Speaker : Huajian Xin, University of Edinburgh

Large language models (LLMs) excel at information retrieval, knowledge memorization, and reasoning, yet they face challenges in domains with scarce data and long-tail distributions, such as formal mathematical theorem proving. In this domain, LLMs must generate rigorous, verifiable proof scripts for interactive theorem-proving systems. Challenges stem from limited natural-language corpora, the demand for logical precision, and strict accuracy requirements. In developing DeepSeek-Prover V1, we automated large-scale translation of natural-language mathematical problems into formal propositions and synthesized corresponding proofs. After rigorous multi-level filtering, fine-tuning on this dataset achieved state-of-the-art results, effectively distilling knowledge from data-rich to data-scarce parallel domains. DeepSeek-Prover V1.5 further introduced automatic annotation of chain-of-thought reasoning within proof code data, enabling smaller models to adopt explicit reasoning strategies that significantly improve long-reasoning tasks. This talk will also introduce formal mathematical theorem proving as an ideal benchmark for evaluating and training language models’ capabilities in rigorous reasoning.

Add to calendar :

Date/Time : 28 Apr 2025 15:00
Venue : S17 #04-05 (SR2)
Speaker : Lin, Youzuo, University of North Carolina at Chapel Hill

Computational Wave Imaging (CWI) enables the reconstruction of hidden structures and the estimation of physical properties within a medium by analyzing propagating wave signals. This technique has critical applications in fields such as seismic exploration of the Earth’s subsurface and ultrasound computed tomography in medical imaging. Traditional approaches to CWI are broadly categorized into physics-based methods and machine learning-based techniques. Physics-based methods deliver high-resolution, quantitatively accurate reconstructions of acoustic properties but are often computationally intensive and susceptible to issues of ill-posedness and nonconvexity. In contrast, machine learning approaches, particularly those leveraging deep learning, have recently emerged as powerful tools to address these challenges by offering faster, data-driven solutions. In this presentation, we introduce our recent advancements in hybrid CWI methodologies that combine fundamental wave physics with state-of-the-art machine learning techniques. We focus on the development of self-supervised learning strategies that significantly reduce computational costs while maintaining accuracy. We will demonstrate the effectiveness of these approaches through applications in subsurface geophysics and medical ultrasound imaging, highlighting their potential for broad, real-world impact.

Add to calendar :

Date/Time : 25 Apr 2025 16:00
Venue : S17 #04-04 (SR3)
Speaker : Youngjoon Hong, Seoul National University

We propose a novel approach for solving parametric partial differential equations (PDEs) using an operator network. This method combines the strengths of deep learning with traditional numerical techniques, specifically the finite element or spectral element methods, to address parametric PDEs ranging from singularly perturbed convection-diffusion equations to the Navier-Stokes equations, all without requiring paired input-output training data. Through extensive experiments on various benchmark problems, our approach has demonstrated excellent performance across diverse settings, showcasing its versatility in terms of accuracy, generalization, and computational efficiency. The proposed framework holds significant potential for applications in fields where PDEs are critical for modeling complex domains with diverse boundary conditions and singular behavior. Additionally, we provide a rigorous theoretical convergence analysis, grounded in numerical analysis, to further support our approach.

Add to calendar :

Date/Time : 25 Apr 2025 14:00
Venue : S17 #04-04 (SR3)
Speaker : Xu Tianyi, Peking University (BICMR)

This talk explores the latest developments and emerging trends in the application of AI to mathematics, focusing on leveraging generative models for writing formalized mathematical proofs. We will introduce the idea of formalizing mathematics using proof assistants—computer programs designed to verify the correctness of mathematical proofs. We will then compare various approaches to formalization, highlighting the unique advantages of using large language models (LLMs) for this task. Additionally, we will address key challenges that naturally arise in this process and present our strategies for overcoming them.

Add to calendar :

Date/Time : 24 Apr 2025 16:00
Venue : S17 #06-11 (SR6)
Speaker : John Harlim, Penn State University

In this talk, I will present two recent topics on learning vector fields of dynamical systems. For the first part, I will discuss the problem of learning vector fields of dynamical systems that lie on a Riemannian submanifold of R^n, with applications ranging from dissipative dynamics that exhibit inertial manifold structure to differential equations with algebraic constraints. I will present an operator-valued kernel constructed by geometrical constraints estimated from the time series and an ODE solver that guarantees the prediction to lie on the manifold in the limit of large data. I will demonstrate the numerical methods on various examples of various ambient dimensions of order 1 to order $10^4$ and compare them to existing neural network approaches. For the second part, I will discuss the problem of learning coarse-grained dynamics on graphs with Graph Neural Network. We systematically determine the GNN architecture by inspecting how the leading term of the Mori-Zwanzig memory term depends on the coarse-grained interaction coefficients that encode the graph topology. I will present numerical demonstrations on two examples, a heterogeneous Kuramoto oscillator model and a power system, which shows that the proposed GNN architecture can predict the coarse-grained dynamics under fixed and time-varying graph topologies.

Add to calendar :

Date/Time : 23 Apr 2025 15:00
Venue : S17 #04-05 (SR2)
Speaker : Jialun Li, Ecole Polytechnique de Paris

I will begin with the classical setting of the modular surface: the unit tangent bundle of the modular curve T^1(SL(2,Z)\H)=SL(2,Z)\SL(2,R), where periodic geodesics correspond to periodic orbits of the diagonal subgroup. Margulis and Bowen established dynamical frameworks for studying these orbits, while Selberg and Sarnak developed spectral and number-theoretic approaches.

We then turn to the higher-rank generalization, periodic diagonal orbits on SL(3,Z)\SL(3,R). In this case, each periodic diagonal orbit is a two-dimensional flat torus embedded in the space. Different counting problems emerge, depending on how one orders these tori–whether by dynamical ordering, geometric ordering or arithmetic ordering. The dynamical and geometric ordering are closely connected through the shapes of the flat tori. Finally, I will discuss my recent joint work with Thi Dang and Nihar Gargava on the density of shapes of periodic tori.

Add to calendar :

Date/Time : 23 Apr 2025 16:30
Venue : S17 #04-05 (SR2)
Speaker : Li Yifei, University of Tübingen

In this talk, I introduce a Sobolev-like space of order $3/2$, denoted as $\widehat{H}^{3/2}$, for Lagrangian finite elements, especially for $C^0$ elements. It is motivated by the limitations of current stability analysis of the evolving surface finite element method (ESFEM), which relies exclusively on energy estimate frameworks. When establishing a PDE-based analysis framework for ESFEM, we encounter a fundamental regularity mismatch: the ESFEM employs $C^0$ elements, while PDE regularity theory requires $H^{3/2}$ regularity for solutions. Our $\widehat{H}^{3/2}$ space resolves this challenge by demonstrating compatibility with elliptic PDE regularity theory, trace inequalities, and inverse inequalities. Notably, we extend the domain deformation estimates in ESFEM to the $\widehat{H}^{3/2}$ setting, thereby providing a rigorous foundation for PDE-based convergence analysis of ESFEM. The talk concludes with applications of the $\widehat{H}^{3/2}$ theory to numerical analysis for a coupled bulk-surface problem.

Add to calendar :

Date/Time : 23 Apr 2025 15:00
Venue : S16 #05-17 (ACTIVE LEARNING ROOM 1)
Speaker : Jared P. Whitehead, Brigham Young University

In classical statistics, predictive error is understood as a trade-off between the bias and the variance that balances model simplicity with its ability to fit complex functions. However, over-parameterized models exhibit counterintuitive behaviors, such as “double descent” in which models of increasing complexity exhibit decreasing generalization error. Others may exhibit more complicated patterns of predictive error with multiple peaks and valleys. Neither double descent nor multiple descent phenomena are well explained by the bias-variance decomposition.

We introduce a novel decomposition that we call the generalized aliasing decomposition (GAD) to explain the relationship between predictive performance and model complexity. The GAD decomposes the predictive error into three parts: 1) model insufficiency, which dominates when the number of parameters is much smaller than the number of data points, 2) data insufficiency, which dominates when the number of parameters is much greater than the number of data points, and 3) generalized aliasing, which dominates between these two extremes.

We demonstrate the applicability of the GAD to diverse applications, showing that it accurately captures the non-monotonic nature of generalization curves in several different settings. GAD can be explicitly calculated from the relationship between model class and samples without seeing any data labels, so that this decomposition can answer questions related to experimental design and model selection before collecting data or performing experiments.

Add to calendar :

Date/Time : 23 Apr 2025 15:00
Venue : S17 #04-04 (SR3)
Speaker : Luca Spolaor, University of California San Diego

I will discuss the boundary regularity for minimizers of the so-called Alt-Caffarelli problem and how it is related to a boundary unique continuation problem. This is joint work with L. Ferreri (SNS) and Bozhidar Velichkov (Pisa).

Add to calendar :