国立情報学研究所ニュース ISSN 1883-1966（Print） ISSN 1884-0817（Online）

NII Interview［プロジェクト研究総括 蓮尾一郎に聞く］

77
Sep. 2017

抽象数学で工業製品の設計支援［大阪大学サイト リーダー］

情報系と物理系の融合のカギを握る制御理論［インテリジェンス協働形式手法グループ リーダー］「形式手法」を複雑化するものづくりの現場に活かすプロジェクト解説

Feature形式手法をものづくりへ

ERATO「蓮尾メタ数理システムデザインプロジェクト」

│ NII Interview │

抽象数学で工業製品の設計支援

ソフトウエアの「形式手法」を製造現場とすり合わせる
蓮尾一郎 国立情報学研究所 アーキテクチャ科学研究系 准教授

総合研究大学院大学 複合科学研究科 准教授
JST ERATO 蓮尾メタ数理システムデザインプロジェクト 研究総括

聞き手：谷島宣之 日経 BP 総合研究所 上席研究員「テスト工程を短縮するといった定量的な成果を、ものづくりの現場で間違いなく出せます」。NIIの蓮尾一郎准教授は断言する。科学技術振興機構（JST）ERATO に採択され、2016 年 10 月から始め、2022 年 3 月まで続ける『蓮尾メタ数理システムデザインプロジェクト』において、工業製品の設計を支援する理論と手法を用意し、製造現場における “ 成功譚 ” を最低 5 件蓄積するという。何をめざし、どう進めるのか、なぜできると言い切れるのか、蓮尾准教授に尋ねた。

谷島 コンピュータソフトウエアの品質保証に役立つ数学のう数学の一領域で、今回のプロジェクトにも圏論が関係してい理論整備をしてこられた蓮尾さんが工業製品の設計支援というますから。

正反対の世界に乗り込もうと決めたのはなぜですか。

圏論は何かということですが数学理論をより抽象的に記述すソフトウエアや数学という抽象度の高い世界と、隅かる言葉だと思ってください。いろいろな理論、あるいは何らか

ら隅まで具体的なものづくりの世界は相当離れているように思の手法の裏付けとなる理論を圏論の語彙を使って記述していく

われるかもしれませんが、私としてはまったく違うことをしてと、理論や手法の抽象度を上げられ、その結果、一般性と普遍いる意識はないのです。ずっと研究してきたのは「圏論」とい性を把握でき、理論や手法の本質が見えてきます。
「そういう

蓮尾

ことか、わかったぞ」と納得できた瞬間、本当に気持ちがいい。新しいことを知る、理解する、その喜びが私が研究を続ける動機になっています。
もちろん、面白がっているだけではいけません。物事を俯瞰して本質をつかめる圏論を使って何かお役に立てないかと考えたとき、工業製品が視野に入りました。日本にとって製造業はとても重要ですから、経済にも貢献できるのではないかと。
抽象度を上げていくとソフトウエアと例えば自動車は同じよ
うに見えてきます。自動車はコンピュータを多数積み、それぞれにソフトウエアが入っている複雑な仕組みですから、それ自体が大きなソフトウエアとみなせる。それならソフトウエアの世界で培われてきた設計支援や品質保証の理論や手法を、同じ
くソフトウエアである自動車にも使えるはずだと考えました。
それを研究するのが今回のプロジェクトです。
谷島 具体的に何をするのですか。
蓮尾 高品質なソフトウエアを設計できる「形式手法」というものを拡張し、ハードウエアとソフトウエアを包含した工業製品に適用していきます。自動車もソフトウエアだと言いまし
たが当然違うところもある。ソフトウエアとは違って、物理的メカニズムがあり、エネルギーを使い、リアルタイム性が欠か蓮尾一郎
Ichiro Hasuo

02

特集│形式手法をものづくりへせません。こうした要素を形式手法で取り扱う必要があります。
プロジェクトには四つのグループがあります。圏論などを使って形式手法の本質を整理する「理論グループ」。理論に基づきつつ、工業製品に使えるように形式手法を拡張していく「実務グループ」。拡張された形式手法をものづくりの現場で使ってもらい、成果を出す「応用グループ」。応用グループは二つあり、一つは日本の製造現場が今抱えている問題に、もう一つは自動運転という将来の取り組みに、今回研究する理論と手法をそれぞれ適用していきます。
谷島 圏論など持ち出さず、形式手法をいきなり製造現場に持ち込んで実践するのと何が違うのですか。
蓮尾 先ほどお話したように一般性と普遍性を把握した上で適用していけることです。形式手法の良いところを的確に現場へ持っていける。今回のプロジェクトの特徴の一つは製造現場のエンジニアの方々と対話し、ニーズをうかがい、
「それなら

蓮尾

覚悟はあると言いましたが、実際に協力いただく企業

こう使えるのではないですか」と我々から提案し、実際に使っを決め、現場に本格的に入るのはこれからです。理論家の我々ていただくところにあります。手法の抽象度を上げておかないが実務家の方と本当に対話できるのか、不安がないと言えば噓

と、かえって個々のニーズに対応しにくい。とはいえ直接適用になります。ただ、準備のために製造業の方々と話をしていく

したからこそ、わかることもありますから、そのあたりはニー

中で、我々のグループに自分の専門外のことを調べる動きが確ズに合わせてやっていくつもりです。

実に出てきています。

谷島 結果を厳しく問われる製造現場で成果を出せますか。

プロジェクトの主旨に賛同いただいた研究者の方に集まって蓮尾 できます。というのは成果を次のように考えているか

もらったのですが、数学、ソフトウエア、制御など皆さん専門らです。例えば「ソフトウエアの検証テストに丸一日かかってはばらばらです。ところが圏論をやっていた人が制御理論の本いるが半日で終わらせたい」というニーズがあったとします。

