Math & Computer セミナー
6 イベント
-
セミナー
Median-based estimators for randomized quasi-Monte Carlo integration
2026年1月9日(金) 15:00 - 17:00
鈴木 航介 (山形大学 准教授)
High-dimensional numerical integration is a ubiquitous challenge across various fields, from mathematical finance to computational physics and Bayesian statistics. While standard Monte Carlo (MC) methods are robust, their probabilistic error convergence rate of $O(N^{-1/2})$ is often insufficient for demanding applications. In this talk, I will introduce Quasi-Monte Carlo (QMC) and Randomized QMC (RQMC) methods, which offer a powerful framework for accelerating integration using low-discrepancy point sets. A key advantage of this deterministic approach is its ability to achieve a convergence rate of $O(N^{-1+\epsilon})$, significantly outperforming the standard MC rate. The second part of the talk will focus on the construction of point sets, specifically lattice rules and digital nets. I will explain how these methods achieve higher-order convergence rates, faster than $O(N^{-1})$, for sufficiently smooth integrands. I will also discuss their randomized variants and demonstrate how RQMC with mean-based estimators provides practical error estimation while maintaining high-order convergence. Finally, I will discuss recent progress in RQMC involving median-based estimators. I will highlight how these estimators achieve almost optimal convergence rates for various function spaces without requiring prior knowledge of the integrand.
会場: セミナー室 (359号室) 3階 359号室とZoomのハイブリッド開催
イベント公式言語: 英語
-
セミナー
Rational function semifields of dimension one
2025年11月7日(金) 13:30 - 15:30
宋 珠愛 (九州大学 大学院数理学研究院 助教)
Recently some researchers gave many studies toward algebro-geometric foundation for tropical geometry. I focused on rational function semifields of tropical curves and characterized them. With this characterization, in this talk, I suggest a definition of ``rational function semifield of dimension one". This definition can write out weight in the term of $\boldsymbol{T}$-algebra homomorphism, and can write balancing condition together with harmonic functions, where both weight and balancing condition are fundamental concepts for tropical varieties and $\boldsymbol{T}$ is the tropical semifield $(\boldsymbol{R} \cup \{-\infty\}, \operatorname{max}, +)$.
会場: セミナー室 (359号室) / via Zoom
イベント公式言語: 日本語
-
セミナー
Introduction to Lean theorem prover
2025年10月31日(金) 14:00 - 17:00
水野 勇磨 (Postdoctoral Researcher, University College Cork, Ireland)
A theorem prover is a tool for the formalization of mathematics, that is, for rigorously expressing and verifying theorems and proofs on a computer. In recent years, the Lean theorem prover has seen progress in the formalization of a wide range of areas of mathematics. In this talk, I will explain formalization of mathematics in Lean from the basics and survey the formalized results achieved to date.
会場: via Zoom / セミナー室 (359号室) 3階 359号室
イベント公式言語: 英語
-
セミナー
Computer Algebra with Deep Learning
2025年9月5日(金) 15:00 - 17:00
石原 侑樹 (日本大学 理工学部 数学科 助教)
Computer algebra is a field that aims to perform various mathematical calculations on computers. In recent years, there has been a surge in efforts to accelerate computer algebra algorithms using deep learning models such as “Transformer,” which is used in ChatGPT. In this lecture, I will introduce the results of joint research with Professor Kera et al. on learning Gröbner bases with Transformer.
会場: via Zoom / セミナー室 (359号室) 3階 359号室
イベント公式言語: 英語
-
セミナー
LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
2025年8月1日(金) 16:00 - 18:00
恩田 直登 (Project Research Engineer, Research Administrative Division, Omron Sinic X Corporation)
We introduce LeanConjecturer, a pipeline for automatically generating university-level mathematical conjectures in Lean 4 using Large Language Models (LLMs). Our hybrid approach combines rule-based context extraction with LLM-based theorem statement generation, addressing the data scarcity challenge in formal theorem proving. Through iterative generation and evaluation, LeanConjecturer produced 12,289 conjectures from 40 Mathlib seed files, with 3,776 identified as syntactically valid and non-trivial, that is, cannot be proven by aesop tactic. We demonstrate the utility of these generated conjectures for reinforcement learning through Group Relative Policy Optimization (GRPO), showing that targeted training on domain-specific conjectures can enhance theorem proving capabilities. Our approach generates 103.25 novel conjectures per seed file on average, providing a scalable solution for creating training data for theorem proving systems. Our system successfully verified several non-trivial theorems in topology, including properties of semi-open, alpha-open, and pre-open sets, demonstrating its potential for mathematical discovery beyond simple variations of existing results.
会場: via Zoom / セミナー室 (359号室) 3階 359号室
イベント公式言語: 英語
-
セミナー
Quantum Computing Algorithms and Institute of Mathematics-for-Industry
2025年7月3日(木) 15:30 - 17:00
落合 啓之 (九州大学 マス・フォア・インダストリ研究所 教授)
This is the kickoff talk of the Kyushu University Collaboration Team, which aims to foster communication between iTHEMS and IMI. I will introduce some of IMI's activities and organization, as well as my own work, including research on quantum algorithms that began with the launch of the Quantum Computing System Center in 2022.
会場: 研究本館 3階 345-347室
イベント公式言語: 英語
6 イベント