最新情報は
イベント公式サイト
をご参照ください。
（参加は要事前登録）
For information in English, click
here
（Preregistration required）
開催概要
JFLI-LIPNのThomas Seiller氏(*)、Université Sorbonne Paris Nord（ソルボンヌ北パリ大学）のCaterina Mosca氏、ならびに慶應義塾大学・産業総合研究所(AIST)のGergei Bana氏をゲストスピーカーとしてお迎えし、「アルゴリズム・プログラム・計算の論理と哲学」をテーマとする半日ワークショップを開催します。
(*) Thomas Seiller氏は現在、国立情報学研究所 (NII) に滞在中です。
形態
- 参加無料
- 要事前登録
- オンライン参加可（ハイブリッド形式）
日時
2026年5月27日(水) 13:30 - 18:00
May 27th, 2026 (Wed), 13:30 - 18:00 (JST)
会場
慶應義塾大学三田キャンパス 北別館1階 レクチャールーム2
Lecture Room 2, 1st Floor, North Annex, Mita Campus, Keio University
キャンパスマップ20番の建物です(慶應義塾大学三田キャンパスより徒歩約7分)
北別館案内図 /
North Annex Map /
Mita Campus
- 東京メトロ南北線 麻布十番駅（2番出口）徒歩約10分
Approx. 10-minute walk from Azabu-juban Station (Exit 2) on the Tokyo Metro Namboku Line - 都営地下鉄大江戸線 赤羽橋駅（中之橋口出口）徒歩約10分
Approx. 10-minute walk from Akabanebashi Station (Nakanohashi Exit) on the Toei Oedo Line - 都営浅草線・三田線 三田駅（A3出口）徒歩約17分
Approx. 17-minute walk from Mita Station (Exit A3) on the Toei Asakusa and Mita Lines - JR田町駅（三田口）徒歩約20分
Approx. 20-minute walk from Tamachi Station (Mita Exit) on the JR Lines
事前登録
参加無料，要事前登録【Pre-registration required】
登録フォームはこちら (Pre-registration form)
プログラム
最新情報および各プログラムの概要は， イベント公式ウェブサイト をご参照ください。
| Time | Program Details |
|---|---|
| 13:30 |
Opening Remarks Koji Mineshima, Mitsuhiro Okada, and Hirohiko Abe |
| 13:40 |
Deontic Reasoning of LLMs and AI Alignment Hirohiko Abe (Keio University) *Joint work with Kentaro Ozeki, Risako Ando, Takanobu Morishita, Koji Mineshima, and Mitsuhiro Okada |
| 14:20 |
Tasks, Programs and Algorithms Caterina Mosca (Université Sorbonne Paris Nord) |
| 15:20 | Break |
| 15:30 |
On a Scaling Issue of LLMs' Inductive Proofs Risako Ando, Koji Mineshima, and Mitsuhiro Okada (Keio University) |
| 16:10 |
What is an algorithm? Algorithms and programs, mathematical and formal proofs Thomas Seiller (University of Paris-13 CNRS LIPN, University of Paris 1 IHPST) |
| 17:10 | Break |
| 17:20 |
First-Order Theories for Secure Protocol Proofs: From Indistinguishability to Overwhelming Truth Gergei Bana (Keio University / AIST) and Mitsuhiro Okada (Keio University) *Joint work with Mitsuhiro Okada |
| 18:00 | Closing Discussion |
Abstracts / アブストラクト
Tasks, Programs and Algorithms
Caterina Mosca (Université Sorbonne Paris Nord)
The concept of a program is commonly interpreted within the framework of the classical programming paradigm, that is, as the implementation of an algorithm using a programming language and through the compiler. However, this conceptual framework cannot be extended to the context of neural network-based systems, in which computational behavior does not derive directly from a structure of codified rules, but emerges from statistical learning processes.
This presentation aims to reconstruct and compare the implementation processes characteristic of two different paradigms of computation: on the one hand, that of traditional programming, and on the other, that of neural systems. The comparison between these models will serve as the starting point for a reflection on the notion of an algorithm, considered not only in its technical dimension but also in its epistemological and philosophical implications. To this end, the notion of a task will be introduced as an analytical category capable of providing a unified framework for interpreting different conceptions of computational systems. This perspective requires us to examine fundamental questions such as the form of representation of the theory that guides the computational process and the ways in which abstract representations are translated into descriptions that are actually computable.
Deontic Reasoning of LLMs and AI Alignment
Hirohiko Abe (Keio University)
This presentation reports an evaluation of the performance of large language models (LLMs) on tasks involving reasoning about obligations and permissions (deontic reasoning). First, drawing on the Wason Selection Task, a well-known task concerning conditional reasoning, we show that LLMs, like humans, achieve higher accuracy on tasks framed in terms of obligations and permissions than on abstract versions, suggesting that reasoning abilities may exhibit a degree of domain specificity. We also find that the error patterns displayed by LLMs resemble those observed in humans. Rather than exhibiting confirmation bias, LLMs tend to display matching bias, namely a tendency to attend merely to the terms explicitly appearing in the conditional statement. Second, we examine the relationship between Standard Deontic Logic, which is based on classical logic, and everyday patterns of reasoning about obligations and permissions. In particular, by examining two inference patterns that are valid in Standard Deontic Logic but are not ordinarily accepted in everyday reasoning, together with one pattern that is regarded as acceptable in everyday reasoning despite being invalid in Standard Deontic Logic, we find that LLMs show a strong tendency to conform to the inferential structure of classical logic. These results suggest that AI alignment is important not only with respect to the content of obligations and permissions, but also with respect to the inferential patterns governing them.
On a Scaling Issue of LLMs' Inductive Proofs
Risako Ando, Koji Mineshima, and Mitsuhiro Okada (Keio University)
Large language models (LLMs) have recently showed strong performance in mathematical reasoning and formal theorem proving. Some models can solve Olympiad-level problems, generate formal proofs in systems like Lean and Rocq, and even assist with research-level mathematical discovery. However, it remains unclear to what extent these successes reflect genuine proof-construction ability and whether LLMs possess scalable proof construction capabilities for increasingly complex proofs. Existing systems often rely on theorem retrieval, mathematical libraries such as Lean's Mathlib, and automated tactics. Because of this, the intrinsic proving and generalization abilities of LLMs are still not well understood. To examine this issue, we study theorem proving in a strict "proof-from-scratch" setting, where models cannot use existing lemmas, external libraries, or automated tactics. We focus on evaluating how well current LLMs can construct proofs on their own, especially proofs involving mathematical induction.
The organizing committee / 実行委員会
Hirohiko Abe (Keio University)Koji Mineshima (Keio University)
Mitsuhiro Okada (Keio University)
主催
慶應義塾大学未来共生デザインセンター
Center for Design of Future Symbiosis, Keio University
https://www.carls.keio.ac.jp/symbiosis/
お問い合せ
同センター論理班：logic@abelard.flet.keio.ac.jp