を読んだり、制御の人と議論したり、そういう変化が起きつつ

我々は形式手法の本質をいろいろなレパートリーとして持ってあります。専門が違っても抽象度をいったん上げると、かえっいますから、ニーズに合わせて解決策を提示できます。複雑なて対話がしやすくなるからでしょう。製造現場に入っても、そテストを単純にするといった点で形式手法は成果を上げてきてうできるとよいのですが。

います。その本質はものづくりの領域でも力を出せると確信し

谷島

ています。

ジェクト』という名称の意味がようやくわかりました。抽象化

谷島 「凄い理論と手法を作りました。使ってください」と胸を経由するからメタ、そして数理でデザイン、つまり設計を支を張るプロジェクトではないということですね。

援するということですね。名称はもう少しなんとかならなかっ

蓮尾 既存の形式手法を「1」と呼ぶとして、工業製品向けにたのでしょうか。

拡張した「形式手法 2」を作り上げることがプロジェクトの目

蓮尾

的ではないのです。ニーズに応じて形式手法 2′
や 2″
がしだい

の方、数学やソフトウエアにそれほど関心がない方に我々の取に蓄積されていくことを想定しています。しかも手法 2′や 2″り組みを知っていただくためにキャッチフレーズが必要だといは研究グループが研究室で作るのではなく、製造現場の知恵をうのはわかります。遅くとも 2022 年までに考えますので宿題お借りし、一緒に作っていくことになります。成果をこつこつにさせてください。

お話を伺って『蓮尾メタ数理システムデザインプロ

私なりにスパイスを効かせたつもりでしたが……多く（写真＝佐藤祐介）

積み上げ、成功譚を五つは蓄積しよう、と言っています。
今でも覚えている恩師の言葉に「応用をやったからこそできる理論研究もある」「そのためには現場に入って手を動かせ」というものがあります。今回のプロジェクトはあくまでも学術研究であり、理論の整備が目的ですが、理論をしっかりさせるために、現場のニーズとすり合わ
せようということです。私は理論研究者ですけれども現場に入って手を動かす覚悟はあります。
谷島 課題はありますか。

インタビュアーからのひとこと「抽象的に求めたなら具体的に手に入ったのではないか」。英国の作家、チェスタトンはこう書き、物事の概念を明確にしない限り、成果など得られないと説いた。蓮尾准教授の説明を聞いている際、この言葉が頭に浮かんだ。
蓮尾プロジェクトはまさに抽象的に求め、具体的話を大きくすると、専門領域を超えた協業という日本の最大課題の一つにこのやり方は寄与できるかもしれない。学会が違うと話が通じない、同じ企業
内でも工場が違うと協力できない、といったことが現実にある。蓮尾准教授には、さまざまな領域で本質を見極めて快感を覚えつつ、日本の協業推進に資な成果を手に入れることをめざしている。もともと抽象的な形式手法の抽象度をさらに上げつつ、製造現場の問題解決に貢献する。このやり方がプロジェクトの特徴と言える。

する研究をしていただきたいと思う。

形式手法は確立されたものだが、手間やコストがかかると言われ、高信頼性が求められる特殊なソフ
トウエアにもっぱら使われてきた。今回のプロジェ
クトで抽象度をいったん上げ、形式手法の本質を見

日経 BP 社 日経 BP 総合研究所 上席研究員
1960 年生まれ。大学で数学を学び、コンピュータのエンジニアをめざしたが、1985 年日経マグロウ

出せれば、製造現場など新たな領域にも広げられそうだ。

谷島宣之 Nobuyuki Yajima

ヒル社（現・日経 BP 社）に入社、『日経コンピュータ』 誌 の 記 者 に な る。2009 年 か ら『日 経 コ ンピュータ』編集長。2016 年から現職。

2017 NII Today │ No. 77

03│ Interview │情報系と物理系の融合のカギを握る制御理論
安全で安心な超スマート社会の実現に向けて

潮 俊光氏

大阪大学大学院基礎工学研究科 教授
JST ERATO 蓮尾メタ数理システムデザインプロジェクト 大阪大学サイトリーダー

新しい技術が社会で役立つためには、それが安全に使えることが必要だ。ロボットや自動運転など
人と親和性の高い技術の場合は、さらに「安心」であることも重要な要素となる。蓮尾メタ数理
システムデザインプロジェクトのグループ 1「ヘテロジニアス形式手法グループ」において、システ
ム工学の立場から従来の制御理論を拡張し、機械学習や最適化問題などを取りこんだ理論の構築をめざす大阪大学大学院基礎工学研究科の潮俊光教授に、プロジェクトにおける役割を聞いた。

情報系と物理系の融合をめざして
ヘテロジニアスの “ ヘテロ ” は “ ホモ（同じ、よく似た）” に対応する言葉で、“ 異質な ” という意味だ。つまり、ヘテロジニ
アスとは異質なものから構成されることを示す。

が必要とされている。当プロジェクト全体で工業製品への応用までを視野に入れるなか、ヘテロジニアス形式手法グループ（G1）は、両者を統合するための理論整備を担当する。

情報系と物理系という二つの系の統合にあたっては、情報系を基盤にして物理系へ向けての拡張と、物理系を基盤にして情

近年コンピュータ制御の役割が飛躍的に増すなか、新たに開報系へという二つの方向性が考えられる。同グループにおい発される工業的な一連のシステムを安全に運営するためには、て、情報系の専門家である蓮尾一郎准教授らは、ソフトウエア

