抄録/ポイント:
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
本論文では,ニューラルネットワーク(NN)ベースの自律着陸システムの形式的検証問題を考察した。このようなシステムにおいて,NN制御器は,カメラから航空機をガイドし,滑走路に接近する。視覚ベースの閉ループシステムの安全性と生活検証のための中心課題は,システム状態(例えば航空機の位置)と視覚ベースのNNコントローラによって処理された画像の間の関係を捉える数学モデルの欠如である。もう一つの課題は最先端のNNモデルチェッカーの限られた能力である。そのようなモデルチェッカーは,ニューラルネットワークの簡単な入出力ロバスト性特性のみを推論できる。この限界は,NNモデルチェッカー能力と閉ループシステムを検証する必要性の間のギャップを創り,一方,航空機動力学,知覚成分,およびNN制御器を考慮している。この目的のために,本論文では,自律着陸に用いるビジョンベースNNコントローラを検証するフレームワークであるNNLander-VeriFを提案した。NNLander-VeriFは,航空機状態とNN制御器への入力の間の関係を捉える数学モデルを得るために,透視カメラの幾何学的モデルを利用する上で,上記の課題に対処した。このモデルをNN(手動で割り当てられた重み)に変換し,それをNN制御器で構成することにより,1つの拡張NNを用いて航空機状態と制御行動の間の関係を捉えることができる。そのような拡張NNモデルは,いくつかのNNロバスト性クエリへの閉ループ検証の自然符号化をもたらし,最先端のNNモデルチェッカーが処理できる。最後に,訓練されたNNの特性を形式的に検証するためのフレームワークを評価し,その効率を示す。【JST・京大機械翻訳】