（敬称略）

研究開発が、運転席や製造現場の「人」とつながる

蓮尾　今日はご多忙の中、お集まりいただき、ありがとうございます。私はもともと数学が専門で、数学と情報学を行き来してきました。今は、「数理的高信頼ソフトウェアシステム研究センター」で、数学を使ってソフトウェアや情報システムの信頼性を高め、新しい技術を社会に受け入れていただくために研究をしています。まず、企業の皆様から自己紹介をいただけないでしょうか。

上田　主に、組み込みシステム向けの異常検知や原因分析など、システムを監視する技術の開発に従事しています。今は、自動車が危険に至るシナリオを時相論理で形式化する研究を、NIIの蓮尾先生と共同で進めています。

髙尾　自動車の自動運転そのものではなく、重要インフラの信頼性を高める研究に取り組んできました。NIIの蓮尾先生と共同で、形式手法に基づく高信頼性制御システムを開発しています。

吉岡　もともとの専門は、車両運動制御でした。ここ数年は、自動運転技術の開発にも携わっています。頼れる副操縦士のような車載AIシステムを目指して、蓮尾先生と共同研究を行っており、運転者の異常を感知して減速や停止を行うことは可能なところまで来ています。

柳澤　私の専門は形式検証とデータ処理で、形式検証は蓮尾先生と共同研究させていただいています。主なミッションは量産開発への貢献で、それと並行して将来を見据えた技術開発も行っています。

石川　私は、ソフトウェアを開発するための支援手法を研究してきました。特に形式手法やテストなど正しさや妥当性を検査したり、誤りを分析・修正したりする研究をしています。いわゆる数学的な技術には限らず、探索的・経験的な技術にも取り組んでいます。

「人間には出来ない」が「人間にしか出来ない」の追求につながる

蓮尾　NIIとしては、地に足のついたソフトウェアの研究を大切にして いますけれども、ものづくりの現場には、最初から中身が数学で出来ているソフトウェアとは違う難しさがあります。たとえば歯車が1つあって、どういう場面でどういう挙動をするのか。歯車1つの数理モデルを作るだけで、多大なコストがかかります。さらに、多数の機構部品が組み合わせられた自動車のような巨大なシステムでは、ソフトウェアの安全性を証明するための過去のアプローチは通用しません。安全性を確保するには、これまで関係者ではなかった方々に当事者になっていただくことを含め、どのようなアプローチでどのような手法を生み出せば良いのか。私たちだけでは出来ないチャレンジです。

上田　人工衛星や自動車のように正常に動作し続けることが求められる高信頼システムでは、ソフトウェアにバグがあってはならないのですが、バグの原因の一つは、人によって仕様書の解釈が異なることです。人間が自然言語で仕様書を書き、それを人間が解釈するわけですから。しかし、国際機関で定められている安全 性評価の規格には、解釈のブレはあってはなりません。そこで国際規格で定められた交通外乱シナリオに対して、NIIさんと共同で、自動車の安全要求を形式言語で厳密に定義することに挑戦しました。結果として、「時々刻々と変化する状況を、数学的に表現する」「仕様の記述・検証・修正を一つのツールで行い、仕様を理解し、検証結果はアニメーションやグラフで理解できる」という成果が得られました。

髙尾　三菱重工では、発電プラント、新交通システムなどの大型インフラ機器だけでなく、フォークリフトなどの中量産産業機械も作っています。共通しているのは、高い信頼性が求められることです。そこで蓮尾先生と、自動検証技術や設計技術の研究開発を進めてきました。要求仕様を時相論理で定義することで、極めて複雑かつ時間的に変化する制約条件を扱えるようにし、さらに「フォルシフィケーション（falsification）」と発見的手法による探索での検証に成功しました。フォルシフィケーションは、要求仕様を満たさ「ない」条件を探索する技術です。それらの条件を回避すれば、要求仕様を満たす条件が見つかります。さらに、複雑に変化する仕様を最も満足させるパラメータの組み合わせを自動生成すれば、基本設計や機能設計の段階で、バグを作り込んだり不適切なパラメータ設定を行ってしまったりすることを避けられます。例えば、ガスタービンのような複雑なシステムで、満たさなくてはならない要件とできれば満たしたい要件が多数あり、要件それぞれの「この時点からこの時点まで」が異なる場合、設計パラメータ調整だけで人間なら数週間かかりますが、この手法を使うと数時間のシミュレーションで行えるようになりました。

