プロジェクトホームページ

研究総括　蓮尾 一郎
（国立情報学研究所 アーキテクチャ科学研究系　教授）
研究期間：2016年10月～2025年3月
※本プロジェクトは、追加支援期間（機関継承型）の枠組みにより当初研究期間を（3年）延長し、2025年3月までJSTが支援を行うことになりました。
グラント番号：JPMJER1603

 

今日の製造業では高度な情報処理技術を用いた根本的な変革が進んでいます。本プロジェクトでは従来のものづくり技術にソフトウェア科学の成果を導入し、仕様策定から設計、実装、保守まで工業製品開発のさまざまな側面を支援する手法・ツール群の構築を目指します。

具体的には、「形式手法」というソフトウェア科学における論理的設計技法を取り込むことにより、製品の品質・安全性保証や効率化の支援を大きく推進します。形式手法の製造業適用においては、確かな結論のみをボトムアップに積み上げていく従来の論理学応用とは異なり、最終目標をトップダウン・ベストエフォートな形で分解していくことを通じた「モデリングの壁」の突破が必要となります。

追加支援期間（機関継承型）ではこのブレイクスルーを、形式手法の数理的基盤を更に掘り下げて統計的手法と融合することにより追求します。この成果を「ICT技術への社会的信頼」という旗のもと結集し、特に自動運転領域に対して社会展開します。また、本プロジェクトを学術研究と産業応用の両面におけるソフトウェア研究、ICTシステム研究のセンターとして位置付け、国内外の研究機関・企業と連携して研究を進めます。

 

 

研究グループ

・メタ理論的統合グループ
・高信頼ソフトウェアシステムグループ

 

研究成果の概要

ソフトウェア制御によって複雑化する⼯業製品の安全性という喫緊の課題に対し、安全性保証技術を開発し産業界に提供するという目標のもとプロジェクト研究に取り組みました。物理情報システムから自動運転、生成AIと、新たな技術トレンドが次々出現する中で、我々は数理論理学及び代数学・圏論による数理的基盤の一般性を活かして、実用的技術を多数開発することに成功しました。たとえば自動運転車の安全性の論理的保証手法は、自動運転の社会受容に向けた一押しとして注目されています。また、論理学と最適化・学習を融合した成果群は、複雑なブラックボックスシステム（内部の動作原理が不明で入出力の観察のみが可能なシステム）の論理的解析手法を与えており、工業製品を含むICTシステム一般に応用が進んでいます。全体として我々の成果は、日々進歩する情報技術に対し、これを安全に社会に取り入れる「人間中心の情報化社会」の実現に向けて、実効的技術および数理的理論基盤を樹立するものです。同時に我々の成果は、情報技術と社会との関わり方を考える上でソフトウェア科学及び数学の果たすべき役割を示すものでもあります。

 

研究成果

自動運転車安全性の論理的証明技術

自動運転車の安全性の議論の持つ数学的本質および社会規範・慣習に注目し、これを数理論理学的に形式化することにより、数多くの運転シナリオにおいて自動運転車の安全性を証明できる手法「GA-RSS（goal-aware RSS）」を確立しました。複雑なブラックボックスシステムである自動車が多数相互に影響するマルチエージェントシステムとしての交通状況に対し、本手法は各車がエージェントとして従うべきふるまいルールを数学的に正確に定式化したうえで、事故が起こらないことの数学的証明を与えます。

テストによる統計的安全性手法が主流である現状で、本手法は論理的・ルールベース手法ならではの高い解釈可能性と説明可能性を持ち、その上で高い実効性を持つため、自動運転の本格普及に向けた一押しとして注目を集めています。プロジェクト発スタートアップ（imiron社）等を通じた社会実装の取り組みも進んでいます。また本成果は、「人命に関わる決定を行うAIをどのように人間社会が受容するか」という大きな問題の解決の先駆例となっています。

 

