AI4Math: Neuro-Symbolic Integration for Mathematical Discovery and Reasoning (AI4Math 2026)
Aim and Scope
Objectives:
In the era of Large Language Models (LLMs), the boundary between human-like “intuition” and machine-like “rigor” is blurring. While LLMs excel at generating plausible mathematical ideas, they often struggle with long-term logical consistency and formal correctness. This special session aims to provide a forum for researchers to discuss the synergy between Neural Intuition (probabilistic generation) and Symbolic Logic (formal verification and algorithmic computation). Our goal is to foster the development of “Mathematical Super Intelligence” capable of discovering new theorems, automating the formalization of mathematical knowledge, and solving complex problems in both pure mathematics and physical modeling.
Key Topics include, but are not limited to:
- Neuro-Symbolic Synthesis: Hybrid models combining LLMs with Theorem Provers (Lean 4, Coq) and Computer Algebra Systems (CAS).
- Verification / Formalization: Techniques for converting informal scientific text into formal, machine-verifiable code.
- Mathematical NLP: Disambiguation of identifiers, semantic parsing, and high-quality scientific data curation.
- Knowledge Representation: Constructing dependency and citation graphs of mathematical concepts for formal repositories.
- Discovery and Conjecturing: Automated generation of mathematical conjectures and verification of unsolved problems (e.g., Erdős problems).
- Mathematics for AI: Mathematical and logical methods for AI reliability, formal verification of neural networks, and mathematical foundations for agent-to-agent communication and protocol synthesis.
Timeliness and Uniqueness
As of 2026, global interest in “AI for Science” and “AI for Math” has reached a peak, evidenced by significant breakthroughs in mathematical reasoning by major AI labs. However, many challenges remain in formalizing “intuition” and integrating symbolic tools seamlessly into modern AI workflows. This session is unique in its focus on Neuro-Symbolic integration and its roots in Japan’s historical strength in symbolic processing and mathematical education. By bringing together experts from NLP, formal logic, and computer algebra, we provide a vital bridge to the international audience at KSE 2026 in Kanazawa.
Submission Guideline
https://kse2026.kse-conferences.org/call-for-papers/
Session Organizers
Masaya Taniguchi (Lead Organizer)
- Email: masaya.taniguchi@riken.jp
- Affiliation: JSPS Postdoctoral Fellow (PD), Explainable AI Team, RIKEN Center for Advanced Intelligence Project (AIP)
- Biography: Received his Ph.D. in Information Science from JAIST. His research focuses on mathematical logic, formal language theory, and the intersection of NLP and interactive theorem proving. He is currently a JSPS Research Fellow (PD) at RIKEN AIP.
Akiko Aizawa
- Email: aizawa@nii.ac.jp
- Affiliation: Professor, National Institute of Informatics (NII) / The University of Tokyo
- Biography: A prominent leader in the field of Natural Language Processing and Information Retrieval. She has spearheaded numerous projects on structural analysis of academic documents and mathematical expressions.
Hitomi Yanaka
- Email: hyanaka@is.s.u-tokyo.ac.jp
- Affiliation: Associate Professor, Graduate School of Information Science and Technology, The University of Tokyo / Team Director, RIKEN AIP
- Biography: An expert in Natural Language Inference and Explainable AI. She leads the XAI team at RIKEN AIP, focusing on the logical capabilities of deep learning models and their application to formal reasoning.
Sho Sonoda
- Email: sho.sonoda@riken.jp
- Affiliation: Senior Researcher, RIKEN Center for Advanced Intelligence Project (AIP)
- Biography: An expert in the theory of deep learning. Further, He leads the AI Mathematician project in the AutoRes project, which focuses on the formalization of mathematics using Lean 4 and LLMs to accelerate scientific discovery.
Takuya Matsuzaki
- Email: matuzaki@rs.tus.ac.jp
- Affiliation: Professor, Faculty of Science Division I, Tokyo University of Science
- Biography: A pioneer in Mathematical NLP, known for his leadership in the “Todai Robot Project” (Can an AI get into the University of Tokyo?), specifically in the automated solving of university entrance exam math problems.
Takuto Asakura
- Email: takuto@is.s.u-tokyo.ac.jp
- Affiliation: Assistant Professor, Graduate School of Information Science and Technology, The University of Tokyo
- Biography: Specializes in the analysis of mathematical expressions and the digital preservation/formalization of diverse mathematical resources, including on-the-fly notation definition analysis.