コンピュータのソフトウエア部分（情報系）と、実際に動作すの品質保証として発展してきた情報系の「形式手法」を工業製る機械部分（物理系）の両方に対応した品質保証や制御法など品開発へ応用する方向で進める。一方、システム工学の専門家である潮教授たちは、逆方向からのアプローチになるという。
潮教授の専門であるシステム工学に欠かせないのが、物理的なモノの動きを制御する制御工学であり、その基本を支えるのが「制御理論」である。従来の古典的な制御理論が扱ってきたのは、連続変数で定量的に表される物理システムだが、これにコンピュータに代表されるような離散変数で定性的に表されるシステムを融合させたものを「ハイブリッドシステム」と呼ぶ。潮教授は、ここに制御理論の応用を試みている。
例えば「ロボットに物を運ばせる」システムを開発するときに、「運ぶ」という作業工程の段取りは情報科学の定性的なロジックによって記述できるが、「どの道筋で運べば最小のエネ
ルギーで済むか」という問題は制御理論の定量的な手法で解く。
「異なる手法をうまく組み合わせて」安全なシステム作りをめざすという。

潮 俊光
Toshimitsu Ushio
1985 年神戸大学博士課程修了。現在、大阪大学大学院基礎工学研究科教授。制御系の非線形現象解析で博士号を取得後、離散事象・ハイブ
リッドシステムの制御の研究に従事し、最近は、
形式的制御系設計、強化学習に関心をもつ。

04

特集│形式手法をものづくりへセンシング

自動車

制御

情報処理

ビル
計算機

航空機

物理世界

指令
情報ネットワーク

情報世界

図│サイバーフィジカルシステムの概念

科学技術と社会との橋渡し役
とりわけ、科学技術の社会実装において、システム工学・制と潮教授は言う。
「ハイスピードで暴走する自動運転車の助手席に座らされて、『絶対に安全です』と言われても、安心できないですよね」

御理論が重要な役割を果たすと潮教授は語る。時代の最先端の自動運転においては安全なシステムを作るだけでは十分では技術をどうしたらうまく使えるか、その方法を提供してきたのなく、その人らしいやり方で運転するような、使う人にとってがシステム工学・制御理論だからだ。
「ワットが発明した蒸気

安心感のあるシステムが必要となる。

機関によって産業革命が進展したことは知られていても、同じ目標とする動作に沿ってきちんと車を動かすことは、古典的く彼が作った “ ガバナー ” が知られていないのは残念です」。

な制御理論が担ってきた。一方、人間にとって好ましい動作を

蒸気機関は安定した出力が得られなければ使いものにならない

どのように設定すべきかについては、データに基づく機械学習

が、それを可能にしたのがガバナーという調節装置。遠心力ののテクニックが有望だ。安全で安心なシステムの実現には、形仕組みをうまく使った遠心振り子でできており、出力が大きく式手法と機械学習との融合がキーポイントである。

なると遠心力でバルブが閉まり、小さくなるとバルブが緩む仕

介護ロボットなど人と協働するロボットは、人の気持ちに組みだ。安定に蒸気機関が稼働するかどうかは、遠心振り子の沿った対応が求められるが、グローバル化を視野に入れれば、開き方とバルブの閉まり方の調整具合による。この関係を理論

人の感じ方ややり方の個人差だけでなく、民族や文化のレベル化したのが制御理論の始まりだという。以後 19 世紀では、機での差を考えることも重要だ。
「日本で暮らす外国人たちに械や装置をいかに安定して動かせるかを追究し、産業発展に大とって安心なロボットの開発にも役立てられる」と潮教授は考いに貢献した。

える。

京都賞、米国国家科学賞などを受賞したルドルフ・カルマン
が提案した “ カルマンフィルター ” は、20 世紀後半の NASA

メタ（高次）の視点を持つ工学（アメリカ航空宇宙局）のアポロ計画で採用された。月面のロケッ

システム工学はさまざまな物理現象を対象とするが、その現トから地球に送られてくる信号に含まれるノイズは桁違いに多象を扱う最適な数学の手法も、またさまざまだ。潮教授は、そく、それまでの除去システムでは対応できなかったという。カの都度必要な数学をすべて学んできたという。数多くの現象を

ルマンフィルターがアポロ計画の成功に大きく貢献し、ここで手がけてきたなかで見えてくるものは何か。
「まさにメタですもシステム工学が重要な役割を果たした。現在では、あらゆるね。多くの現象に共通の枠組み、原理を見ようとする、そうい

分野でカルマンフィルターが使われている。

う意味でシステム工学はメタを扱う学問とも言えるのです。数21 世紀になった今日、IoT（モノのインターネット）が発達し、学は本来メタ的なことをやろうとしており、システム工学はそ超スマート社会の到来もすぐそこだ。今後のシステム工学・制の数学を基本において、ものを設計しようとしています」。抽

御理論の展開こそがそのカギを握ると潮教授。
「最先端の技術

象度のレベルは違っても、二つの学問は同じものを志向していをいかに安全に安心に実用化できるか。それが我々のこれからるようだ。

の使命だと思います。今回のプロジェクトの中から一つの答えが出てくればうれしいですね」

人と協働するロボットへの応用

この研究領域には世界的に注目が集まっているが、メタの視点から取り組むのが本プロジェクトの特徴だ。
「基礎理論が実際に応用されるのは 10 年、20 年先のこと。ソフトウエアだけ
でなく工業製品の設計までを見据えて、理論基盤を整備するこ

今回の研究は、人と親和性の高いロボットの開発にも有効のプロジェクトの意義は極めて大きい」と潮教授。次世代に貢だ。例えば自動運転の場合、「安全な運転と安心な運転は違う」

献する成果を期待したい。 （取材・文＝平塚裕子 写真＝佐藤祐介）
2017 NII Today │ No.77

05

│ Interview │「形式手法」を複雑化するものづくりの現場に活かす
AIと結びつくことで品質向上や次世代技術へ展開

石川冬樹

国立情報学研究所 コンテンツ科学研究系 准教授
電気通信大学 大学院情報理工学研究科 客員准教授
総合研究大学院大学 複合科学研究科 客員准教授

