ニュース / News
ニュースリリース
信頼性が高いガスタービンのシステム設計を自動で効率良く発見する技術を開発
~ブラックボックス最適化での論理仕様に着目、企業の実製品の設計プロセスに応用~
情報・システム研究機構 国立情報学研究所(NII、所長:喜連川 優、東京都千代田区)のアーキテクチャ科学研究系リサーチアシスタント(総合研究大学院大学 大学院生) 佐藤 創太、同研究系准教授 蓮尾 一郎らの研究チームは、三菱重工と協働し、ガスタービンの制御システム設計で与えられた複数の要求仕様を満たす設計を自動で発見する手法を開発しました。この研究は、科学技術振興機構(JST、理事長:濵口 道成、東京都千代田区)の戦略的創造研究推進事業 ERATO蓮尾メタ数理システムデザインプロジェクト(*1)(ERATO MMSD、研究総括:NIIアーキテクチャ科学研究系准教授・蓮尾 一郎)のもとで行われたものです。
従来の制御システム自動設計手法では、エキスパート(専門家)による設計に匹敵する品質の制御方法を発見できませんでした。今回開発した手法では、従来の手法を改良し、エキスパートによる設計に匹敵する制御方法を全自動計算によって発見できるようになりました。本手法は、内部の挙動を数式などのモデルで記述できない「ブラックボックス」な制御システム一般に対して活用でき、自動運転をはじめとした様々な分野での設計プロセスに応用が期待されます。
本研究成果は、第24回国際フォーマルメソッド・シンポジウム(オンライン開催)で2021年11月24日(水)(中国時間)に発表されます。
背景
機械製品の制御システムを設計するうえでは、「効率の良さ」や「安全性」といった要求仕様をシステムが満たすかを確認する製品の「品質保証」を行う必要があります。ここで、製品の効率化・高信頼化のためにシステムを調整することは「最適化」と呼ばれ、産業界における製品開発では日常的に行われています。今回我々は三菱重工との協働で、発電用ガスタービンの安全性確認・最適化に取り組みました。そのような大規模な制御システムの安全性確認と最適化のためには、実際の機器で繰り返し実験することは現実的ではないため、コンピューターによるシミュレーションを利用することが有効です。
効率の良いガスタービンのシステム設計とは、制御に無駄のない発電システムの実現を意味します。例えば、電力需要が下がった場合に、出力を急激に抑えてしまうと、内部の温度が限界を下回りエンジンが止まってしまう「失火」というトラブルが発生するおそれがあります。失火するとエンジンの再起動に長い時間と手間がかかってしまいます。一方で、出力を下げるのが緩慢すぎると、タービンの回転数が上がってしまい、故障に繋がります。つまり、信頼性の高いガスタービンを設計するためには、温度や回転数といった複数の要素に関する要求をすべて満たすような、賢く精密に制御できるシステムが必要です(図1)。多くの場合、制御システムの最適化は「パラメータ」と呼ばれる数個~数百個の数値を調整する複雑な問題になります。つまり、信頼性の高い制御システムを設計するためには、無数の可能性の中からより良いパラメータ値を効率良く見つけることが必要です。
<図1>ガスタービンの制御システムでは、温度変化が失火領域に入らないようにしつつ、回転数が上がりすぎるなどの故障の原因を防ぎたい。この複数の要求を同時に満たすには、賢い制御システムを設計する必要がある。
パラメータの最適化は、多くの場合エキスパート(専門家)による試行錯誤と熟練の知識によって行われますが、もしこれをコンピューターで自動的に行うことができるならば、設計コストの大幅な削減が期待できます。例えば、システム内部の挙動がすべて明らかで、微分方程式など、挙動を精緻に表せる数式を用いてシステムのふるまいを記述できる場合は、最適化は既存の解法(ソルバー)を用いて自動探索が可能です。そのようなシステムは「ホワイトボックス」と呼ばれますが、個別の複雑な問題が複合して現れる実際の産業製品では、システムをホワイトボックスと見なして実用的な結果が得られるケースは非常に限られています。複雑なシステムの挙動を完全に数式化することが難しいためです。本研究では三菱重工で実際に使われているガスタービン製品を対象システムとして扱いましたが、このシステムを制御するソフトウェアは大部分がマシン語で記述されているため、人が解読するのが困難で、かつ複雑なコンピューター制御になっており、数式などの手法により数学的に扱うことができない「ブラックボックス」でした。
これまで、ブラックボックスシステムの最適化のためには、「確率的最適化」や「進化計算」などのアルゴリズムが用いられてきました。これらのアルゴリズムは、パラメータとその出力の対応関係のみを利用してシステムを最適化できるパラメータの数値を探索するため、今回の対象システムのようなブラックボックスにも適用することができ、ガスタービンのほかに自動車や飛行機の制御システムの設計などにおいても利用されています。しかしながら、システムがより複雑に、要求仕様がより厳しくなるにつれ、実用に耐えるパラメータを発見するのは困難になっていきます。今回の対象システムでは、これら既存のブラックボックス最適化手法を用いても、人間が設計したシステムに匹敵するような結果は得られませんでした。このように、多くの実用的なシステム設計では、エキスパートの根気強い試行錯誤と、明文化されていない熟練の知識によるパラメータ最適化がいまだ一般的に行われています。
研究手法・成果
本研究では、「反例生成」と呼ばれるブラックボックス最適化手法の1つを改良することで、実際のシステムで実用的で最適な結果を出せる手法の開発に取り組みました。その結果、既存のブラックボックス最適化手法では安全基準を満たすパラメータを見つけられなかった難点を克服すると同時に、エキスパートが手動で最適化した結果に匹敵する品質のパラメータを見つけることに成功しました。
また、エキスパートによる手動最適化では7日間の試行錯誤が必要でしたが、今回開発した手法ではコンピューターによる3時間の自動計算で結果を得ることができ、大幅に設計コストを抑えることができました。また、この新手法は大規模な計算設備を用意する必要はなく、ラップトップ程度の身近なコンピューター上で実行可能です。
<図2>従来の反例生成手法では、複数の形式仕様が与えられたときに違反度の情報が隠れてしまう「マスキング」問題があった(左)が、提案手法では複数の目的関数を用いることでそれぞれの違反度をバランス良く考慮している(右)。
一般に反例生成では、「ある要求仕様を満たすパラメータを見つける」という品質保証の問題を解くために①あるパラメータを与えたときのシステムが要求仕様をどのくらい違反しているかを実数値で表す関数(目的関数)を作成する、②目的関数の値がより小さくなる方向にパラメータを繰り返し修正する(勾配降下法などの汎用アルゴリズムを利用)、という2段階の手順を踏みます。このとき、要求仕様は、時相論理と呼ばれる時間に関する表現を扱う論理式で記述した「形式仕様」の形で与えられます。従来の反例生成手法では、論理式が「安全性に関する要求仕様Aを満たし、かつ効率に関する要求仕様Bを満たし、......」といった複数の要求仕様を「かつ」で結んだ形になっている場合(いくつもの要求仕様を同時に満たさなければならない場合)に、全体ではなくただ1つの要求仕様が小さくなる方向にパラメータの修正が進む場合がありました。この問題は「マスキング」と呼ばれ、要求仕様が複数あったとしても目的関数は1つしかないことに由来しています(図2・左:従来の反例生成)。本研究では、反例生成の2段階の手順をそれぞれ拡張し、①目的関数を複数用いて、②複数の目的関数上で探索を行う手法を開発しました。このような複数の目的関数を用いる最適化は「多目的最適化」と呼ばれ、従来の最適化とは全く異なる複雑な計算が必要です。そのため、反例生成にそのまま応用しても現実的な時間で計算を終えるのは難しくなってしまいます。そこで本研究では、多目的最適化の条件を弱めた「制約つき最適化」を用いた手法を考案し、論理式が複数の要求仕様を「かつ」で結んだ形になっている場合に有効であることを示しました。さらに、最近の制約付き最適化の研究で de Paula Garcia らによって提案された「ランキングベース」のアルゴリズムを用いることで、複雑な計算を行うことなくマスキングの問題を回避しました(図2・右:提案手法)。
以上のように、本研究では、ブラックボックス最適化において、論理式で書かれた形式仕様に着目して改良を行いました。従来のシステムの最適化において、このような論理的仕様を活かした計算が効果を発揮するのは、システムの挙動を書き出せるような離散的で扱いやすいモデルを持っている場合(ホワイトボックスの場合)のみに限られる傾向にありました。しかし本研究において、そのようなモデルがない場合(ブラックボックスの場合)でも、論理に着目した手法が実用性を持つことを実証できました。
今後の展望
本研究では、論理的仕様を活かしたブラックボックス最適化により、人間による手動最適化を上回る結果を、短時間で出すことができました。論理的仕様を活かしたブラックボックス最適化はこれまで主に自動車や航空機といった特定の分野の危険シナリオ発見に応用されてきましたが、今回、ガスタービンなどより広汎な工業製品の設計・安全性確認・最適化に有用である例を示すことができました。
本手法のポイントは、形式仕様の持つ論理的な構造をうまく最適化アルゴリズムに反映したことにあります。このことは、従来は限られた場面でしか注目されてこなかった論理的手法を、実世界の問題に広く応用できる大きな可能性を示しています。一方で、本手法を用いるには難点もあります。本手法では、これまで自然言語で書かれていた要求仕様を論理式で書き表す必要があります。そのためには、新しいプログラミング言語を学ぶように、専門的な知識を身につけることが必要です。今後の課題は、誰でも使える対話型の形式仕様記述支援ツールを開発し、本手法を利用しやすくすることです。
佐藤 創太リサーチアシスタントからのコメント:
「論理学は数学的に厳密な枠組みですが、現実世界の不確実なシステムを扱うには融通が利かないところがあり、状態遷移図が書けるような限られた応用先でしか利用されていませんでした。一方で、ブラックボックス最適化や機械学習のような、確率論や連続最適化にルーツを持つ手法は多くのシステムに適用できるものの、アルゴリズムに手を加えたり、出力結果を解釈したりすることが困難です。本研究では論理的な手法とブラックボックス最適化や機械学習という相反する2つの手法の、いわば良いところ取りをすることで応用先をより広げることができました。両手法の接点を探るという方向性は、さらに推し進めていくことができそうです。また、手法の性能を引き出すためには、論理的な枠組みを人間がより理解しやすくすることが不可欠です。形式仕様の記述をはじめ、人間と論理の繋がりをサポートする技術も研究していきたいと考えています。」
研究プロジェクトについて
本研究は科学技術振興機構 戦略的創造研究推進事業 ERATO蓮尾メタ数理システムデザインプロジェクト(JPMJER1603)の一環で行われました。
論文タイトルと著者
- タイトル:Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: a Gas Turbine Case Study
- 著者:Sota Sato, Atsuyoshi Saimen, Masaki Waga, Kenji Takao, Ichiro Hasuo
- 発表会議:24th International Symposium on Formal Methods
- 発表日:2021年11月24日(中国時間)
関連リンク
ニュースリリース(PDF版)
信頼性が高いガスタービンのシステム設計を自動で効率良く発見する技術を開発
~ブラックボックス最適化での論理仕様に着目、企業の実製品の設計プロセスに応用~
- (*1)ERATO蓮尾メタ数理システムデザインプロジェクト:国立研究開発法人 科学技術振興機構(JST)の「戦略的創造研究推進事業ERATO」に採択されている研究プロジェクトで、Society 5.0の大きな柱となるCPSの品質保証手法の学術的研究を推進している。特に、CPSの典型例の一つとして注目される自動運転システムを重点応用対象として、その信頼性保証を支えるモデリング手法・形式検証手法・テスト手法、さらにこれらを包括する実用的な V&V 技術の研究開発に取り組んでいる。このような大きなチャレンジでは、ソフトウェア・制御・AI といった多様な学術分野の協働が必要となるため、学術分野融合の基礎となる数理的(メタ)理論も重視して研究を推進する。略称はERATO MMSD。プロジェクト詳細はhttps://www.jst.go.jp/erato/hasuo/ja/参照。
※本発表は、科学技術振興機構との共同発表です。
注目コンテンツ / SPECIAL
2024年度 要覧 SINETStream 事例紹介:トレーラー型動物施設 [徳島大学 バイオイノベーション研究所] ウェブサイト「軽井沢土曜懇話会アーカイブス」を公開 情報研シリーズ これからの「ソフトウェアづくり」との向き合い方 学術研究プラットフォーム紹介動画 教育機関DXシンポ 高等教育機関におけるセキュリティポリシー 情報・システム研究機構におけるLGBTQを尊重する基本理念 オープンサイエンスのためのデータ管理基盤ハンドブック 教育機関DXシンポ
アーカイブス コンピュータサイエンスパーク