山形 賴之

広い意味での数理論理学およびその応用を研究してきました。最近の研究テーマは以下が挙げられます

1.  ソフトウェアサプライチェーンのアシュアランス

ソフトウェアの開発やデプロイは多くの既存のソフトウェアパッケージや開発環境・デプロイ環境を利用します。この結果、ソフトウェアのセキュリティ等の妥当性が開発者にも把握できないことが多くなっています。この課題に対し、安全工学で用いられるアシュアランスケース（システムの安全性などをドメイン専門家に理解しやすいよう非形式的に記述した構造化文書）を活用し、とくにアシュアランスケースを記述するための図式記法であるGSN（Goal Structured Notation）を操作することに特化したプログラミング言語PGSNを開発しています。PGSNは純粋関数型言語であり、演算順序に結果がよらないことや出力の妥当性が型システムにより保証されるなど良い性質を持ちます。（ISSRE2021, 科研費基盤研究B:2023-2026）

2.  サイバーフィジカルシステムの形式検証

水道・送電網・鉄道などの公共インフラは制御にコンピューターが使われています。このような、コンピューターが作り出す情報空間（サイバー空間）と送電網などの物理系（物理空間）を統合したシステムをサイバーフィジカルシステムと言います。このようなサイバーフィジカルシステムの信頼性は重要な社会的課題ですが、サイバーフィジカルシステムの複雑性によりその信頼性を保証することは容易ではありません。この課題に主に形式的手法から取り組んでいます

• 反例生成：サイバーフィジカルシステムの完全な形式検証は困難ですが、システムの正当な動作を時相論理で記述し、不正な動作を引き起こすシステムへの入力を各種の最適化技法を用いて探索する研究が行われています。これに関し、深層強化学習を用いる手法を考案し研究を行っています（TSE2020など)。
• 時相論理の確率過程への応用：サイバーフィジカルシステムは不確定な動作を行うため、確率過程として記述されます。しかし時相論理の確率過程への応用についての理論的検討は十分とはいえません。この問題に関し数学的な検討を行っており、時相論理式が満たされるというイベントが可測であること（確率論を適用する理論的前提条件）、連続時間を用いる解釈が離散時間を用いる解釈の極限としては必ずしも得られないこと、また極限として得られる場合の特定などの結果を得ています（投稿中）。
• 統計モデルによる異常検知：形式手法とは関係ありませんが、純粋に機械学習的な手法で異常を検知する研究も行っています（ICDMW2017など)。

3. 限定算術と計算複雑度

P?=NPなどといった計算複雑度にかかわる問題は基本問題です。一方、数学的帰納法を有限の範囲にのみ言及する命題がに言及した自然数に関する論理体系を限定算術といいます。（限定算術では「ある素数pとその２倍との間に必ず素数が存在する」には数学的帰納法が使えますが、「すべての数は素因数分解できる」には数学的帰納法は使えません）。限定算術のさまざまなクラスを分離する問題と計算量複雑度を分離する問題には強い関連があることが知られているため、計算複雑度の問題を限定算術からアプローチする研究を行っています（JSL2018など）

4. コロナ感染シミュレーション

私の専門とは違いますが機械学習を活用したソフトウェアを開発した経験を活用し、携帯の位置情報からCOVID19の感染を予測する研究を行ってきました。このシミュレーターは機械学習にもとづいたものではなく疫学にもとずいていますが、大規模なモデルを実行するためにPyTorchを活用してGPU上で演算を行います（BigData Workshop 2022）