JST ERATO 蓮尾メタ数理システムデザインプロジェクト インテリジェンス協働形式手法グループ グループリーダー

本プロジェクトは、工業製品のものづくりに、ソフトウエア工学の知見を取り入れ、仕様策定から設計、製造、保守に至るまでの支援をめざしている。具体的には、ソフトウエアの品質保証などに用いられている「形式手法（Formal Methods）」を採用。製造業が培ってきた知見と組み合わせることで、複雑化するものづくりにおける信頼性や安全性、迅速性を、高い水準へ引き上げるというものだ。この
プロジェクトにおいて、グループ 3 「インテリジェンス協働形式手法」のグループリーダーを務める NIIの石川冬樹准教授に、形式手法によるものづくりの進化とめざす成果などについて聞いた。

さまざまなシステムの保証に活用
形式手法とは、ソフトウエアの品質を保証するために用いられている数学的、記号論理的手法である。NII の石川准教授
は、形式手法の特徴を次のように説明する。

るために、数学を活用しています。ソフトウエアのふるまいが十分に定義されているか、不具合がないかを、数理論理学を用いて判断し、事前に不具合を修正し、正しく働くことを保証するのです」
形式手法は、すでに多くの場面で利用されている。フランス「いまや、すべての構造物や工業製品に、数学が用いられての地下鉄では、高い信頼性を確保するために、形式手法を採用います。例えば、ビルや橋梁を建設する場合には、地震や洪水している。証明しながらプログラムを作る工程を経ることで、といった自然災害などを考慮して構造計算を行い、最適な設計

各部品の信頼性を高めることができたという。ほかにも、自動を行っています。ソフトウエアも同様に、品質や安全性を高め車向けのシステム開発やセキュリティなどへの応用があり、欧米主導による国際規格への適用も始まっている。
また、形式手法によって品質を保証するというケースでは、
次のような活用もある。米国では、トヨタが開発、製造、販売したクルマにおいて、アクセルペダルが戻らず急加速するという不具合が発生し、2009 〜 2010 年に大規模リコールを実施するに至った。このとき、NASA が形式手法などを用いて、これを検証。その結果、クルマのソフトウエア制御に関わる欠陥は見つからず、ソフトウエアが原因となった可能性については排除された。
以上は品質保証のために強力な検証技術を活用した事例だが、そのほかにも形式手法は効果があるという。
例えば、おサイフケータイで利用されている FeliCa の技術

石川冬樹
Fuyuki Ishikawa

06

特集│形式手法をものづくりへ

では、第 2 世代の開発において形式手法を採用し、構文・意

テリジェンス協働形式手法」は、どのような役割を果たすのだ

味が決まった方式で厳密に仕様書を記述する形に変更。これにろうか。

よって、日本語や英語などの表記による曖昧な表現を排除する

石川准教授は、「インテリジェンス協働というのは、人間やことに成功した。社内外の開発者が、表現を正しく理解するこAI による経験や傾向に基づくアプローチを従来の形式手法にとで、仕様書に起因する問題が非常に少なくなった。以後の形交えていくということ」だと語る。

式手法の利用法の改善もあり、記述不足や不明確な記述、記述「まずは、ますます複雑化する製造業のものづくりにおいの誤りにより後工程で問題が発生することはなくなったと報告て、ソフトウエア工学的形式手法がどのような効果を発揮するされている。

のか、産業界が何を求めているのかを探るところからスタート

複雑化するものづくりの安全保証に
ここ数年、製造業において、形式手法に関心が集まっている
背景にはいくつかの理由がある。

して、実務的視点からの学際的理論展開をめざします」
具体的な取り組みの一つが、ものづくりの品質向上である。
「これまでのものの作り方を検証するとともに、より効果的な作り方を模索するためのツールを提供します。これにより、完一つめは、ものづくりの複雑さが増している点だ。クルマを成したクルマが、単に安全なだけではなく、燃費が良く、速く例にあげれば、さまざまなエレクトロニクス機器やセンサーな

走り、快適であるといったようなさまざまな条件を満たす際

どが搭載され、これらを一元的に制御することの難しさが開発の、最適な品質を実現するものづくりの手法の検証が可能にな者の頭を悩ませている。現在、1 台のクルマに搭載されるセン

ります。また、効率的なものづくりという意味では、AI を組み

サーは 100 個以上とも言われており、信頼性と安全性の確合わせた形式手法を活用することで、一定の確信をもって信頼保、性能の維持といった要件の検証がますます難しくなってい

性保証を行うこともできます。例えば、従来、30 種類の検証をる。そこに、形式手法を用いることで、それらの要件をクリア行っていたものを、25 種類で済むようにしたり、あるいは 40

していくことができる。

種類に増やすべきといった判断ができたりするようになるで

二つめは、メーカーに安全性保証と説明責任が求められていしょう」

ることである。最新のクルマには衝突防止機能が搭載されお二つめは新たな技術への挑戦だ。ここでは、自動運転が直近

り、この安全性を保証し、同時にその安全性について説明するのテーマになる。
「目の前で起きていることを判断し、安全に責任が自動車メーカーには求められている。形式手法により自自動運転を行うために、無数のケースを検討する必要がありま

動検証を行い、安全性の保証と説明責任を果たすことができるす。これを個々に人手でチェックするだけでなく、理論も踏まようになるとして、関心が高まっているのだ。

えてツールで検証し、安全性を保証するのです。ここでは、グ

そして、三つめが、新たな機能や応用が広がっていること。

ループ 2 の「産業応用グループ」と連携して、同グループが最たる例が自動運転だろう。自動運転中、クルマの前に人が飛取り組んでいる実際のクルマを利用した自動運転車による検証

