数理論理学からコンピュータ･サイエンスへ

数学の基礎理論を武器に、ソフトウェアに関わる研究に挑んでいる木村大輔准教授。気鋭のコンピュータ･サイエンティストだ。学生への取材時、彼らの口から「ダイスケ先生は」というフレーズが出た。年齢の近さもあるだろうが、この呼称が木村准教授の親しみやすい人柄、そして指導者と学生の良好な関係を如実に物語っている。
木村准教授が研究の基盤とする『数理論理学』は、非常に難解な “ロジカル学問”だ。
「論理の真偽や構成について研究する論理学は、紀元前から存在する伝統的学問です。数理論理学はその数学版。三段論法や背理法など、人間の論理的思考を数学的手法により探究する学問です。思考や主張を論理式に“変換”し、それが正しいか否かを厳密に証明していきます。現代的な数学は数理論理学を土台として構築されており、この学問の厳密さに支えられていると言えるのです」
木村准教授は中高時代から｢数学が得意で大好き｣で、大学時代にこの数理論理学に出合い深く没入した。だが意外にもプログラミングに関しては、｢大学に入って初めて触れた｣というほど無縁だったという。
「プログラム作成の技術習得も途中で挫折してしまって（笑）。でも数理論理学を学ぶなか、『プログラムって、そもそもどんなものなのだ？』という疑問が膨らみ、それについて考え納得した後は、スラスラとプログラムを書けるようになりました。人間がコンピュータにやらせたいことをさまざまな記号で表す……。プログラムって実は数理論理学と非常に親和性の高い存在だったのです」
こうした経験のなかでコンピュータ･サイエンスに興味を持ち、以降、木村准教授はこの分野の研究に取り組み始めたのだという。

数理論理学を用いた静的な『プログラム検証』とは？

木村准教授が現在、メインテーマとしているのが『数理論理学を用いたプログラム検証』だ。現代社会では、あらゆる場面でソフトウェアが活躍している。スマートフォンやパソコン、銀行のシステム、乗り物の制御……など。それらは人間の手作業で作成されたプログラムによって稼働するが、“人力”なので当然のことながら、ミスやエラーが出るリスクが生じてしまう。実際、それが原因で多大な損害が発生した例はたくさんある。
「そうした誤りを防ぐため、プログラムが仕様通りであるかを確認する作業がプログラム検証です。その方法には大きく分けて『動的』と『静的』の２種ありますが、我々は数理論理学を活用し、後者の方法でアプローチする研究に携わっています」
ちなみに『動的』とはソフトウェアの開発後、それを実際に作動させて誤りがあった場合にケアしていく方法。現在、各メーカーで行われているのがこの検証法で、膨大な費用と手間がかかるのがネックとなっている。一方、『静的』は作動前にプログラムの内容を入念にチェックし、誤りを見出して正すという検証法だ。
「作成されたプログラムが『仕様通りであること』を数学的に証明し､保証する。それができる機械を作ろうとしているわけです。しかし、伺いを立てれば即座に応えてくれる、という万能の機械は現時点では理論的に不可能です。
万能”は難しいですが、この分野は非常に幅広い領域で、今、世界中で研究されており、我々はとくにメモリの検証にターゲットを絞って研究を進めています」
そして、この研究にはもう一つ重要なポイントがある。それは、『全自動ツールの作成』をめざしている、ということだ。プログラムの検証を全部、機械に任せていては膨大な時間がかかってしまう。そこで人間が力を貸し協力して作業を進める、という方法が浮上するが、大量のマンパワーを必要とするのが難点だ。
「この場合、人間が機械に付きっきりにならなければならず現実的とは言えません。それを念頭に置き、我々は機械だけで作業が進められる『全自動ツール』の開発を目標に置き、研究に携わっているのです」
難題が多く研究はスムーズに進まないが、ようやくある程度、目算が立った状況にまでは達したようだ。

まだまだ未開拓
大きな夢が抱ける研究分野

このプログラム検証に並行させ、より基礎研究色が強い2つの研究も進めている。『関数型プログラミング言語理論』と『型理論』がそれだ。前者は「プログラムって、そもそも何?」という数学者の"原点"的考察からスタートした研究分野だという。
「計算という、人間や機械が行う仕事を改めて考え直し、そこから理論を再構築するという研究です。数学の一分野としての基礎研究の色合いが強いですが、この研究の蓄積によって使い勝手の良い実用的な関数型プログラミング言語ができつつあります。そして実は、全自動ツールの開発はこのプログラミング言語を用いて行われています」
後者は型(数学用語)について考察する研究。ちなみに型とは、前出の関数型をはじめ「多くのプログラミング言語で用いられているデータ型の概念を抽象化した数学的概念。この研究もまた「そもそも、型って?」という考察から始まった研究だという。
「これらの研究は現在、Googleなどのグローバル企業が取り組む研究分野にダイレクトにつながっています。そのため、こうした企業は数学のプリミティブな勉強に取り組んだ人材を欲しているのです。良いアイデア、そして理論的な足腰が備わっていれば世界的企業に就職できる可能性、あるいは自ら起業し大成功を収める、という道も用意されています。そう、まだまだ未開拓で大きな夢を抱ける研究分野なのです」
研究室の学生にも大きな夢を持ってほしいと熱く語る姿が印象的だった。

COMMENT