多様な人や組織のつながりが、人を幸せにする技術につながる

吉岡　私たちは、「MAZDA COPILOT CONCEPT」というコンセプトの実現を目標として開発を行っています。2022年、車の運転者が急病などで運転できない時に自動的に減速させて停止させる「ドライバー異常時対応システム」を実用化し、これまでになかった考え方の安全システムということで高い評価をいただいています。

自動車事故の死亡・重傷者数は、近年、日本全体で減少を続けています。Mazda車に限定すると、全国合計よりも減少幅が大きくなっています。視界視認性の向上・衝突安全性の向上といった基本的な安全技術に、車両周辺をセンシングしてド ライバーのうっかりミスを見つけてサポートする先進安全技術を積み重ねた努力の結果です。

私たちは、この取り組みを通じて、ドライバーの体調急変による重大事故が一定数で存在しており、しかも近年は増加しており、ほとんどが一般道で発生していることに気づきました。よりいっそう安全性を高めるためには、一般道で機能する先進サポート技術が必要です。また、車の運転そのものにも効用があります。運転を継続している高齢者は、認知症リスクを4割程度減らせるというデータもあります。高齢者が運転しなくなると事故のリスクは下がるかもしれませんが、健康寿命という意味ではリスクが高まる可能性があります。そこで、「人が運転する」ということの重要性に基づいて、「COPILOT」、頼れる副操縦士がいるというコンセプトを提唱しました。平常時は黙って見守り、人が何らかの理由で運転できない状態になった時には運転タスクを切り替えて安全状態を保つという、従来の先進安全技術に人の状態に基づく安全サポートを積み重ねる概念です。

特に一般道においては、多種多様なシーンとユースケースがあります。すべてを網羅して安全性を検証することは、これまでの手法では不可能だと思われました。そこで、何らかの論理的な技術が適用できないだろうかと考え、蓮尾先生に相談し、共同研究を開始しました。現在、形式検証を使うことによって、テストだけに頼らない検証方法の構築が可能であるということを確認できています。

柳澤　2023年に中途入社し、自動車に関わる研究開発に従事しています。私の所属する InfoTech では、研究開発を通した現場（量産開発）への貢献が非常に重視されています。しかし、これがなかなかに難しい。

現場の課題をヒアリングし、課題に基づいて大学等と共同研究を行い、成果を現場にフィードバックする...というサイクルを回せるのが理想です。しかし、入社当初はまったく上手くいきませんでした。社内にコネクションがなかったため、そもそも現場にリーチするのに苦労しましたし、いざ現場に技術を売り込みに行っても、「うちの部署では使いま せん」と言われてしまったり...。何とかして理想のサイクルに近づきたいのですが、まず現場の課題がわからないことにはどうしようもありません。そこで企画したのが、現場と研究開発部門を交えた形式検証の勉強会です。蓮尾先生と柳澤が提唱している Specification-Driven Engineering (SDE)の考え方を実践していくという意気込みを込めて、SDE勉強会と名付けました。

もちろん、こちらの都合（現場の課題が知りたい）だけでは勉強会が成立しませんから、現場の方の役に立つ内容にする必要があります。勉強会の内容は主に3種類です。1つ目は、現場での成功事例を共有いただき、全社での知識の平準化とレベルアップを目指すというもの。2つ目は、現場での採用事例がない技術を、研究開発部門や大学の先生方から紹介いただくもの。3つ目は、現場の未解決の課題や困りごとを持ち寄り、皆で議論するものです。

この取り組みの成果として、現場と研究開発部門とのコミュニケーションパスが確立・強化され、現場からの相談が活発になり、さらには共同でのプロジェクトが立ち上がろうとしています。

