ERATO MMSD – ERATO Metamathematics for Systems Design Project

採用情報

以下のポジションで研究員・プログラマーを募集しています．ぜひ国内からの応募もご検討ください．

関連して，協力して研究を行っている京都大学五十嵐・末永研究室でも，次の求人があります．

博士研究員募集（IoTセキュリティのためのプログラミング言語理論，京都大学）

自動運転車の安全性に数学的証明を与える新手法を開発
～論理的安全ルールの効率的導出により自動運転の社会受容を加速～

以下の論文の成果を，NII および JST からニュースリリースしました．

情報・システム研究機構国立情報学研究所（ＮＩＩ、所長：喜連川優、東京都千代田区）のアーキテクチャ科学研究系教授蓮尾一郎らの研究チームは、科学技術振興機構（ＪＳＴ、理事長：橋本和仁、東京都千代田区）の戦略的創造研究推進事業ＥＲＡＴＯ蓮尾メタ数理システムデザインプロジェクト（ＥＲＡＴＯＭＭＳＤ、研究総括：ＮＩＩアーキテクチャ科学研究系教授蓮尾一郎）のもと、自動車の自動運転システムの安全性に強い数学的保証を与える技術とその基礎理論を開発しました。

本研究では、自動運転安全性の数学的証明のための既存の方法論「ＲＳＳ（責任感知型安全論、responsibility-sensitive safety）」に注目し、その応用範囲を大きく拡大し実世界へ本格展開できるよう拡張した手法「ＧＡ－ＲＳＳ（goal-aware RSS）」を確立しました。形式論理学の知見を用いた今回の拡張によって、非常停止などの目標達成を求める複雑な運転シナリオに対しても、安全性の数学的証明が可能になります。

本研究成果は、２０２２年７月５日（米国東部時間）に、「IEEE Transactions on Intelligent Vehicles」のオンライン版で公開されました。

リンク

採用情報

以下のポジションで研究員・プログラマーを募集しています．ぜひ国内からの応募もご検討ください．

自動運転における重大な問題をシミュレーションで検出する技術を開発
～問題が発生するかを探り、起こりうる問題だけを効率的に自動探索～

以下の論文の成果を，NII および JST からニュースリリースしました．

情報・システム研究機構国立情報学研究所（NIIエヌアイアイ、所長：喜連川優、東京都千代田区）のアーキテクチャ科学研究系准教授石川いしかわ冬樹ふゆきらの研究チームは、科学技術振興機構（JSTジェイエスティー、理事長：濵口道成、東京都千代田区）の戦略的創造研究推進事業 ERATOエラトー蓮尾メタ数理システムデザインプロジェクト（ERATO MMSD、研究総括：NIIアーキテクチャ科学研究系准教授蓮尾一郎）のもと、自動運転システムのシミュレーションにおいて、急加速や急ハンドルが起きているなど事故につながるような複合的で重大な問題が発生するシミュレーションシナリオを効率よく自動で見つける技術を開発しました。

本手法では、シミュレーションの試行を繰り返す中で、追い越しや右折などのシナリオごとに起こりえない問題を見つけて不要なシミュレーション試行を除外することで、重大な問題が起きるような本当に重要なシナリオ、例えばあまりにも強い加速と急ハンドルが同時に発生するなどの状況を効率的に見つけ出すことができます。

　本研究成果は、ソフトウェア工学における自動化についてのフラッグシップ国際会議ASE 2021で2021年11月16日（オーストラリア時間）に発表されました。

NIIからのニュースリリース

ニュースリリース：信頼性が高いガスタービンのシステム設計を自動で効率良く発見する技術を開発～ブラックボックス最適化での論理仕様に着目、企業の実製品の設計プロセスに応用

以下の論文の成果を，NII および JST からニュースリリースしました．

情報・システム研究機構国立情報学研究所（NIIエヌアイアイ、所長：喜連川優、東京都千代田区）のアーキテクチャ科学研究系リサーチアシスタント（総合研究大学院大学大学院生）佐藤さとう創太そうた、同研究系准教授蓮尾はすお一郎いちろうらの研究チームは、三菱重工と協働し、ガスタービンの制御システム設計で与えられた複数の要求仕様を満たす設計を自動で発見する手法を開発しました。この研究は、科学技術振興機構（JSTジェイエスティー、理事長：濵口道成、東京都千代田区）の戦略的創造研究推進事業 ERATOエラトー蓮尾メタ数理システムデザインプロジェクト^（*1）（ERATO MMSD、研究総括：NIIアーキテクチャ科学研究系准教授・蓮尾一郎）のもとで行われたものです。