Ichiro Hasuo, Clovis Eberhart, James Haydon, Jérémy Dubut, Rose Bohrer, Tsutomu Kobayashi, Sasinee Pruekprasert, Xiao-Yi Zhang, Erik André Pallas, Akihisa Yamada, Kohei Suenaga, Fuyuki Ishikawa, Kenji Kamijo, Yoshiyuki Shinya, Takamasa Suetomi, “Goal-Aware RSS for Complex Scenarios via Program Logic,” in IEEE Transactions on Intelligent Vehicles, vol. 8, no. 4, pp. 3040-3072, April 2023, doi: 10.1109/TIV.2022.3169762.

プレスリリース：自動運転車の安全性に数学的証明を与える新手法を開発

 

「仕様駆動型エンジニアリング」を支えるブラックボックスシステム論理的解析技術

自動車や大規模ソフトウェアなど、近年の情報システムは複雑化・多様化しており、その設計と実装は多数のステークホルダーが参加する長期間の取り組みです。ここで発生する問題の原因究明コストや、部署間のコミュニケーションコスト、さらにシステム安全性の評価コストを下げるため、システムの満たすべき要求仕様について論理的に形式的記述を行うことで、設計と実装の厳密性・説明可能性・トレーサビリティ・効率を向上させる「仕様駆動型エンジニアリング」の考え方を、産業界とともに推進しています。これを実現するにあたり必要な技術群が我々の主要な成果の一つです。たとえば、形式仕様を元に大量の時系列データを高速にフィルタリングするアルゴリズムや、形式仕様を充足するパラメータ値を高速に自動探索するアルゴリズム、形式仕様をもとにバグを探索するアルゴリズム、さらに形式仕様記述のヒントとして論理式の充足例を高速に生成するアルゴリズムなどが、具体的成果となります。

　

仕様駆動型エンジニアリングの必要性については自動車産業・製造業を中心に広い支持を得ており、これを実現するために上記要素技術を集約したツールスイートを現在プロジェクト発スタートアップにおいて開発中です。このツールスイートのさまざまな産業領域への広汎な展開により、システムの果たすべき責任としての安全性仕様の明示化と、その安全性の効率的チェックが可能になり、新技術の製品化と社会受容のスピードが加速することが見込まれます。

 

Waga, M., André, É., Hasuo, I. (2019). Symbolic Monitoring Against Specifications Parametric in Time and Data. In: Dillig, I., Tasiran, S. (eds) Computer Aided Verification. CAV 2019. Lecture Notes in Computer Science, vol 11561. Springer, Cham.https://doi.org/10.1007/978-3-030-25540-4_30

Zhang, Z., Lyu, D., Arcaini, P., Ma, L., Hasuo, I., Zhao, J. (2021). Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness. In: Silva, A., Leino, K.R.M. (eds) Computer Aided Verification. CAV 2021. Lecture Notes in Computer Science, vol 12759. Springer, Cham.https://doi.org/10.1007/978-3-030-81685-8_29

Sato, S., Saimen, A., Waga, M., Takao, K., Hasuo, I. (2021). Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: A Gas Turbine Case Study. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds) Formal Methods. FM 2021. Lecture Notes in Computer Science, vol 13047. Springer, Cham. https://doi.org/10.1007/978-3-030-90870-6_17

Sato, S., An, J., Zhang, Z., Hasuo, I. (2024). Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications. In: Gurfinkel, A., Ganesh, V. (eds) Computer Aided Verification. CAV 2024. Lecture Notes in Computer Science, vol 14683. Springer, Cham.https://doi.org/10.1007/978-3-031-65633-0_13

 

自動運転車及びAIシステム一般の効率的テスト手法

自動運転車のテストは安全性保証のため重要ですが、（１）無数の運転シナリオの中で危険なものは稀、（２）他車に責任があり自車にはどうにもならない危険シナリオが多数存在する、（３）安全性だけでなく交通ルール遵守や快適さ、車体性能といった複数の要求を考慮する必要がある、というような独特の困難が存在します。我々は自動運転車のテストシナリオの実効性概念について実応用に基づき考察し、これを進化計算による探索技術と組み合わせることによって、自動運転システムの設計に役立つ実効的テストケースを自動生成する手法を開発しました。

本成果は、テストという統計的安全性保証手法の実効性を向上させ、また得られる安全性の説明可能性を向上させるものです。上記の論理的安全性保証手法と合わせて、自動運転の社会受容の実現に向けた取り組みの両輪となっています。また、自動運転を超えたAIシステム一般のテストへの展開も進んでいます。

