山形 賴之
研究の関心
広い意味での数理論理学とその応用を研究してきました。形式手法・ソフトウェア検証・サイバーフィジカルシステムの信頼性から、限定算術と計算複雑度といった数学基礎論まで、理論と実装の両面からソフトウェアの信頼性に取り組んでいます。とくに近年は、AIのソフトウェア検証への応用に強い関心をもっています。現在取り組んでいる研究テーマは、以下の4つです。
1. ソフトウェアサプライチェーンのアシュアランス
ソフトウェアの開発やデプロイは、多くの既存のソフトウェアパッケージや開発環境・デプロイ環境を利用します。この結果、ソフトウェアのセキュリティ等の妥当性が開発者にも把握できないことが多くなっています。 この課題に対し、安全工学で用いられるアシュアランスケース（システムの安全性などをドメイン専門家に理解しやすいよう非形式的に記述した構造化文書）を活用し、とくにアシュアランスケースを記述するための図式記法であるGSN（Goal Structured Notation）を操作することに特化した純粋関数型プログラミング言語PGSNを開発しています。PGSNは演算順序に結果がよらないこと、分散実行が可能なこと、またリソースが制限された完全なサンドボックス内で実行されるため、第3者の作成したコードを安全に実行できるなどの利点があります。
2. サイバーフィジカルシステムの形式検証
水道・送電網・鉄道などの公共インフラは、制御にコンピューターが使われています。このような、コンピューターが作り出す情報空間（サイバー空間）と送電網などの物理系（物理空間）を統合したシステムをサイバーフィジカルシステムといいます。このようなサイバーフィジカルシステムの信頼性は重要な社会的課題ですが、その複雑性により信頼性を保証することは容易ではありません。この課題に、主に数理的手法から取り組んでいます。
反例生成：サイバーフィジカルシステムの完全な数理的検証は困難です。一方、システムの正当な動作を数理的に記述し、不正な動作を引き起こす入力を各種の最適化技法で探索する研究が行われています。これに関し、深層強化学習を用いる手法を考案し研究を行っています。
時相論理の確率過程への応用：サイバーフィジカルシステムは不確定な動作を行うため、確率過程として記述されます。時相論理はサイバーフィジカルシステムの仕様を論理的に記述する手法の1つとして研究が行われています。しかし、時相論理の確率過程への応用についての理論的検討は十分とはいえません。この問題に関し数学的な検討を行っており、時相論理式が満たされるというイベントにたいして確率概念が適用できること、連続時間を用いる解釈が離散時間を用いる解釈の極限としては必ずしも得られないこと、また極限として得られる場合の特定などの結果を得ています。
統計モデルによる異常検知：機械学習的な手法でソフトウェアのログを解析し、バグを発見したりサイバー攻撃を検知する研究を行っています。
3. 限定算術と計算複雑度
P =? NP などといった計算複雑度にかかわる問題は現代数学の基本問題です。一方、数学的帰納法を有限の範囲にのみ適用できる命題に言及した自然数に関する論理体系を限定算術といいます（限定算術では「ある素数pとその2倍との間に必ず素数が存在する」という有限に範囲にだけ言及する命題には数学的帰納法が使えますが、「すべての数は素因数分解できる」といった無限の領域に命題には数学的帰納法は使えません）。限定算術のさまざまなクラスを分離する問題と計算複雑度を分離する問題には強い関連があることが知られているため、計算複雑度の問題を限定算術からアプローチする研究を行っています。
4. コロナ感染シミュレーション
私の専門とは違いますが、機械学習を活用したソフトウェアを開発した経験を活かし、携帯の位置情報からCOVID-19の感染を予測する研究を行ってきました。このシミュレーターは機械学習にもとづいたものではなく疫学にもとづいていますが、大規模なモデルを実行するためにPyTorchを活用してGPU上で演算を行います。
経歴
- 2025年1月 – 現在福井大学 大学院工学研究科 Associate Professor
- 2018年11月 – 2024年12月産業技術総合研究所 サイバーフィジカルセキュリティ研究センター 主任研究員
- 2015年4月 – 2018年10月産業技術総合研究所 情報技術研究部門 主任研究員
- 2013年3月 – 2015年3月産業技術総合研究所 セキュアシステム研究部門 主任研究員
- 2012年4月 – 2013年2月産業技術総合研究所 セキュアシステム研究部門 研究員
- 2010年4月 – 2012年3月産業技術総合研究所 組み込みシステム連携研究体 研究員
- 2008年4月 – 2010年3月産業技術総合研究所 システム検証研究センター 研究員
- 2005年4月 – 2008年3月産業技術総合研究所 システム検証研究センター 任期付研究員
- 2004年8月 – 2005年3月産業技術総合研究所 システム検証研究センター 特別研究員
- 2002年9月 – 2003年3月東京都立大学 理学部数学科 非常勤講師
学歴
- 1997年4月 – 2002年3月東京大学 大学院数理科学研究科（博士課程）
- 1995年4月 – 1997年3月東京大学 理学部 数学科
- 1993年4月 – 1995年3月東京大学 理科I類
所属学会
スキル
プログラミング言語
OS・フレームワーク
語学
趣味
趣味はピアノ（クラシックのほか、『ヴァイオレット・エヴァーガーデン』など映画・アニメのサントラも演奏。なお練習していない曲はすぐに弾けなくなるので、いきなり弾けと言われても弾けません）と読書（哲学書・歴史書・ノンフィクション・漫画）です。