び出して来た場合、どういう条件なら安全かを、形式手法を用も行う予定です」

いて計算することが可能になる。
「形式手法を用いることで、こうした検証は、実際に、国内の自動車メーカーと連携しな

個々のケースを一つずつシミュレーションするだけでなく、無がら実施していくことなる。そして、ここで得た知見をクルマ数のケースを理論的にまとめて扱うような『強力な検証』も実以外の分野にも応用していく考えだ。

現でき、自動運転の安全性を高めることができるのです」
さらに、形式手法に人工知能（AI）を組み合わせることで、もう一つ石川准教授が、今回の取り組みを通じて期待しているのが、異なる分野の専門家が交流することのメリットだ。

より効率的な検証が可能になり、品質向上にも役立つ。
「クル

今回のプロジェクトには、数理学、ソフトウエア科学、制マのような物理的な動きが加わると、複雑性は一気に増しま

御、人工知能など異なる分野の専門家が参画している。石川准す。そこに AI を加えることで、問題の特性を学びながらある教授がリードするグループ 3 では、民間企業も加わって、形程度的を絞れるようになる。このような経験や傾向に基づく式手法の活用に向けた技術追求や実験を行う。
「プロジェクトAI のアプローチを形式手法と組み合わせれば、これまでよりを通じて、違う分野の専門家が一緒に論文を書くといったこと

効果的・効率的な検証が可能になるでしょう」と、石川准教授もあるでしょう」と、これまでにない相乗効果に期待する。

は語る。

「とにかくやりたいことが多い。なにを優先するか、まず交通

品質向上と新たな技術へのチャレンジ
このように、製造業を中心に、ソフトウエア工学的形式手法
が注目を集めるなかで、石川准教授がリーダーを務める『蓮尾メタ数理システムデザインプロジェクト』のグループ 3「イン整理をしなければなりません」と、石川准教授はうれしさを隠さない。
日本のものづくりを強化する上でも、このプロジェクトの成果に注目が集まる。
（取材・文＝大河原克行 写真＝佐藤祐介）

2017 NII Today │ No.77

07

│ Commentary │JST ERATO
蓮尾メタ数理システム
デザインプロジェクトについて

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

図1│

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

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

工業製品
連続的物理ダイナミクス
定量的性能指標（確率，時間，エネルギー，…）に至る工業製品開発のさまざまな側面を支援するソフトウエ
ア・ツールの構築をめざしています。
具体的には、「形式手法」という、ソフトウエア科学における数学を基盤としたシステム設計の技法を取り込むことにより、自動車などの工業製品を例とする「物理情報システム」に対して、品質保証や効率化を担うソフトウエア支援の方法論を探究します。物理情報システムに形式手法を適用するためには、これまでコンピュータでの計算を前提として「離散的要素」を扱ってきた形式手法に、物理系の連続ダイナミクスや確率・時間などの「連続的要素」を包含させ、拡張することが必要になります（図 1）。この理論的に困難な課題に対して、我々は独自のアプローチとして形式手法の拡張の過程そのものを数学的に解析し、高次（メタレベル）の理論を構築することで普遍的な知見を獲得して、形式手法の諸技法を一挙に拡張したいと考えています（図 2）。
このメタレベルのアプローチは、「論理学」や「圏論」といったさまざまな抽象数学の技法を駆使するという、きわめて理論的なものです。一方で、こうした理論研究の成果を産業界

ソフトウエア
離散的ダイナミクス
定性的指標（Yes / No）
形式仕様記述＊制約・性質の計算機で操作可能な
記述

形式検証

自動生成

＊仕様充足の数学＊仕様充足の数学＊計算機での自動

＊自動探索

的証明
証明も

的保証付き

主にソフトウエアを対象として研究開発が行われてきた形式手法
は、ソフトウエアが期待通り動作することの数学的証明（検証）や、
期待通り動作するソフトウエアの自動生成など、さまざまな成果を上げてきました。計算機制御に起因する膨大な複雑さを持つ物理情報シ
ステムに対して、同様に形式手法を適用しようというのは自然なアイが実際に抱える課題に対して適用しようとする応用志向も、本

デアですが、そのためには越えるべき大きな障壁がいくつかありま

プロジェクトのきわだった特徴です。

す。例えば、一般的に微分方程式で記述されるような連続ダイナミク

産業界の具体的なニーズへの適用や自動運転における先駆的な取り組みなどを推進
応用の具体的な方向性については、二つのアプローチで進めます。一つ目は、国内外の企業と協働し、実際の製品設計プロ

08

特集│形式手法をものづくりへ

スは、伝統的なソフトウエア科学では扱いません。また、物理情報シ
ステムの満たすべき性質は、Yes/No で答えられる定性的なものよりも、「何秒後に成り立つのか」「どれくらいのエネルギーが必要なのか」「どれくらいの確率で成り立つのか」といった定量的であることが多い。そのため、形式手法の拡張が必要になるのです。

セスに対して形式手法による支援を行います。これは設計プロ

応用の方向性の二つ目は、ソフトウエアを中心とした先駆的

セス全体を刷新しようというものではなく、例えば、あるテスな製品設計プロセスにおいて、形式手法の果たすべき役割を追トにかかる時間を 3 日から半日程度に短縮するといった、具究することです。ここではカナダのウォータールー大学の自動体的かつ実践的な試みです。それを可能にするのが理論的アプ

運転システム開発プロジェクト「Autonomoose」のメンバー

ローチによる定式化であり、課題に対する柔軟な対応を実現しと協働し、彼らが開発する自動運転車をテストベッド（試験用ます。理論的な成果を用いることで、産業界の具体的ニーズとのプラットフォーム）として、形式手法の産業応用について先駆のマッチングが容易になるのです。

的研究を行います。
本プロジェクトは四つのグループで、以上のような研究を推

