科学哲学科学史(演習)(科学史科学哲学 8241006)(学部/大学院共通)
授業開始:4月14日(火)16:45-18:15
文学部第6演習室
授業の概要・目的
本授業の最終的な目標は、受講者が論理的で明晰な思考に慣れ、何かを主張する際にはその主張がどのような根拠に基づいているかを明確化し、抜けも漏れもない論証ができるようになることである。
近年、生成人工知能の大規模言語モデル(LLM)の急速な普及に伴い、「ハルシネーション」——AIが事実に反する内容をもっともらしく生成する現象——が実用上の深刻な問題として浮上している。本授業では、この問題を第一の題材として取り上げる。LLMは統計的確率に基づいてテキストを生成するが、その出力が「正しい推論」であるかどうかをどう判定するか。通常は外界(外部のデータベースなど)への参照によって発見しようとするとするが、推論の形を見るだけで判定できることもある。後者の理論として本授業が提示するのが証明論的意味論である。これは、真理値を用いず、推論規則(導入規則・除去規則)の整合性そのものから意味を定義するアプローチであり、LLMの出力検証や記号的推論システムの基礎理論としても見なせる。
授業では、哲学的論理学の立場から、「論理とは何か」という問いを出発点に、最小命題論理の自然演繹の体系を解説し、証明論的意味論の中核概念(ハーモニー・保守的拡張など)まで段階的に習得することを目指す。JR西日本における実務でのLLM活用計画との関わりでこの問題設定に至った担当者の経験を踏まえ、純粋な哲学的論理学の学習と、人工知能への応用という視点を両軸として授業を進める。
到達目標
最小命題論理の自然演繹で基本的な演習問題が解けるようになる。さらに、導入規則と除去規則のハーモニーという観点から、推論規則の「正しさ」とは何かを理解し、LLMの推論出力を評価するための論理的な視座を身につける。
授業計画と内容
本授業は大きく三つのフェーズで構成される。第一フェーズ(第1〜9回)では自然演繹の体系を一通り習得し、第二フェーズ(第10〜11回)では証明の読み書きを演習によって定着させ、第三フェーズ(第12〜14回)では証明論的意味論の核心に踏み込む。
- 導入:LLMとハルシネーション、そして証明論的意味論——なぜ今この問題か
- 命題と導出、自然演繹の基本的な考え方
- ∧の導入規則と除去規則
- ∧を用いた証明演習
- ∨の導入規則と除去規則
- →の導入規則と除去規則
- ∨と→を組み合わせた証明演習
- ¬の規則と最小論理の位置づけ
- 最小命題論理全体の整理と復習
- 証明の読み方・書き方の演習(1)
- 証明の読み方・書き方の演習(2)
- 導入規則と除去規則のハーモニー
- Boche問題と保守的拡張——どんな規則でも許されるのか
- 証明論的意味論とLLMの推論検証——応用的展望
- 総括と後期への橋渡し
履修要件
特になし(ただし後期の哲学演習の履修は、本授業の履修が必要となるので注意すること)
成績評価の方法・基準
ほぼ毎回出題する宿題の累計成績に準じて行う。
授業外学習
授業資料は毎回、事前(1〜2日前)にKULMSにアップロードする。受講者は授業前に資料にざっと目を通しておくことが望ましい。
教科書
毎回KULMSよりハンドアウトを配布する。
参考書等
- 戸次大介『数理論理学』(東京大学出版会)
- 小野寛晰『情報科学における論理』(日本評論社)
- Dag Prawitz, Natural Deduction: A Proof-Theoretical Study
- Michael Dummett, The Logical Basis of Metaphysics(証明論的意味論の古典的文献)
その他(オフィスアワー等)
形式的な体系を理解するためには、まず手を動かして練習問題の証明をやってみること。記号の意味を哲学的に問うのはそれから。
オフィスアワーはKULMSで確認してください。