Yixing Luo, Xiao-Yi Zhang, Paolo Arcaini, Zhi Jin, Haiyan Zhao, Fuyuki Ishikawa, Rongxin Wu, and Tao Xie, “Targeting Requirements Violations of Autonomous Driving Systems by Dynamic Evolutionary Search,” 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), Melbourne, Australia, 2021, pp. 279-291, doi: 10.1109/ASE51524.2021.9678883.

プレスリリース：自動運転における重大な問題をシミュレーションで検出する技術を開発

 

論理学・ソフトウェア科学と制御理論の融合

物理系とソフトウェア制御を組み合わせた物理情報システムの安全性保証の問題は、自動車や多くの工業製品に応用を持つ重要な問題です。ここでは、伝統的に物理システムの解析を行ってきた制御理論の学術分野と、ソフトウェア制御の解析を行ってきたソフトウェア科学分野、この二分野の知見を結集し、新たな課題を解決していく必要があります。我々はプロジェクトの学際的研究体制を活かし最先端の知見を持ち寄ることで、実時間性やネットワーク構造を包摂し、論理的要求仕様を実現するようなシステム制御手法の成果を得ました。

物理情報システムの安全性保証は今後も重要な問題ですが、AI技術の進歩により、対象システムの面でも解析手法の面でも大きな変化が起きつつあります。しかし、人間中心の情報化社会を目指す限り、人間・社会との契約の明示化としての論理的要求仕様の重要性は変わりません。我々の上記成果は引き続き安全性保証技術の理論的基礎として重要な役割を果たしていくものと期待されます。

 

 

C. Eberhart, J. Haydon, J. Dubut, A. Cetinkaya and S. Pruekprasert, “Logic for Timed Agent Network Topologies,” 2022 IEEE 61st Conference on Decision and Control (CDC), Cancun, Mexico, 2022, pp. 2870-2877, doi: 10.1109/CDC51059.2022.9992550.

 

圏論の数学的構造論が導く高速モデル検査アルゴリズム

現代数学の抽象言語である圏論は、代数学をはじめ数学のさまざまな分野で使われています。情報学、特にソフトウェア科学における圏論の応用も盛んに研究されていますが、これまでの応用の多くは「正当性の確認の道具」及び「発想の道具」としての活用にとどまり、情報学の花形である高速アルゴリズムへの直接応用の事例は限られていました。この現状に対し、我々は状態遷移システムの安全性を自動で証明するモデル検査の問題に注目して、アルゴリズム的本質を圏論の抽象言語で適切に表現することにより、「圏論が高速アルゴリズムを直接導く」事例を複数示しました。その一例として、複雑なシステムのモデルを分割統治し、全自動で効率よく検査できる要素還元的確率モデル検査アルゴリズムを初めて開発しました。

上記成果群についての論文は、圏論の抽象言語を用いながらも、モデル検査のアルゴリズム的研究の最高峰国際会議で発表された数少ない例となっています。これらの成果は高速な安全性保証手法を新たに実用に供するのみならず、圏論を情報学の諸現象のモデリングに用いるシステム意味論分野と、モデル検査のアルゴリズム的研究分野の間の垣根を打破し、ソフトウェア科学研究の新地平を示すものです。

 

 

Watanabe, K., Eberhart, C., Asada, K., Hasuo, I. (2023). Compositional Probabilistic Model Checking with String Diagrams of MDPs. In: Enea, C., Lal, A. (eds) Computer Aided Verification. CAV 2023. Lecture Notes in Computer Science, vol 13966. Springer, Cham.https://doi.org/10.1007/978-3-031-37709-9_3

Kori, M., Ascari, F., Bonchi, F., Bruni, R., Gori, R., Hasuo, I. (2023). Exploiting Adjoints in Property Directed Reachability Analysis. In: Enea, C., Lal, A. (eds) Computer Aided Verification. CAV 2023. Lecture Notes in Computer Science, vol 13965. Springer, Cham.https://doi.org/10.1007/978-3-031-37703-7_3

 

評価・追跡調査

• 中間評価