情報システム学専攻　LEE Yeonseok

博士課程でのご自身の研究テーマ

私の研究テーマは、Formal Methods（形式手法）を用いたプログラム検証であり、具体的には数学と論理学を活用します。
情報学部学生の方は、「論理学」の授業でHoare Logicを学んだことがあるかと思います。これは「{事前条件} プログラム {事後条件}」というトリプルでプログラムの正当性を表現するものです。
私は、このHoare Logicを拡張した分離論理（Separation Logic）を扱う研究に取り組んでいます。分離論理は、C言語のポインターといったメモリー構造を扱うために拡張された論理体系です。
現在、研究は主に二つの柱があります。
一つ目は、Concurrent Separation Logicの分野です。これは並行プログラムを検証するために分離論理をさらに拡張したものです。その研究の中で、各論理式間の含意関係（Entailment Relation）のチェックを自動化することに取り組みました。この自動化は、Hoare Logicスタイルの証明体系において不可欠な要素です。
二つ目は、Incorrectness Separation Logicに関する研究です。この論理は、プログラムのエラー検出に特化した分離論理の拡張です。私はその証明体系の相対的完全性（Relative Completeness）を証明しました。この文脈での完全性とは、「全ての妥当な仕様が証明可能である」という性質を指し、この性質を持つ証明体系は高い信頼性が保証されます。
私の目標は、これらの研究を通じて信頼性の高いソフトウェアの自動検証に貢献することです。

博士課程に進学しようと決めた時期および動機等

博士課程への進学を決めたのは、交換留学生として滞在していた時期です。当時、論理学の授業を受講し、結縁先生と中澤先生の指導が非常に丁寧で分かりやすく、講義自体にも大変興味を持ちました。
講義後に先生方の研究室ウェブサイトで研究内容を知り、非常に興味深い分野だと感じました。すぐにゼミを申し込み、そのまま大学院へ進学しました。
コンピュータサイエンス全般に自信があったわけではありません。むしろ、「まだ知らないこと」、「埋めるべき空白」が自分の中に多いと感じたことが、大きな動機です。「もっと深く学びたい」という気持ちが、私にとって最大の進学理由となりました。

博士課程において、楽しいところ・大変なところ

博士課程で楽しかったことは、自分の予想が正しかったことを数学的に証明できた瞬間です。特に、自分が正しいと考えていた数理的性質を証明できた時には、大きな喜びを感じました。 大変だった点は、指導教員の中澤先生と結縁先生の手厚いご指導とサポートのおかげで、これといった大きな困難はありませんでした。しかし、あえて一つ挙げるとすれば、推し進めていたトピックが難航したり、正しいと思った性質がなかなか見つからなかったりした時は、やはり少しつらかったです。 ただ、理論計算機科学の分野では、自分の考えが間違っていたと証明されても、それが業績になる可能性があります。何も見つけられない状態が最も苦しいですが、これは人生のどの道においても共通する問題です。研究は「間違いの証明」も価値になるという点で、むしろリスクが少ないと感じています。

これからのキャリアや夢

人生で最も重要な時期の一つである20代後半を、優れた研究施設を持つ名古屋大学で、指導教員の先生たちや研究室のメンバー、そして日本の学界の多くの研究者の皆様の温かいご支援と励ましをいただきながら、数学と論理を深く学べたことを心から感謝しています。この時間は私にとっては恵みです。
これからは、この博士課程で培った数学的・論理的思考を、どのように世の中に役立てていくかが私の課題であり夢です。単に理論を構築するだけでなく、社会が必要としている「質問」に対して、世界が望む「答え」を導き出し、貢献できるようなキャリアを築いていきたいと考えています。

後輩たちに対するメッセージ

もし「研究が面白い」、「論文を書くのが楽しい」、「学会発表がワクワクする」と感じているなら、ぜひ博士課程に挑戦してほしいです。
「やはり新卒入社して社会人にならないと」と言う人もいるけど、皆様の実力なら、どこへ行っても困らないのは確信しております。
ただ、一度企業に入ると、また研究の道へ戻るにはコストが必要になります
（残念ながら、ほとんどの会社は皆様の論文や研究に興味がない可能性が高いです）。
博士課程は奨学金などの経済的サポートが手厚いから、生活の心配をする必要はないです。