Tuesday, December 16, 2025

2025-12-22 / 17:00 ~ 18:00

SAARC 세미나 - SAARC 세미나:

by 최우진(KAIST 명예교수님)

Our approach relies on input-convex neural networks (ICNNs) to discretize the JKO steps, which can be optimized by stochastic gradient descent. Unlike previous work, our method does not require domain discretization or particle simulation. As a result, we can sample from the measure at each time step of the diffusion and compute its probability density. We demonstrate our algorithm’s performance by computing diffusions following the Fokker-Planck equation and apply it to unnormalized density sampling as well as nonlinear filtering.

2025-12-22 / 15:00 ~ 16:00

학과 세미나/콜로퀴엄 - 응용수학 세미나: Rethinking Formal Mathematics: Towards Human-Oriented Theorem Proving and Autoformalization

by 임효재()

Theorem proving with large language models has recently gained substantial attention as a direction for developing trustworthy and verifiable AI reasoning. This talk gives a brief introduction to the proof assistant Lean, which provides the verification layer for formal theorem proving, and reviews recent trends in LLM-based theorem proving. These methods rely increasingly on natural-language descriptions of mathematical arguments, which brings renewed attention to the relationship between informal mathematical language and formal representations. I will discuss the gap between natural-language mathematical expressions and the formal representations, and explain why the high level of abstraction in existing formal structures can be a limitation for natural-language–driven methods. This motivates the need for more human-oriented forms of formalization. As one approach, I will present a rule-based method for autoformalization. This talk is based on the work done at the 2025 KIAS winter school on Mathematics and AI.

2025-12-16 / 16:30 ~ 17:30

IBS-KAIST 세미나 - 이산수학: Cliques in Paley graphs and cyclotomic graphs

by Chi Hoi Yip(Georgia Institute of Technology)

Given a prime power $q \equiv 1 \pmod 4$, the Paley graph of order $q$ is the graph defined over $\mathbb{F}_q$ (the finite field with $q$ elements), such that two vertices are adjacent if and only if their difference is a square in $\mathbb{F}_q$. In this talk, I will present some recent progress on the clique number of Paley graphs of non-square order, the characterization of maximum cliques in Paley graphs of square order, as well as their extensions to cyclotomic graphs. In particular, I will highlight a new proof of the Van Lint–MacWilliams’ conjecture using ideas from arithmetic combinatorics.

Events for the 취소된 행사 포함