図2│

独自の方法論：メタ理論による移転理論拡張のプロセス自体を理論的に解析

圏論，論理学，…

T+e

T [e]

の包括的な一般論を構築（さまざまな T と e に一挙に適用可能）
メタ理論家

+
+
+

T1
T2
T3
ソフトウエアのための形式手法e1e2
e3

T 1 [e1]T 2 [e2]T 3 [e3]

新たな関心事

物理情報システムのための形式手法

物理情報システムの多様な応用に即応

産業界
（製造業）
のニーズに根ざした理論展開
現代数学の抽象性から生まれる応用

本来、ソフトウエアを対象とする形式手法を物理情報システムに適用するには、もともとの手法・理論 T を拡張して、連続ダイナミク

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

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

スなどの新たな関心事 e に対処できるようにする必要があります。このような拡張の必要性は世界的に広く認識され、さまざまな研究成果が得られています。しかし、これら既存研究は各個撃破的とも言え

図3│

プロジェクト構成

る、個別対応をとることが多く、ある特定の T とある特定の e に対して、拡張 T［e］を樹立する形で進んできました。
こうした問題に対して、私たちは、独自の理論的アプローチによって、さまざまな課題に対応できる柔軟な方法論を確立したいと思っています。
具体的には、個別の理論 T と個別の関心事 e について拡張が行われる例をいくつか観察し、数理的に解析することで、理論の拡張のための理論を構築します。理論について一つ上のレベル（高次元）から語る理論なので、これをメタ理論と呼びます。メタ理論の構築という取り組みは、理論家に「本質への理解」という喜びを与えますが、応用面でも次のような利点があります。すなわち、拡張 T + e → T［e］の一般論の定式化（T と e を特定のものに制限しない）と、それから一挙に

G0 メタ理論的統合グループ

論理学，圏論＊リーダー：勝股審也（NII）＊プロジェクトの理論研究発展を追跡，
メタ理論的統合をめざす

ソフトウエア科学

G1 ヘテロジニアス
形式手法
グループ

＊リーダー：
蓮尾一郎（NII）＊形式手法拡張の実務
を担当
制御理論
制御工学

連続量
最適化

産業応用
G2 グループ

ンテリジェンス
G3 イ
協働形式手法グループ＊リーダー：＊リーダー：
石川冬樹（NII）

K.Czarnecki（Waterloo）＊自動運転を通じた応用と問題同定
ソフトウエア工学＊実務的視点からの学際的理論展開
機械学習
人工知能

UI

導かれる多数の個別的理論の拡張という成果です。さまざまな側面を持つヘテロジニアスシステムとしての物理情報システムへの応用にお「聞き上手な数学者」としてのグループ 0 の介在によって、数学をいて、このような一般論の持つ柔軟性は大きな魅力です。

軸とした異分野協働を実現します。

2017 NII Today │ No.77

09

NEWS

1

情報学の最前線を分かりやすく解説
平成 29 年度市民講座「情報学最前線」スタート

平成 29 年度市民講座「情報学最前線」

心理アンケートから学習者の個性を分析がスタートしました。情報学最前線は、国し、人工知能がそれぞれの学習者に最適な立情報学研究所等の研究者が、情報学分野

学習機能とインセンティブ機能を推薦するの最先端の研究や旬な話題について、広くという学習アプリです。
「能力を褒められ一般の方々にわかりやすく解説する無料のたい人がいれば、努力を褒められたい人も公開講座で、今年度は 7 回開催します。

いる。それぞれの個性に合ったインセン

7 月 12 日に開催した第 1 回は、アーキ

ティブを付与することで、学習者の意欲をテクチャ科学研究系 坂本一憲助教が「や高めることができると考えています」と話る気を引き出す人工知能 ─ 個性を活かししました。

て学習意欲を高める AI ─」と題して講義しました = 写真（上）。

第 2 回は、8 月 25 日に開催しました。
横浜国立大学 大学院工学研究院 小坂英男

坂本助教はまず、学習者はさまざまな個

教授が「ダイヤモンドと量子情報 −テレ

性を持っており、個性によってそれぞれ有ポーテーションから量子認証まで−」と題

効な学習方法が異なる、ということを心理し、ダイヤモンドを利用した最新の量子技学研究の事例を用いて説明しました。坂本

術について講義を行いました = 写真（下）。

複合欠陥のことを NV 中心といいます。NV

助教は、欲望を一時的に抑えることができ

小坂教授は、本研究所量子情報国際研究セ

中心は、光の最小単位である光子の量子状

る「自制心」を持つ子どもの方が、自制心

ンター（センター長：情報学プリンシプル研究系

態を電気の最小単位である電子へと量子テを持たない子どもよりも将来、社会的な成根本香絵教授）が取り組む新学術領域「ハイレポーテーションの原理で転写し、磁気の功を収めやすいという「マシュマロ・テス

ブリッド量子科学」の研究メンバーです。

最小単位であるスピンとして保存する天然ト」について説明し、自制心が成功におけ小坂教授はまず、世界各国で量子コンの量子メモリとなります。このようなダイる重要な要因であることを示しました。まピュータや量子暗号通信ネットワークの研

ヤモンドの特殊能力は、量子暗号通信の長

た、自制心を鍛える上で「動機付け（モチ究開発が高速で進化していることを紹介

距離ネットワーク化に貢献する量子中継

ベーション）」が重要であること、動機付け

し、量子情報技術はこれからとても身近にや、パスワードや証明書発行の不要な量子には「適切な報酬（インセンティブ）の付与」

なる技術であると述べました。次に、室温認証などを可能にし、モノのインターネッが必要であり、それは学習者ごとに異なるで量子の世界を保持できるダイヤモンドをト（IoT）の安全性を量子力学と呼ぶ物理法ということを説明しました。