　従来の制御システム自動設計手法では、エキスパート（専門家）による設計に匹敵する品質の制御方法を発見できませんでした。今回開発した手法では、従来の手法を改良し、エキスパートによる設計に匹敵する制御方法を全自動計算によって発見できるようになりました。本手法は、内部の挙動を数式などのモデルで記述できない「ブラックボックス」な制御システム一般に対して活用でき、自動運転をはじめとした様々な分野での設計プロセスに応用が期待されます。

　本研究成果は、第24回国際フォーマルメソッド・シンポジウム（オンライン開催）で2021年11月24日（水）（中国時間）に発表されます。

SSBSE 2021 Distinguished paper award受賞

Paolo Arcaini 特任准教授，SSBSE 2021にて “Distinguished paper award受賞

Paolo Arcaini 特任准教授 (NII) が下記の論文によって、国際会議 SSBSE 2021において”Distinguished paper awardを受賞しました

Xinyi Wang, Paolo Arcaini, Tao Yue, Shaukat Ali

Generating Failing Test Suites for Quantum Programs With Search

Paolo Arcaini 特任准教授は ERATO MMSD プロジェクトグループ 3のグループリーダです

ニュースリリース：計測誤差があるセンサーを使っても安全に動くよう制御ソフトウェアを自動で変換する手法を開発～「誤差はないものとする」理想上設計で現実を安全に～

以下の研究成果が，NII および JST からニュースリリースされました．

情報・システム研究機構国立情報学研究所（ N I I 、所長：喜連川優、東京都千代田区）のアーキテクチャ科学研究系特任研究員小林努（こばやし・つとむ）、同研究系准教授蓮尾一郎（はすお・いちろう）らの研究チームは、科学技術振興機構（ J S T 、理事長：濵口道成、東京都千代田区）の戦略的創造研究推進事業 ERATO蓮尾メタ数理システムデザインプロジェクト(*1)（ERATO MMSD、研究総括：NII アーキテクチャ科学研究系准教授・蓮尾一郎）のもと、制御システムのセンサーに計測誤差があっても、安全に動くように制御ソフトウェアのモデルを自動で変換する手法を開発しました。この手法を使うと、ソフトウェアのモデルを自動変換するとともに、出力された制御ソフトウェアが耐えられる誤差の限界を示す数式を得ることができます。本手法は、自動運転をはじめとした外部環境とやり取りする様々な制御システムに対して活用でき、多様な利用環境や計測手段に対応するシステムへの応用が期待されます。
本研究成果は、第 13 回 NASA フォーマルメソッド・シンポジウムで 2021 年 5 月 26 日（水）にオンライン発表されました。

NII からのニュースリリース

JST からのプレスリリース

関連メディア記事（日刊工業新聞電子版）

関連メディア記事（BtoBプラットフォーム業界チャネル）

FreneticアルゴリズムがSBSTコンテストで優れた成績を残しました!

Ezequiel Castellano, Ahmet Cetinkaya, Cédric Ho Thanh, Stefan Klikovits, Xiaoyi Zhang, Paolo Arcainiからなるチームは物理情報システムのテストコンテストであるSBST 2021にツール Freneticを提出し、失敗事例の生成レートと多様さの点において良い成績を挙げました。

コンテストは自動運転システムの車線保持機能のテストシナリオを生成することを主眼にしており、BeamNGシミュレーターを用いています。コンテストの目的は車線保持の失敗(境界逸脱エラーとも言う)を引き起こすような仮想の道路を、限られた時間内に複数生成することにあります。コンテストに提出されたツールは、制限時間、自動車の状態、境界逸脱エラーの許容量を変えた２つの設定の元で競いあいます。

Freneticは曲率に基づく道路の表現を用いた遺伝的手法を採用しており、摂動を加えることでより多様な道路を生成する工夫がなされています。

コンテストに参加したツールの実装に順位はつけられていませんが、コンテスト報告によりますと、Freneticは一般に大変効率がよく、多くの失敗事例を引き起こしたとのことです。また、２つの設定の元で、少なくとも10倍の境界逸脱エラーを他と比較して引き起こしたツールは２つしかなく、Freneticはそのうちの１つでした。特に、Freneticは平均して最も多様な失敗事例を提示し、自車が対向車線に逸脱するような境界逸脱エラーを最も多く見つけました。この成果は自動車メーカーにとって興味深いことであるかもしれません。

Freneticの実装とアルゴリズムの解説は私達のレポジトリにあります。