石川　私は今、産業界からデータをいただいて、テストに関する研究を していることが多いです。産学連携は製造業と自動運転だけではなく、あらゆるシステムのあらゆる側面に関わっています。開発は、テストを必ず伴います。何をどうテストすれば見落としがなくなるのか、どのようなテスト目標をクリアすれば不安を最小にできるのか。企業の方々とは、まず、そこを議論します。ですが自動運転の場合、「他の車の位置」という膨大な状態があるわけです。その条件下で、充分と言えるテストは存在するのか。見つけられるのか。どうやって探すのか。そういう課題に、研究者として取り組んできました。

現在、「衝突が起きる条件を探し出す」という目標があれば、テストエージェントとシミュレータで探し出し、衝突の危険度を「75点」などと採点することはできています。数学や証明は前面に出さず、シミュレータがあれば自動探索できるという方向性で、蓮尾先生の取り組みとは表裏一体の関係にあります。「5時に来てください」と、「5時に来たら 合格点、5時5分に来たら5点減点」は、表裏一体ですが、同じことを表しているわけです。とはいえ、現場の方々とは、「数学を意識せずに使える賢いテストを作る」という共同研究をさせていただいています。マツダさんの事例では、賢いテストエージェントに「このスコアが高くなるようなケースを探すことで、衝突が起きるケースを見つけて」と頼むイメー ジです。より難しいケース探しを頼むと、「赤信号を無視して衝突」という極端なケースを見つけてきたりします。また衝突に至らなくても、安全走行していたはずの車が急加速する挙動は意図していないですよね。そういった挙動の把握も含めて、目的に応じたテストを生成します。自動運転やAIシステムに出来ることが拡大し続けている中で、ここ5年ほど、共同研究している企業の皆様や蓮尾先生と協力して、研究を拡大し続けているというところです。

課題を共有し、知見を重ね合わせてシナジーを

上田　「形式言語を製品開発に応用したい」という私たちのニーズ、蓮尾 先生の「専門知識を産業界に還元したい」という思いが共同研究という形で調和して、お互いに価値ある成果を得ることができたと確信しています。今後は、記述方法をさらに改良して、形式言語の専門家でなくても容易に扱えるようにすることを目指しています。また、自動車以外のシステムへの適用も考えています。

それにしても今日は、皆さんのお話がとても新鮮で有意義でした。たとえば産業界の現場の課題を研究開発部門が受け止めて学術界につなぐ流れを作ることは、どの企業も必要だと感じているのでしょうけれど、実際に成功事例を聞いてみると非常に学びが多く、「ウチでも出来るかもしれない、やってみよう」と思えますね。

柳澤　ありがとうございます。勉強会を主宰しているうちに、もともと関係のなかった部署どうしの交流が始まるなど、予想していなかった展開もありました。

吉岡　私たちも、今後さらに共同研究と新しい展開を重ねていきたいと思っています。自動運転技術の開発とは、究極のドライバーモデルを獲得することです。論理学的なアプローチの知見を高めることで、人の運転の問題点を数学的にモデル化し、より的確な情報支援・判断支援・運転支援を可能にすることに役立てる応用の可能性もあると考えています。

髙尾　私たちはガスタービンという具体的な課題を共同研究に持ち込ませていただいたのですが、蓮尾先生がそれに大変モチベートされたと伺いました。また、当時の学生さんで理論的な検討の得意な方が非常に関心を持ってくださって、アルゴリズム理論の面からも貢献してくださいました。産学連携の成功例の一つだと思っています。

石川　やりたいことを言語化することは、実現するための最初の一歩ですよね。やりたいことを数学や図式やスコアで「言語化」すると、技術として具体的に実現される可能性が生まれ、実際に実現されたりします。「数学で書く」ということから広がる可能性を、産学連携で共同研究を行っている皆さんから伺えて、今日は有意義な一日でした。課題をお持ちの産業界の皆様、ぜひお気軽にお声がけください。

蓮尾　研究を担っている研究員や学生の皆さんの頑張りにも、改めて感謝したいです。問題や課題を持ち込んでくださる企業の皆さん、それこそが私たちのモチベーションの源です。心から感謝しています。今後とも、どうぞよろしくお願いします。

構成：みわよしこ

• 蓮尾一郎 - アーキテクチャ科学研究系 - 研究者紹介
• 石川冬樹 - アーキテクチャ科学研究系 - 研究者紹介

記事へのご意見等はこちらへ