材料に用いた量子情報技術について説明し則で絶対的に保証することに応用できま

次に、このような心理的傾向に情報科学ました。ダイヤモンドは最も貴重な宝石とす。最後に、小坂教授は「量子を使ってセ者としてアプローチし、学習者ごとに最適して知られますが、量子と呼ぶとても壊れキュリティを強化し、超スマート社会におな学習方法を提供する人工知能（AI）技術やすい状態を長く保持する量子結晶としてけるみなさんの安全を守ることが量子の使を搭載したソフトウエアを開発しているこも貴重です。ダイヤモンドの結晶中、本来命だと考えています。10 年、20 年かけてとを紹介しました。このソフトウエアは、は炭素（C）があるべきところに窒素（N）

それを実現したいと考えています」と結び自尊感情や注目欲求、競争心などに関するが置き換わり、その隣に空孔（V）がある

ました。

NEWS

2

人工知能技術搭載の学習アプリやプライバシーバイザーを展示「イノベーション・ジャパン 2017」に出展、「JSTフェア」も

NII アーキテクチャ科学研究系 坂本一憲

スマモチのデモを体験した来場者からは、助教は、8 月 31 日、9 月 1 日に東京ビッ「社員研修に使ってみたい」という声が多グサイトで開かれた「イノベーション・

く聞かれました。

ジャパン 2017 ～大学見本市 & ビジネス

また、同時に、「JST フェア 2017 ～科

マッチング～」に出展し、人工知能技術を学技術による未来の産業創造展～」も開

使って学習意欲を引き出すアプリ「スマモ催。国立研究開発法人科学技術振興機構

チ」についてポスター展示やデモを行いま（JST）の産学連携マッチングイベント「新した = 写真（上）。

技術説明会」をきっかけに商品化された事「スマモチ」は、心理アンケートやアプ例として、NII 情報社会相関研究系 越前 功

リの操作履歴などからユーザーの個性を分教授が研究開発した顔検出妨害技術を、福析して、学習意欲が高まる最適な設定を推

井県鯖江市の眼鏡製造技術を活用して商品薦する人工知能技術を搭載した学習アプリ

化した眼鏡型装着具「プライバシーバイです。タブレットやスマートフォンによるザー」が紹介、展示されました＝写真（下）。

10

ニュース

NEWS

3

「ERATO 感謝祭 Season IV」開催
トップ会議に採用された論文を多数発表

NII 情報学プリンシプル研究系 河原林健
一教授が研究総括を務める「JST ERATO
河原林巨大グラフプロジェクト」は 8 月

3 日、4 日の 2 日間、本年の情報系トップ
国際会議に採用された論文を発表する研究
成果発表会「ERATO 感謝祭 Season IV」
を開催しました。
「河原林巨大グラフプロジェクト」は、平成 24 年（2012 年）10 月に国立研究開発法
人 科学技術振興機構（JST）の戦略的創造研究推進事業・総括実施型研究（Exploratory
Research for Advanced Technology=ERATO）に「ERATO 感謝祭 Season IV」で発表を行った若手研究者や大学院生たち。前列左から 4 人目が河原林教授採択された研究プロジェクトです。日々膨張するネットワークを点と辺で構成されたも取り組んでいます。

河原林教授は「講演者は情報系トップ国「巨大なグラフ」（ビッグデータ）と考え、最プロジェクト最終年度となる今回は、全際会議に採用された論文の筆頭著者である

先端の数学的理論を駆使して諸課題の解決

国から集結した優秀な若手研究者や大学院大学院生やポスドクが大部分を占めておに役立つ高速アルゴリズムの開発をめざし

生らが、理論計算機科学、データマイニン

り、やっとワールドスタンダードに近づいています。また、基礎研究による日本のコ

グ、機械学習、人工知能、自然言語などのてきたと実感している。今後もこの傾向がンピュータサイエンスの底上げに貢献する分野について、これまでで最多となる 32

続くようがんばってほしい」とエールを送ため、さまざまな分野の若手人材の育成に件の発表を行いました。

りました。

NEWS

4

日本とアジアの学生

科学技術を通し交流「さくらサイエンスプラン」で留学生受け入れ

国立情報学研究所は 7 月 3 日から 21 日研究機関、企業が必要とする海外の優秀なまで、「日本・アジア青少年サイエンス交

人材を育成することを目的として、国立研

流事業（さくらサイエンスプラン）」により、

究開発法人科学技術振興機構（JST）が実

中国の上海交通大学、中国科学技術大学、施。本研究所は、3 年連続で同事業に採択

タイのチュラロンコン大学、ベトナムのハされました。

「さくらサイエンスプラン」で来日した留学生たち。
前列右から、指導にあたった米田友洋教授、岡田仁志
准教授、胡 振江教授

ノイ工科大学から学部及び修士の学生計

留学生たちは約 3 週間にわたり、担当の歩みに触れながら、交流を深めました。

10 名を受け入れ、研究指導を行いました。

教員の指導を受けながら研究に取り組みま

最終日は、留学生が研究成果を発表し、さくらサイエンスプランは、未来を担うした。また、本研究所が情報学専攻を開設

お互いの研究について活発に意見交換を行

アジア地域と日本の青少年が科学技術の分する総合研究大学院大学の学生とともに日いました。留学生からは、「将来は日本で野で交流を深めるとともに、日本の大学や

本科学未来館などを訪れ、日本の科学技術研究をしたい」といった声が聞かれました。

SNS「これいいね！」

Facebook、Twitter アカウントの最も注目を集めた記事（2017 年 6 月～ 8 月）

国立情報学研究所 NII（公式） Facebook
www.facebook.com/jouhouken/

本年 11 月 15 日から開講し、受講受け付

る最新 AI システムを開発／国立情報学研

