ソフトウェア工学と人工知能の技術を融合し
プログラミングに革新的な変化をもたらす
情報科学研究科 情報理工学専攻
複合情報工学講座 知能ソフトウェア研究室・教授
工学博士栗原 正仁
プロフィール
1978年 北海道大学工学部卒業。1980年 北海道大学大学院工学研究科情報工学専攻修士課程修了。1986年 工学博士（北海道大学）。1980年より北海道大学助手、講師、助教授を経て、1996年に北海道工業大学教授。2002年 北海道大学大学院工学研究科教授、2004年同情報科学研究科教授。2010年度～2013年度同研究科長。1990年情報処理学会創立25周年記念論文賞、2011年電子情報通信学会論文賞受賞。情報処理学会、電子情報通信学会、人工知能学会、日本知能情報ファジィ学会、日本ソフトウェア科学会所属。
ソフトウェア工学と人工知能の技術を融合
知能ソフトウェア研究室ではどのような研究をおこなっているのですか。
栗原 本研究室では、ソフトウェア工学分野と人工知能分野にまたがる研究を行っています。ソフトウェア工学とは、ソフトウェアをつくる技術者たちを支援し、より簡単に、より確実にソフトウェアを開発できるようにするための技術です。ソフトウェア開発には高度に専門的な知識・技術が必要で、人間の知恵や経験に頼る部分が大きい分野です。それをより簡単に作ることは、技術者の労力の軽減のみならず、開発スピードの短縮などビジネス的な側面でも非常に重要です。また、金融や交通など私たちの生命・財産に関わるシステムでは、何よりも信頼性の高さが求められます。こうしたニーズに答えるため、ソフトウェアを作る際に技術者をサポートするための各種のツールが開発されており、それらの研究分野をソフトウェア工学と呼んでいます。
本研究室では、まだ実用化されていない領域の技術や手法を開発すると同時に、人工知能の技術を取り入れたより高度なソフトウェア工学の実現を目指しています。ソフトウェアの開発には高度な知能が必要とされますが、その知能的な部分はほとんど機械化されていません。技術者の知能に頼っていた部分をコンピュータに肩代わりさせるため、人工知能の技術を応用しようというのが本研究室の特長です。
あいまいなキーワードからソースコードを自動生成
具体的にどのようなテーマがあげられますか。
栗原 本研究室では幅広い領域で数多くの研究を行っていますが、その中から2つご紹介します。まずひとつは「キーワードプログラミングシステム」です。これは学生のアイディアから生まれたものです。ソフトウェア開発の中心は、コンピュータが理解できるプログラミング言語によって、コンピュータへの指令書であるプログラム（コード）という文書を作成するプログラミングという作業です。現在のプログラミングでは、ライブラリやフレームワーク、参考書、ウェブサイトなどに存在する既存のコードを再利用して自らのコードを記述するのが一般的です。しかし、それらのライブラリやAPI群は巨大かつ複雑であるため、ユーザが記憶したり検索したりして活用するのが非常に困難です。これに対し、ユーザが必要とするコードスニペット（コードの断片）を抽出するコードサーチエンジンや、ユーザが現在編集中のソースコード情報を利用して、現在位置で必要なコードを補完するコードコンプリーション（コードの自動補完）という機能が利用されています。
私たちは、これらの機能をさらに進化させ、ソースコードの文脈から最適なコード片の候補を自動生成し、最も正解に近い候補を上位に表示するシステムを開発しました（解説1）。このシステムの特長は、あらかじめ用意されたライブラリから検索・抽出するのではなく、プログラミング言語の文法規則に則って人工知能技術が候補を作りだしている点です。プログラミング言語の型名に拘束されることがないため、プログラミング言語の文法について詳細な知識が乏しくても効率的にコーディングすることができます。さらに記憶があいまいで正確なキーワードが入力できない場合も、コンピュータが推論して候補の一覧を表示する機能を開発・実装しました。
帰納的定理証明によるソフトウェアの検証
他にはどのような研究がおこなわれているのですか。
栗原 先ほどもお話したようにソフトウェア工学はソフトウェアを効率よく確実に開発する技術であり、人命や財産に関わるシステムなどはプログラムの「正しさ」が極めて重要です。そのため、実際に動かしてみて期待通りの動作をするか、安全であるかなどのテストをするのですが、すべての状況をもれなくテストすることはほぼ不可能で、部分的な正しさを確認するテストを行うのが一般的です。時折、大規模システムのトラブルなどがニュースになるのも、テストでは検証しきれなかった事態が起きたためです。
テストよりも一歩進んだ検証の手法として「定理証明」があります。もともとは数学の世界で数式の正しさを証明するものですが、これをプログラムに当てはめ、数式と同じようにプログラムの正しさを証明しようというのがソフトウェア工学における定理証明です。
そのためには、ソースコードを数学のように扱える形式に書き換える必要があり、さらにそれをコンピュータで計算できるようにしなければなりません。数学の定理をコンピュータで証明することは人工知能の分野で50年以上前から研究が行われていて、ここでもソフトウェア工学と人工知能技術の融合が新たな可能性をもたらしています。
一般的なプログラムは、例えばJavaのように、英語によく似た単語が使われており数式とはかけ離れています。このままでは定理証明には使えないので、本研究室では、数式に近い関数型プログラミング言語（解説２）をベースにした「項書換え系（解説3）」という疑似的なプログラミング言語によってプログラムを記述します。その上で、プログラムが満たすべき性質を、数学的帰納法（解説4）によってコンピュータで自動的に証明し、ソフトウェアの性質や正しさの検証を行います。
項書換え系のプログラミング言語で記述されたプログラムの性質を、数式の帰納的定理と同じような方法で記述し、それをコンピュータで自動証明する。それが本研究の重要なポイントです。現段階では、ソフトウェア全体を完全に保証するわけではありませんが、定理証明によって裏付けられた部分は自信を持って「正しい」と言うことができます。現代社会では、ソフトウェアの品質を客観的に評価することがますます重要視されており、定理証明によるソフトウェアの検証はソフトウェア開発にとって不可欠な技術になると考えられます。また、関数型プログラミング言語や定理証明の知識・技術をもった人材の必要性も高まると予想され、大学における教育にも力を入れていきたいと思います。
解説
解説１：キーワードのあいまい一致と分割を導入したキーワードプログラミングシステム
統合開発環境（IDE）に付加して使用することができるキーワードプログラミングシステムを開発・実装。プログラムコードを入力する際、コードの一部を入力するだけでGoogleなどのWeb検索エンジンのようにポップアップに候補の一覧が表示される。人工知能技術を応用することにより、ユーザが正しいスペルをよく覚えていなくても、自信のある文字だけを入力あるいは打鍵数削減のために簡略化した単語を入力するだけで完全型のソースコードを生成することができる。また、1文字程度の間違いや置換や追加が起こった場合も、最適なソースコードがなるべく上位に来るよう設計されている。
解説２：関数型プログラミング言語
計算や処理などを関数の定義の組み合わせとして記述していくプログラミング言語。数学における関数と似た性質を持った関数の定義としてプログラミングを行う。現在の技術による１つのプロセッサの能力向上には限界がある（ムーアの法則）ため、複数のコアにより並列計算を行うマルチコア・プロセッサが普及してきている。それに合わせて、計算を逐次的に行わせる伝統的なプログラミング言語ではなく、並列計算の記述と実行に適した関数型プログラミング言語が今後普及すると考えられている。Haskellが特に有名。最近は、ErlangやScalaなど、注目すべき関数型プログラミング言語がつぎつぎと開発され、入門書が出版されている。
解説３：項書換え系
関数型プログラミング言語の理論的なモデル。等式（たとえば、ｓ＝ｔ）を左から右、または右から左に向き付けて得られる書換え規則（たとえば、ｓ→ｔ）の集合により計算システムを表現する。たとえば、自然数xより１だけ大きい数をs(x)というデータ表現でコーディングすると、つぎの２つの書換え規則
plus(0,x) → x
plus(s(x),y) → s(plus(x,y))
で定義された関数plusによって、つぎのように、plus(s(s(0)),s(0))は最終的にs(s(s(0)))に書き換えられる。
plus(s(s(0)),s(0)) → s(plus(s(0),s(0)))
→ s(s(plus(0,s(0))))
→ s(s(s(0)))
実際、plus(x,y)はxとyの和を定義しており、上の書換えは2+1=3を計算している。このような計算が、コンピュータ上のデータや命令の具体的な表現とは独立に実行可能であるほか、この書換え規則（等式）に基づいて、関数plusの様々な数学的性質（たとえば、plus(x,y)=plus(y,x)）をコンピュータで自動的に証明する道が開かれる。コンピュータで行われるどのような計算も、必ず項書換え系で表現することができる。
解説４：項書換え系による帰納的定理の証明
項書換え系では、コンピュータにさまざまな関数の定義とそれらの満たすべき性質を与えると、コンピュータが数学的帰納法を用いてそれらの性質の自動証明を試みる。数学的帰納法とは、高校の数学で習ったように、任意の自然数ｎについて成り立つ命題を、(1)ｎ＝１のときに成り立つ、(2)ｎ＝ｋのとき成り立つと仮定するとｎ＝ｋ＋１のときも成り立つ、の２つのことを示すことによって証明を行う方法。実際には、自然数のほかにも、コンピュータのプログラムで扱う様々なデータ（記号、記号の列、構造データなど）に言及する定理を、発見的に自動証明する方法が研究されている。
この技術により、有限個のｎの値を与えてプログラムの正しさをテストすることに加えて、無限個あるすべてのｎについてプログラムをテストしたのと同様の効果が得られる。また、わかりやすいが効率が悪い関数を、わかりにくいが効率が良い関数に定義しなおしたとき、両者が内容的に同じ関数であることも証明できる可能性がある。一般に、数学的帰納法を使わないと証明できない定理（帰納的定理）は、そうでない定理（論理的帰結）よりも自動証明が技術的に難しく、チャレンジングな研究テーマの１つとなっている。
