理論と応用を両方やることが何より楽しいし、面白い

　「大学に入学したときは、将来数学や情報科学に進もうとは考えていなかった」という蓮尾だが、東京大学1年のときに論理学に出合う。「数学の定理を自動証明する機械が作れるか」というゲーデルの不完全性定理につながる講義で、高校数学でいろいろな証明問題に取り組んできた蓮尾は、「個別の証明を自力で書いているレベルよりも、さらに上の視点があることを知り」ショックを受けた。

　その後、論理学と関連する計算機科学に進み、オランダのナイメーヘン・ラドバウド大学に有給の博士課程学生として採用され留学。指導教官のバート・ヤコブス教授は、システム検証やセキュリティなどの応用に取り組みながら、一方ですぐには応用に結び付くとは限らない計算機にまつわる論理学的かつ代数的構造を数学的に研究していた。この教授のもとで、理論と応用の両方を手掛けることの楽しさと面白さを知り、さらに「応用面での新しい成果は、理論を突き詰めた中から出てくる」ことを実感したという。

　帰国後は京都大学数理解析研究所で仕事を続けるが、ここで同僚の研究者、末永幸平氏（現・京都大学大学院情報学研究科准教授）から「蓮尾さん、日本は車をやらんとね、車を」と声をかけられ、それが一つの転機となる。末永は常に自分の専門分野の外に目を向けており、「誰も思いつかないような突飛でワイルドなアイデアをたくさん持っていた」と蓮尾は言う。

　末永氏の言葉の背景には、当時、2006年頃からアメリカで「Cyber-Physical System（物理情報システム）」がキーワードとして注目され、国策として巨額な研究開発費が投じられていた状況があった。ソフトウェアの品質保証には"形式手法"が使われるが、何百万、何千万ラインもある膨大なプログラムには、検査にかかる時間と人手とコストは現実的ではなくなり、"スケーラビリティの壁"が立ちふさがる。さらに、自動車のように実際に動く機械を相手にするには、デジタルだけでは処理できない連続ダイナミクスを扱わなければならず、極めて難しい問題となる。この分野の将来的な重要性を鑑みた末永氏は、自動車に突破口を見出せると考えたのかもしれない。

スケーラビリティの壁を超える新たな手法の確立をめざして

　末永氏の言葉を受け、蓮尾は自動車をはじめとする物理情報システムにチャレンジする。ソフトウェア検証に使われる形式手法を物理情報システムへ拡張する方法は、これまで個々の事例ごとに行われていたが、蓮尾にはそれらに共通する本質が、なんとなくモヤモヤと見えていた。それを、圏論や論理学などの抽象的な現代数学の言葉できちんと論理的に書き下ろして全体を把握する、そのようなアプローチを考えたのだ。

　2011年に東京大学で始めたこの取り組みは産業界からも注目され、2016年に科学技術振興機構（JST）のERATOプロジェクトとして立ち上げられた。理論と応用の研究者が顔を突き合わせて研究を進める独自のスタイルは非常にうまくいっており、早くも"スケーラビリティの壁"を超えるソフトウェア科学的な解決方法が、一つの成果として見えてきた。それは、ソフトウェア科学で対応できない部分はテストに絞る、という現実的だが主流とは言えない方法だった。論理学的な知見で「この範囲には絶対バグがない」と証明できれば、そこをテスト範囲から除外でき、効率的なテストを行える。現在は、このようなテスト手法を実システムに適用すべく、自動車メーカーなどと協力して研究を進めている。

　理論からの直接的な貢献が力となる一方で、「理論を突き詰めることによってできる応用があることを、ぜひ実証したい」と意欲を示す蓮尾。理論と応用が両輪になり健全な研究の展開ができると、相乗効果でどちらの研究も進むことがわかってきた。そのこと自体がこのプロジェクトの大きな成果といえるだろう。