最先端研究を訪ねて


【ソフトウェア】

プログラミング言語

「ソフトウェア検証」の研究、機械的に間違いが検出できるプログラミングを作るために「数学」を活用

五十嵐淳先生

 

京都大学

工学部 情報学科 計算機科学コース(情報学研究科 通信情報システム専攻)

 

研究者同士で議論
研究者同士で議論

 

◆どのような研究ですか

 

人工知能の技術は発展し、オンラインショッピングなどの社会インフラや、医療機器、ロケットなどにも取り入れられています。

 

しかし人間の書いたプログラムには間違いがつきものです。間違いはソフトウェアの誤動作につながり、重大な損害を引き起こす恐れがあります。私はこうした間違いがないことを保証するため、数学に基礎づけられたソフトウェアの間違いを検証する世界最先端の研究をしています。

 

 

◆どんな成果が上がりましたか

 

プログラムの開発においては、書かれたプログラムが本当に安全なプログラムなのか事前に検査することが何より難しいのですが、新しいプログラムの事前検査の方法を開発しました。その結果は、現在、Java という広く使われているプログラミング言語に取り入れられています。

 

その方法とは、プログラムが間違いをしないパターンを数学的に読み取り、さらに間違いが混入してもそのチェックが自動的にできるようなプログラミング言語の開発です。人の経験や勘に頼らずにソフトウェアの誤動作を防ぎ、様々なソフトウェアの質を上げることができるようになります。

 

◆その研究が進むと何が良いのでしょう

 

人工知能の社会が到来し、ソフトウェアは大きな進歩を遂げました。社会基盤の一部としてのソフトウェアは、うまく動いて当たり前、普段はほとんど意識する必要のない存在であるべきですが、現在のソフトウェアは、頻繁に不具合を起こして、その存在を我々に見せてしまっているのが現実です。私たちの研究は、ソフトウェアの完全な「見えない化」の実現という、最も困難なソフトウェア工学の課題の解決に貢献できると考えています。

 

 SDGsに貢献! 〜2030年の地球のために

コンピュータは現代社会の中核を成す技術のひとつで、システムに不具合があれば、人命を危険にさらしかねない時代です。そのような状況下で、特にソフトウェアに由来する不具合を減らす、できればなくすための一助になる研究をしているつもりです。しかしながら、いつも「SDGsに貢献しなければ…」と深刻に考えているわけではなく、数学的なパズルを解いている気分で、楽しく研究をしています。

 


 きっかけ

自分が研究者になろうとは、卒業研究で研究室に配属されるまで、いや、されてからもしばらくは、全く思ってもいませんでした。

 

博士課程に進学したのは、研究で取り組む問題そのものが面白かったことももちろんですが、既に進学している先輩方の大変な充実ぶりが、大きなきっかけとなりました。

 

博士課程の学生の時、研究発表をするためにパリへ。人生初めての海外旅行でした。「おお、よい研究をしていると、海外のいろいろなところに行けるみたいだぞ!?」と味をしめたのは、その後も研究を続ける(不純な)原動力になっている気がします。(このアンケートに回答している時点では、新型コロナウイルスのせいで旅行できない日々が続いていますが…)

 


 この分野はどこで学べる?

「ソフトウェア」学べる大学・研究者はこちら (※みらいぶっくへ)

 

その領域カテゴリーはこちら↓

13.IT・AI」の「53.ハード・ソフト(OS、アプリ)、プログラム系」

 


 もっと先生の研究・研究室を見てみよう
 学生はどんな研究を?

プログラム検証手法の改良や、新しいプログラミング言語(既存の言語の機能拡張も含む)の設計と作成などに取り組んでいます。

 

 OB/OGはどんなところに就職?

◆主な業種

 

・コンピュータ・情報通信機器

・ソフトウェア・情報システム開発

・大学・短大・高専等、教育機関・研究機関

 

◆主な職種

 

・基礎・応用研究、先行開発

・システムエンジニア

 

◆学んだことはどう生きる? 

 

システムエンジニアであれば、「そもそもソフトウェアシステムの正しさとは何か」といったことに常に意識を向けながら開発をするといった形で、学んだことが活かされているのではないかと考えています。

 


 先生からひとこと

理論研究は難しい!と言われがちで、確かに抽象的で難しい、とっつきにくい所があります。しかし、この分野の研究でやっていることは、自分でパズル問題を作って、それを解いているようなものです。

 

