The Bekki Laboratory conducts research spanning three fields known as mathematical linguistics, theoretical linguistics, and computational linguistics. All three are natural sciences concerned with human language, and they use mathematical models to elucidate the structure of natural language (the structure that mediates between sound and meaning). The field that studies the mathematical properties of theories is called mathematical linguistics, the field that studies the empirical consequences and verification of theories is called theoretical linguistics, and the field that studies the computational properties of theories through implementation is called computational linguistics. The Bekki Laboratory mainly employs theoretical frameworks such as Combinatory Categorial Grammar (CCG), Dependent Type Semantics (DTS), and Neural Language Models to pursue theories that explain various linguistic phenomena in a unified manner, and to investigate the structure of the human language faculty that underlies them.
While the practical application of LLMs faces challenges in verification and improvement, this research proposes a solution mediated by a linguistic pipeline (LP). First, we explore the performance ceiling of both LLMs and LPs in natural language understanding. Second, we create a feedback loop in which an LP operable by experts in the language sciences verifies the validity of LLM reasoning and improves LLMs by providing reward models. Development and operation are undertaken through collaboration among language science specialists.
Using Dependent Type Semantics (DTS), a theory of natural language meaning based on dependent type theory, this project aims to establish a method for analyzing diverse linguistic phenomena from a broad perspective and automatically verifying the validity of those analyses through implementation. DTS enables the simultaneous satisfaction of the dynamics and compositionality of meaning, which had been a long-standing challenge. In implementation, we combine a Japanese CCG parser, an automated theorem prover, and the semantic test suite JSeM to construct a pipeline that automatically computes inference validity from sentences, thereby quantitatively verifying the theory.
- 2026/3/8At NLP2026@Utsunomiya, we present 7 posters in "Q6: Computational and Formal Linguistics" on Wed., March 11, 11:15–12:45.👉
- 2025/10/21LENLS21 (Nov.28-30, Nagoya) program is now available. Registration deadline is Oct.31 for conference dinner participants, and Nov.16 for general participants.👉
- 2025/9/30Our project has been adopted by JST CREST "Creation of an Interdisciplinary System Foundation for Realizing a Society of Human-AI Coexistence and Collaboration": "The Nexus of Human-LLM Interaction: A Multidisciplinary Linguistic Approach to Building a Collaborative Feedback Loop" — PI: Daisuke Bekki; Co-PIs: Daisuke Kawahara (Waseda), Takuya Matsuzaki (Tokyo Univ. of Science), Yohei Oseki (UTokyo), Hitomi Yanaka (UTokyo).👉
- 2025/11/10Natsunako Miyakawa (M1, Bekki Lab) received the Student Encouragement Award at the 2025 Annual Conference of the Japanese Society for Artificial Intelligence, for "Towards the Development of an Automated Theorem Prover Neural Wani for Dependent Type Theory."👉
A Japanese/English CCG parser with DTS semantic composition, and automated theorem prover for dependent type theory.
Japanese semantic test suite (Japanese FraCaS and extensions)
A collection of deep learning tools for Hasktorch to facilitate neural network development including implementations of various layers, such as LSTMs and Transformers.
This course provides a comprehensive overview of Dependent Type Semantics (DTS), a proof-theoretic semantics of natural language based on dependent type theory.
