2023.06.13
ソフトウェア工学やQA(Quality Assurance) に関する様々な角度からの研究について、研究者の方にお話を伺う『QA最前線！』。
デジタルトランスフォーメーション時代といわれ、品質向上・QAの重要性が高まる今。最先端の現場で、どのような研究が行われているのか、教育の現場がどのようになっているのか、注目されている方も多いと思います。
本記事でQA関連の研究者の方にインタビューをして皆さまにお伝えします。今回は、広島工業大学 情報学部 情報工学科の垣内洋介 准教授にお話をいただきます。
今回インタビューを受けてくださった方
- 垣内 洋介 准教授
広島工業大学 情報学部 情報工学科
2007年 大阪大学大学院情報科学研究科 博士後期課程 修了。博士（情報科学）。同研究科助教を経て、2012年より広島工業大学情報学部情報工学科 助教。現准教授。設計自動化、形式検証に関する研究に従事。最近では、形式検証の技術を応用した数理最適化に関する研究も行う。
システムテストを自動化して膨大な手間と時間を削減
――これまでのご経歴や現在、研究されているテーマを教えてください。
2012年に大阪大学から広島工業大学に来て11年です。現在はハードウェア／ソフトウェアの機能検証と設計自動化を中心に研究を進めています。
大学は大阪大学大学院情報科学研究科で博士課程を修了し、同大学で助教として5年ほど働きました。その後、2012年から広島工業大学情報学部情報工学科で働いています。着任時は助教でしたが、現在は准教授になっています。
主な研究内容は、「数理最適化」という分野とソフトウェア工学の話であれば「要求仕様の検証」を行っています。
――数理最適化はどのような研究になるのでしょうか。
数理最適化というのは「最適化」という名前がついている通り、簡単に説明すると「1番良い答えを見つけましょう」という研究です。
現実の問題を数式（数理モデル）として定義し、制約条件を満たしつつ、コストの最小化や利益が最大化されるような変数の値を求める手法です。具体的に例えると、何か問題があったら、それを数式で表現（モデル化）して、それを解かせて解を出すという感じになります。
この解を出すときはいろいろなプログラムを書いている先生方もいらっしゃいますが、私は専用のソフトウェア「ソルバー（※）」を使って、解を求める形になることが多いですね。
例えば「こういう条件を満たしなさい」というのにプラスαで目的関数という解の良さを図るための式を追加で定義し、それが例えばコストであれば最小になるとか、時間であればなるべく短くなるなど、そういう形で解かせて良い解を求めるのが数理最適化という分野になります。
（※）ソルバー......制約条件を満たす解を自動的に求めるソフトウェアツールのこと。一般的に、制約条件は式の形で書かれ、解は変数への値の割り当てとして求められる。
――ちなみにこのソルバーはかなり種類があるのでしょうか。
私が形式検証の研究をやっているときから使っているのは「充足可能性判定ソルバー」というもので、要するに式が満たされるかどうかをちゃんと判定してくれるソルバーです。アカデミックな世界でもコンペがあり、なるべく早く大きい問題を解くことをずっと競っているので、時代とともにかなり性能自体も改善されています。数理最適化の方でも専用のソルバーがいくつかあり、そういう意味では選択肢はたくさんありますね。
――大学の教員紹介ページにも掲載されていますが、ソフトウェアエンジニアやプログラムコンテストでよく見かける「巡回セールスマン問題」との関係はあるのでしょうか？
おっしゃる通り、巡回セールスマン問題は数理最適化の代表的な問題の一つです。TSP（Traveling Salesman Problem）というもので、私も関連する共同研究をさせていただいたことがありました。
巡回セールスマン問題に置き換えることができる問題があるのですが、たとえば企業さんがやっているハードウェアの基盤の接点を順番に押さえながら電気的なテストをするような問題です。要するに接点の導通を1個1個調べていくので、巡回セールスマン問題に帰着できるということで、そういう形で解いていたことがあります。
この巡回セールスマン問題自体歴史のある問題で、厳密的な解を出すことは計算量的に難しいのですが、さまざまな近似解を求める手法が研究されて来ました。
――人々の生活を便利にしてくれそうな研究だと思います。先生が数理最適化に取り組むようになったきっかけを教えてください。
元々の研究がきっかけですね。大学時代からハードウェアの検証をやっていまして、いわゆるデジタル回路というものでVLSIの検証を研究していました。
検証の仕方としては形式検証と呼ばれる方法で、いわゆるフォーマルメソッドというものなのですが、これは「静的テスト」とも言われており、値を回路に入力して出力を見る動的検証とは少し違うんです。この形式検証というのは回路の中身をモデル化します。
実際の回路は全部論理式なので論理式をそのまま自動検証できるんですね。そこで得たモデル検査の知識や手法を最初は数理最適化に適用していこうと研究を始めました。
――どんなときに研究の面白さや、やりがいを感じますか？
やはり、より早く良い答えを出せたときにやりがいを感じますね。
元々、大規模な問題といいますか、コンピュータでも全部網羅探索するのは難しい問題を解きますので、それに対してある程度近似的な解法で、短時間で良い答えが出たときに「よかった！」という感じでモチベーションが上がります。
その時代に即した問題の解を見つける
――研究された技術の成果が社会に与える影響について、どのような点が挙げられるでしょうか。具体的な事例などがあればお教えください。
この分野はさまざまな問題の解決に取り組んでいるので、一概にこれと言うことはできませんが、たとえば最近話題になっているUberEatsのような、クラウドソーシングフードデリバリーですね。数理最適化を使ってクラウドソーシングフードデリバリーの配達者割り当てをやられている方がおられて、「なかなか面白い問題だな、コロナ時代に即した問題だな」と思いました。いろいろな場面でモデル化すればさまざまな社会的な問題に使えるはずなので面白い分野だと思いますね。
あとは、やはり機械学習です。AIが非常に進歩してきているので、そういう分野の研究を援用すれば近似的な解が改善されるのではないかと考えています。
――先日、量子コンピュータをクラウドで利用できるサービスを開始すると発表がありましたが、そういったものを使えば、研究に関してもブレークスルーが進む可能性があるのでしょうか。
確かに計算の方法が変わってモデル化の方法も変えたらうまくいくようになるかもしれないので、さらに一歩進む可能性はあります。ただし、一般人がどれだけ利用できるか、というところに疑問があるので、非常にそういう研究の需要は高いと思います。
社会の中では、地道な努力の上に製品が成り立っている
――現在の研究は将来的にどのような発展が期待できますか。また、どのようなインパクトを与えたいとお考えでしょうか。
基礎研究をやっている側としては難しいところなんですけれども、要求仕様の研究に関しては今まで人間が見て使うためのものを検証可能なモデルとして使いましょうというものなので、そういう検証やテストの一助になれば、と思っています。
数理最適化に関しても適切な問題が見つかれば、それを解くための手段ですので、いろいろな問題に適用できると思います。
――普段、大学で教えられている学生はどんなふうに育てようとお考えですか。
これは一貫して「自主独立」を掲げています。学生には自分で問題を発見して、自分で問題を解決できるようにやってくださいというメッセージを常に伝えるようにしていて。
やはり日本の学生さんは、高校や大学も低学年は教師に与えられて、それをやる癖がついているんですよね。なので、特に研究に関しては「自分でやるんだよ」と、うちの研究室ではテーマなんかも基本的には自分で決めさせています。学生のやりたいことがバラバラで、とりとめもないような研究室になっています。
社会の中では、地道な努力の上にいろいろな製品が成り立っているので、我々アカデミアの者としては、開発エンジニアの方にもテストエンジニアの方にも非常に敬意を払っています。これからも頑張ってくださいという想いがあります。
――本日はいろいろお話をしてくださり、ありがとうございました。
