PPL2024では，以下の2件の招待講演を予定しております．
| 渡部 有隆 | 会津大学 |
|---|---|
| コードレビュー AI によるプログラミング学習支援 | |
| 山田 晃久 | 産業技術総合研究所 |
| 岩村の補題、超限帰納法と Isabelle/HOL |
渡部 有隆（会津大学）
コードレビューは、開発者が書いたコードの品質を保証し、改善するための重要なプロセスです。これはプログラミングの学習者にとっても大きな学びの機会を提供します。しかし、特に教育現場においては、指導者の不足が問題となり、十分に実践できません。この講演では、プログラミング学習支援にAIを活用し、効果的なコードレビューの提供を目指す研究プロジェクトを紹介します。具体的には、昨今注目を集めている大規模言語モデル（LLM）を用いた手法に焦点を当て、コードレビュー活動を支援する－コード分類、バグ分類、コード修正、リファクタリング－に関する研究成果を紹介します。また、本プロジェクトの研究基盤となっているAizu Online Judge (AOJ)についても紹介します。
会津大学大学院コンピュータ理工学研究科博士課程を修了後、日本学術振興会特別研究員(PD)に採用。2008年より会津大学助教。2009年より会津大学准教授。2016年より会津大学上級准教授。研究テーマはソフトウェア工学、AI工学、プログラミング、教育支援など。Aizu Online Judgeを開発。情報処理学会優秀教育賞受賞。
山田 晃久（産業技術総合研究所）
Isabelle/HOLは、1986年から開発が続く、現在でも最も広く利用されている定理証明支援系の一つである。Isabelle/HOLが採用する公理系Higher-Order Logic (HOL)は、単純型付きラムダ計算に基づいており、一般の順序数や超限帰納法を扱えない等の制約がしばしば指摘される。本発表では、一般には順序数や(非可算の)超限帰納法を用いた証明しか知られていない定理のIsabelle/HOL形式化、特に有向集合に関する岩村の補題やそのdomain theoreticな応用について紹介する。
民間企業を経て、2014年 名古屋大学大学院 情報科学研究科 博士後期課程修了。その後Innsbruck大学、国立情報学研究所を経て、現在、産業技術総合研究所 サイバーフィジカルセキュリティ研究センター インフラ防護セキュリティ研究チーム 主任研究員。博士(情報科学)。専門は項書き換え、形式論理。