世界中の人が長年頭を悩ませているパズルもあれば、ごく一部の人だけが興味のあるパズルもあります。自分でパズル問題を作るといっても、たいていは既に知られているパズルのルールをちょっとだけ変えて、それでも解けるかとかその程度ですが、それでも自分の作ったパズルが人に面白がってもらえると、何だか嬉しいものです。

 

そのパズルが、現代の情報社会を支えるコンピュータ技術と結びついて、ひょっとしたらとっても役に立つのですから不思議です。

 

 先生の研究に挑戦しよう!

・現代の暗号技術について調査してみよう。DES暗号(今は少し古くなってしまいましたが)や公開鍵暗号系RSAの原理、RSA暗号を使ったデジタル署名の原理くらいなら高校生でも頑張れば十分理解できます。

 

・「計算とは何か」という問いに答えるためにチューリング機械などの「計算モデル」が数多く提案、研究されてきました。その中でもコンウェイが考案したライフゲームは単純な原理に基づきつつも、複雑なことができて、かつ、見た目にも楽しいものです。ライフゲームやその一般形であるセル・オートマトンについて調べてみる、遊んでみるのは面白いと思います。(巷には、ライフゲームを動かすためのプログラムもいろいろあると思います。)

 


 中高生におすすめ

CODE コードから見たコンピュータのからくり

Charles Petzold(日経BPソフトプレス)

広い意味での計算機の原理に関して、一般向けに丁寧に書かれた本で、コンピュータが非常に単純な仕組みを非常にたくさん積み重ねることでできていることがよくわかる。多くは機械的な仕組みに関する解説だが、ソフトウェア研究に興味がある人も、まずは、コンピュータがどのように構成されているかを知ることは非常に大切だ。



ゲーデル、エッシャー、バッハ あるいは不思議の環

ダグラス・R・ホフスタッター(白揚社)

だまし絵で知られるエッシャー、バロック時代後期の大作曲家・バッハは有名だが、ゲーデルの名前をご存じだろうか。ゲーデルは20世紀の大論理学者。「論理学って何?」という人はもちろん、パズルが好きな人、「この3人の関係がさっぱり想像つかないけれど、エッシャーの絵は不思議で好き」という人も、一度手に取ってみて欲しい。話題は、論理学、計算機科学、哲学、人工知能、音楽など多岐に渡る。内容が難しくても気にせず、最初は途中に出てくるアキレスと亀の対話篇(漫才?)や、エッシャーの作品を眺めるだけでもいい。スルメのようにだんだん味が出てくる本である。



暗号解読

サイモン・シン(新潮文庫)

子どもの頃、友達とだけ通じる暗号を使って、秘密のメッセージ交換をしたことはないだろうか。ローマのカエサルの昔からナチス・ドイツの暗号機「エニグマ」に至るまでの暗号創造と暗号破りの戦いについて、はたまた現在のコンピュータに不可欠なディジタル暗号の技術について、そして原理的に絶対に破られることのない未来の技術「量子暗号」まで、暗号の過去、現在、未来が全て分かる。暗号が世界にどんな影響をもたらしてきたのか、これからどう使われていくのか、覗いてみよう。



科学哲学の冒険  サイエンスの目的と方法をさぐる

戸田山和久(NHKブックス)

学校で習う科学法則って何で正しいの?原子なんて目に見えないのにどうして「ある」って言えるの?学校で教わったからといってそれがなぜ「正しい」と言えるのか、気になったことはないだろうか。科学哲学は、「科学はどういう学問で、どうして何が正しいかを明らかにしていく(ように見える)のか」について考える学問分野。上のような疑問を持ったことがない人も、本書を読むと、世の中には疑り深い・ひねくれた・変なことを考える人もいるんだな、と目から鱗が落ちること間違いなし。

 



 先生に一問一答

Q1.日本以外の国で暮らすとしたらどこ? 

シンガポールは食べ物が美味しいし、英語が通じるし、緯度が低いため台風も来ないそうなので、一度住んでみたい気がします。

 

Q2.一番聴いている音楽アーティストは?

ジャンルの分け隔てなく色々聴くのでしぼり辛いのですが、なんだかんだで、フランク・ザッパを聴く時間が、一番長いようです。彼の音楽が様々なジャンルを折衷しているからかも知れません。

 

Q3.大学時代のアルバイトでユニークだったものは?

老舗の海苔屋さんでの接客です。いろいろなお客さんが来るので、社会勉強になりました。また、箱や缶の包装がうまくなりました。