けを 8 月 23 日に開始します。本研究所の究所と国文学研究資料館による共同研究▶ オンライン講座「オープンサイエンス

MOOC 講座開講は今回が 2 回目です。詳

時代の研究データ管理」開講／ JMOOC

細は以下のページをご参照ください。

の公認プラットフォーム「gacco」でhttp://www.nii.ac.jp/news/release/

国立情報学研究所は、一般社団法人 日本

2017/0818.html（2017/08/18）

オープンオンライン教育推進評議会（JMOOC） 公認の配信プラットフォーム「gacco」で、無料オンライン講座「オープンサイエンス時代の研究データ管理」を（2017/06/08）

つぶやくビット君@NII_Bit

Twitter

NII 研究 100 連発の MC をしてくれた池澤あ
Twitter

やか（ @ikeay ）さんとだびっと！ #NIINow

スケッチや画像から古典籍画像を検索でき＊記事の本文は一部編集・省略しています。

国立情報学研究所 NII（公式）@jouhouken（2017/06/10）

2017 NII Today │ No.77

11

「ACM チューリング賞」50周年を記念した式典が、2017年6月にサンフランシス

Essay

コで開催されました。計算機科学分野の国際学会「ACM（Association for Computing

ACMチューリング賞
50周年を祝って

Machinery）」によって創設され、計算機科学におけるノーベル賞として知られている

本賞は、創設から50年が経ち、この分野への功績により今までに64名が受賞しています。式典では、計算機科学に関わる多様なテーマについて、過去の受賞者を交えパネルディスカッションが行われました。ACM のウェブサイトでは、それらすべてのビデオをご覧いただくことができます。（http://www.acm.org/turing-award-50/video）
式典の中のドナルド・クヌース博士（1974年受賞者）の講演「知識の集積としての

喜連川 優

Masaru Kitsuregawa

計算機科学」を情報処理学会学会誌（情報処理 Vol.58 No.11 Nov. 2017）の特集でも取

国立情報学研究所 所長

り上げています。クヌース博士は、計算機科学の黎明期より活躍してきたこの分野を代 表 す る 研 究 者 で あ り、 日 本 語 訳 も 出 版 さ れ て い る “The Art of Computer

Programming” という本の著者として知られています。この著書は、数多くのアルゴリズムとその計算量を含む分析をカバーしていて、計算機科学における金字塔となっており、その内容に関してクヌース博士は1974年にチューリング賞を受賞しています。
プログラミング技法から画期的な電子出版ツールまで幅広い分野におけるコンピュータ科学への多大な貢献をされた博士は、講演の中で、「計算機科学には、数学と同じように、私たちが研究課題を創案できるという特権があります。自然界が決めた方向に進む必要はなく、自分で研究分野を作り出し、独自の言語、公理などをデザインできるのです」と振り返っています。NII のウェブサイトでも、クヌース博士の講演録を公開していますのでぜ
ひご覧ください。
（http://www.nii.ac.jp/about/upload/acm_NIIToday77.pdf）

講演するドナルド・クヌース博士（ACM ウェブサイトより）今後の予定
10月3日～ 6日│ CEATEC JAPAN 2017（出展）

幹細胞治療部門 特任教授、スタンフォード大学 教授）、「ベー

10月8日│大学共同利用機関シンポジウム 2017（出展）（演奏：ヴァイオリ
トーヴェン ～ ロマン派音楽への先駆」

10月18日│市民講座「情報学最前線」第 4 回「動きをデザイ

ニスト 大津純子、ピアニスト 岡田知子、チェリスト 渡部玄一）（講ンする科学 ─制御屋さんのモノの見方と考え方─」

11月16日│市民講座「情報学最前線」第 5 回「時代を映すイ

師：情報学プリンシプル研究系 岸田昌子 准教授）＝詳細、お申（講
ンフラ ─電話から学術情報ネットワーク SINET ─」

し込みは、以下のページで。
http://www.nii.ac.jp/event/shimin/
10月末│第 2 回 SPARC Japan セミナー 2017 ＝詳細は http://
www.nii.ac.jp/sparc/ で。
11月7日～ 9日│第 19 回図書館総合展（後援・出展）
11月11日│軽井沢土曜懇話会 第3回「iPS細胞から臓器を作る：

師：アーキテクチャ科学研究系 栗本 崇 准教授）

12月12日│市民講座「情報学最前線」第 6 回「ウェブ上の膨大な画像・映像・音楽からの知識発見 ─マルチメディ（講師：コンテンツ科学
ア情報で暮らしをもっと楽しく─」
研究系 ユ イ 助教）

12月13日～15日│大学ICT推進協議会2017年度年次大会（出展）

国境を跨いだ挑戦」（講師：中内啓光 東京大学医科学研究所

表紙の言葉

今回、プロジェクトのテーマの核心である「メタ」（高次の）という考え方を、ロボット自身がロボットを組み立てたり検査したり、といった状況になぞらえて描きました。難しい概念を、少しでも具体的に感じていただければと思います。

情報から知を紡ぎだす。 国立情報学研究所ニュース［NII Today］第 77 号 平成 29 年 9 月「NII Today」で検索！

発行│大学共同利用機関法人 情報・システム研究機構 国立情報学研究所〒101-8430 東京都千代田区一ツ橋 2 丁目 1 番 2 号 学術総合センター
発行人│喜連川 優 編集長│佐藤一郎
表紙画│城谷俊也 編集│田井中麻都佳
制作│株式会社マツダオフィス／サイテック・コミュニケーションズ

本誌についてのお問い合わせ│総務部企画課 広報チーム
TEL│03-4212-2028 FAX │03-4212-2150 e-mail│kouhou@nii.ac.jp

情報犬ビットくん（NII キャラクター）

http://www.nii.ac.jp/about/publication/today/