山形 賴之
基本情報
- 所属
- 国立研究開発法人産業技術総合研究所 サイバーフィジカルセキュリティ研究センター 主任研究員
- 学位
-
博士(数理科学)(東京大学)
- 連絡先
- yoriyuki.yamagataaist.go.jp
- ORCID ID
- https://orcid.org/0000-0003-2096-677X
- J-GLOBAL ID
- 201601013913312218
- researchmap会員ID
- B000257585
- 外部リンク
広い意味での数理論理学およびその応用を研究してきました。最近の研究テーマは以下が挙げられます
1. ソフトウェアサプライチェーンのアシュアランス
ソフトウェアの開発やデプロイは多くの既存のソフトウェアパッケージや開発環境・デプロイ環境を利用します。この結果、ソフトウェアのセキュリティ等の妥当性が開発者にも把握できないことが多くなっています。この課題に対し、安全工学で用いられるアシュアランスケース(システムの安全性などをドメイン専門家に理解しやすいよう非形式的に記述した構造化文書)を活用し、とくにアシュアランスケースを記述するための図式記法であるGSN(Goal Structured Notation)を操作することに特化したプログラミング言語PGSNを開発しています。PGSNは純粋関数型言語であり、演算順序に結果がよらないことや出力の妥当性が型システムにより保証されるなど良い性質を持ちます。(ISSRE2021, 科研費基盤研究B:2023-2026)
2. サイバーフィジカルシステムの形式検証
水道・送電網・鉄道などの公共インフラは制御にコンピューターが使われています。このような、コンピューターが作り出す情報空間(サイバー空間)と送電網などの物理系(物理空間)を統合したシステムをサイバーフィジカルシステムと言います。このようなサイバーフィジカルシステムの信頼性は重要な社会的課題ですが、サイバーフィジカルシステムの複雑性によりその信頼性を保証することは容易ではありません。この課題に主に形式的手法から取り組んでいます
- 反例生成:サイバーフィジカルシステムの完全な形式検証は困難ですが、システムの正当な動作を時相論理で記述し、不正な動作を引き起こすシステムへの入力を各種の最適化技法を用いて探索する研究が行われています。これに関し、深層強化学習を用いる手法を考案し研究を行っています(TSE2020など)。
- 時相論理の確率過程への応用:サイバーフィジカルシステムは不確定な動作を行うため、確率過程として記述されます。しかし時相論理の確率過程への応用についての理論的検討は十分とはいえません。この問題に関し数学的な検討を行っており、時相論理式が満たされるというイベントが可測であること(確率論を適用する理論的前提条件)、連続時間を用いる解釈が離散時間を用いる解釈の極限としては必ずしも得られないこと、また極限として得られる場合の特定などの結果を得ています(投稿中)。
- 統計モデルによる異常検知:形式手法とは関係ありませんが、純粋に機械学習的な手法で異常を検知する研究も行っています(ICDMW2017など)。
3. 限定算術と計算複雑度
P?=NPなどといった計算複雑度にかかわる問題は基本問題です。一方、数学的帰納法を有限の範囲にのみ言及する命題がに言及した自然数に関する論理体系を限定算術といいます。(限定算術では「ある素数pとその2倍との間に必ず素数が存在する」には数学的帰納法が使えますが、「すべての数は素因数分解できる」には数学的帰納法は使えません)。限定算術のさまざまなクラスを分離する問題と計算量複雑度を分離する問題には強い関連があることが知られているため、計算複雑度の問題を限定算術からアプローチする研究を行っています(JSL2018など)
4. コロナ感染シミュレーション
私の専門とは違いますが機械学習を活用したソフトウェアを開発した経験を活用し、携帯の位置情報からCOVID19の感染を予測する研究を行ってきました。このシミュレーターは機械学習にもとづいたものではなく疫学にもとずいていますが、大規模なモデルを実行するためにPyTorchを活用してGPU上で演算を行います(BigData Workshop 2022)
研究キーワード
6経歴
9-
2018年11月 - 現在
-
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月
学歴
3-
1997年4月 - 2002年3月
-
1995年4月 - 1997年3月
-
1993年4月 - 1995年3月
主要な論文
30-
IEEE Transactions on Software Engineering abs/1805.00200 1-1 2020年 査読有り筆頭著者
-
The Journal of Symbolic Logic 83(3) 1063-1090 2018年9月 査読有り筆頭著者
-
IEEE International Conference on Data Mining Workshops, ICDMW 2017- 1058-1065 2017年12月15日 査読有り
担当経験のある科目(授業)
2所属学協会
6共同研究・競争的資金等の研究課題
2-
日本学術振興会 科学研究費助成事業 基盤研究(B) 2023年4月 - 2026年3月
-
日本学術振興会 科学研究費助成事業 基盤研究(B) 2014年4月 - 2017年3月