形式手法に連続的要素を取り込むために、 抽象数学による理論構築をめざす

　今日、製造業において、高度な情報処理技術を用いた自動化とソフトウエア支援により、設計から生産までの製造工程のあり方を根本的に変える取り組みが進んでいます。こうした背景を踏まえて、本プロジェクトでは従来のものづくり技術にソフトウエア科学の成果を導入し、仕様策定から設計、実装、保守に至る工業製品開発のさまざまな側面を支援するソフトウエア・ツールの構築をめざしています。

　具体的には、「形式手法」という、ソフトウエア科学における数学を基盤としたシステム設計の技法を取り込むことにより、自動車などの工業製品を例とする「物理情報システム」に対して、品質保証や効率化を担うソフトウエア支援の方法論を探究します。物理情報システムに形式手法を適用するためには、これまでコンピュータでの計算を前提として「離散的要素」を扱ってきた形式手法に、物理系の連続ダイナミクスや確率・時間などの「連続的要素」を包含させ、拡張することが必要になります（図1）。

図1　形式手法の拡張：ソフトウエアから物理情報システムへ

　主にソフトウエアを対象として研究開発が行われてきた形式手法は、ソフトウエアが期待通り動作することの数学的証明（検証）や、期待通り動作するソフトウエアの自動生成など、さまざまな成果を上げてきました。計算機制御に起因する膨大な複雑さを持つ物理情報システムに対して、同様に形式手法を適用しようというのは自然なアイデアですが、そのためには越えるべき大きな障壁がいくつかあります。例えば、一般的に微分方程式で記述されるような連続ダイナミクスは、伝統的なソフトウエア科学では扱いません。また、物理情報システムの満たすべき性質は、Yes/Noで答えられる定性的なものよりも、「何秒後に成り立つのか」「どれくらいのエネルギーが必要なのか」「どれくらいの確率で成り立つのか」といった定量的であることが多い。そのため、形式手法の拡張が必要になるのです。

　この理論的に困難な課題に対して、我々は独自のアプローチとして形式手法の拡張の過程そのものを数学的に解析し、高次（メタレベル）の理論を構築することで普遍的な知見を獲得して、形式手法の諸技法を一挙に拡張したいと考えています（図2）。

　このメタレベルのアプローチは、「論理学」や「圏論」といったさまざまな抽象数学の技法を駆使するという、きわめて理論的なものです。一方で、こうした理論研究の成果を産業界が実際に抱える課題に対して適用しようとする応用志向も、本プロジェクトのきわだった特徴です。

図2 独自の方法論 ： メタ理論による移転

　本来、ソフトウエアを対象とする形式手法を物理情報システムに適用するには、もともとの手法・理論Tを拡張して、連続ダイナミクスなどの新たな関心事eに対処できるようにする必要があります。このような拡張の必要性は世界的に広く認識され、さまざまな研究成果が得られています。しかし、これら既存研究は各個撃破的とも言える、個別対応をとることが多く、ある特定のTとある特定のeに対して、拡張T［e］を樹立する形で進んできました。
　こうした問題に対して、私たちは、独自の理論的アプローチによって、さまざまな課題に対応できる柔軟な方法論を確立したいと思っています。
　具体的には、個別の理論Tと個別の関心事eについて拡張が行われる例をいくつか観察し、数理的に解析することで、理論の拡張のための理論を構築します。理論について一つ上のレベル（高次元）から語る理論なので、これをメタ理論と呼びます。メタ理論の構築という取り組みは、理論家に「本質への理解」という喜びを与えますが、応用面でも次のような利点があります。すなわち、拡張 T + e → T［e］の一般論の定式化（Tとeを特定のものに制限しない）と、それから一挙に導かれる多数の個別的理論の拡張という成果です。さまざまな側面を持つヘテロジニアスシステムとしての物理情報システムへの応用において、このような一般論の持つ柔軟性は大きな魅力です。

産業界の具体的なニーズへの適用や自動運転における先駆的な取り組みなどを推進

　応用の具体的な方向性については、二つのアプローチで進めます。一つ目は、国内外の企業と協働し、実際の製品設計プロセスに対して形式手法による支援を行います。これは設計プロセス全体を刷新しようというものではなく、例えば、あるテストにかかる時間を3日から半日程度に短縮するといった、具体的かつ実践的な試みです。それを可能にするのが理論的アプローチによる定式化であり、課題に対する柔軟な対応を実現します。理論的な成果を用いることで、産業界の具体的ニーズとのマッチングが容易になるのです。

　応用の方向性の二つ目は、ソフトウエアを中心とした先駆的な製品設計プロセスにおいて、形式手法の果たすべき役割を追究することです。ここではカナダのウォータールー大学の自動運転システム開発プロジェクト「Autonomoose」のメンバーと協働し、彼らが開発する自動運転車をテストベッド（試験用のプラットフォーム）として、形式手法の産業応用について先駆的研究を行います。本プロジェクトは四つのグループで、以上のような研究を推進します（図3）。

図3　プロジェクト構成

「聞き上手な数学者」としてのグループ0の介在によって、数学を軸とした異分野協働を実現します。
　
　　

　ソフトウエア科学と制御理論を専門とする研究者が協働しながら形式手法の具体的拡張を担うグループ1と、ソフトウエア工学の実践的視点から機械学習等の研究者と協働しながら実用的手法の実現をめざすグループ3の両方が、国内外の企業と協働して研究成果の実用化を担当します。そして、産業応用の先駆的研究を行うのは、ウォータールー大学に拠点をかまえるグループ2です。これらのグループの研究活動を追跡し、抽象数学の視点からの一般化や、異なるトピックのマッチングを行うのがグループ0です。グループ0、1、3の大部分を東京のNII拠点に集約し、グループの垣根にとらわれない自由で学際的な研究活動を行っています。

　なお、本プロジェクトは科学技術振興機構のERATOプログラムのプロジェクトの一つとして、2016年10月に研究を開始しました（2022年3月まで）。本プロジェクトの長期的意義としては、上述の産業応用はもちろんのこと、現代数学の抽象化・一般化志向によってのみ獲得することが可能な柔軟性を社会の課題に応用するという、応用数学の新たな一類型を呈示することもめざしています。