目次
この記事をシェア
※記事に記載された所属、職名、学年、企業情報などは取材時のものです
AIがプログラムを生成する――少し前のSFの世界はもう現実のものとなっている。そのプログラムは人の意図を正確に反映し、正しく動くのか。その信頼性を担保する理論の発展が喫緊の課題となっている。
この「人の意図」と「プログラム」の間にあるギャップに数学的な厳密さを与える研究に取り組むのが、大学院理学研究院の塚田武志教授だ。約40年来の未解決問題を解決し、2024年の千葉大学先進学術賞や2025年の国際会議POPL*の優秀論文賞を受賞するなど、その独創性は高く評価されている。自らの探究心に導かれ道を切り拓く塚田教授に、研究の奥深さと面白さをうかがった。
*Principles of Programming Languages (POPL): 米国計算機学会(ACM) SIGPLANが主催する国際会議。プログラミング言語に関する理論研究を中心に扱い、この分野で最も権威のあるトップ会議の一つとされている。
「論理的な正しさ」と「人の曖昧さ」に導かれて
――現在の研究分野に興味を持ったきっかけを教えてください。
技術者だった父の影響で、幼い頃からたくさんの本に囲まれ、自然と工学に関心を持つようになりました。専門的な知識を得るため高専へ進学し、情報分野と出会いました。
論理学や意味論分野へ関心を持ったきっかけは、15歳から十年以上続けた「競技ディベート」です。競技ディベートとは、与えられた論題に対し肯定・否定の立場に分かれて論じ、審判の前で論理性や説得力を競う競技です。論理の正しさだけを評価したいのですが、実際には審判の解釈や価値観を抜きに判定は不可能です。その経験から「人を論理的に説得するとはどういうことか」といった、言語や論理の本質的な部分に関心を抱くようになりました。
その後京都大学で情報学を学び、プログラミング言語理論を専門とする研究室で出会ったのが「プログラム意味論」です。
――「プログラム意味論」とは？
コンピュータは全てプログラムで動きますが、人間の意図通りに動かない「バグ」が生じることがあります。ゲームならバグを楽しんでもらえることもありますが、飛行機や車の制御システムでは命に関わる重大な問題です。
このようなバグは、人間がプログラムに抱く直感的な認識と、コンピュータの機械的な処理との間に生じるギャップが原因で発生します。このようなズレを防ぎ、プログラムが人間の意図通りに動くことを数学的に厳密に保証すべくこの問題に取り組むのが、「プログラム意味論」です。
約40年未解決だった「線形論理」の数学的基盤の発見へ
――「人間の意図」を「数学的に厳密に扱う」とは、どのように実現できるのでしょうか？
人間の意図がコンピュータに正確に伝わっているかを数学的に保証するためには、まずプログラムの振る舞いを厳密に記述できる数学的な“言葉”が必要です。その強力な手段の一つが、フランスの論理学者 ジャン＝イヴ・ジラールが1987年に提唱した「線形論理」という論理体系です。
線形論理の画期的な点は、論理式を“一度だけ使える資源”として扱う点です。従来の論理体系では、一度証明した事実は自由に何度でも利用できますが、線形理論では一度使うと再利用できません。この「複製を禁止する」という一見不便なルールがあるだけで、論理の構造が整理され、ものごとをより簡単に扱えるようになります。そのため、線形論理は非常に便利で、広く使われています。
――「線形論理」の「線形」とは？
ジラールの提唱した「線形論理」は、証明を行列のように整理できるなど、行列やベクトルを扱う数学の分野である「線形代数」の考え方を参考にして発展してきたことから、その名がつけられました。しかし、その理論の土台となる数の舞台、すなわち「ベクトル空間」*がどのようなものかは、約40年間不明のままでした。
*ベクトル空間: 「平面上のすべての点の集まり」や「空間上のすべての点の集まり」を一般化したもの。各点を「ベクトル」と呼び、ベクトル同士を足したり、ベクトルに数をかけたりすることができる。
――今回の研究で、その根幹を支えるベクトル空間が発見できたと。
そうです。この空間の特徴は、「算数のように足し算が常にできる訳ではない」という点です。この制約があることにより、線形論理の仕組みを正確に把握できることがわかりました。さらにこの空間ではその係数を変えることで、今まで別々に考えられていた複数の理論を一つに統合できます。例えば、量子コンピュータのプログラミング言語も、この考え方で扱うことができます。
――この発見まで、どのような苦労がありましたか。
2018年の時点で既に構想はあったのですが、想像以上に難航しました。当初は半年ほどで形になるはずが、試行錯誤で完成までに3年半ほどかかりました。専門的な話になってしまいますが、この空間の土台となる「基底」という概念をどう定めれば理論が破綻しないかが分からなかったのです。半ば諦めていたのですが、「加群」という分野を勉強していた時に「双対基底」という概念を見つけて、これが使えるということに気付いたことが突破口になりました。
AI時代のすべてのプログラムの信頼性や安全性を最も深い場所から支える
――「プログラム意味論」の発展は、社会にどのような影響を与えるのでしょうか。
プログラム意味論は、直接社会に影響を与えるというよりも、プログラマーさえも普段は意識することのない、さらに奥深くにあるコンピュータ言語の信頼性の担保に関わる分野です。
たとえば、プログラムの目的や出力を変えずに処理を軽くする「最適化」という技術があります。処理時間や負荷を考慮してプログラムの書き換えが行われますが、その際に問題となるのが、プログラムの「意味」が本当に変わっていないかという点です。
先述の通り、人間の「意図」とコンピュータの「処理」にはギャップがあります。プログラム意味論はそれを埋め、最適化後も意味が保たれることを厳密に保証します。これは重要な応用例のひとつです。
――やはりAIがプログラムを書くようになったこの時代、プログラムの安全性の保証は大きな課題なのでしょうか。
これまでは人間が書き、動作確認をするという2軸で信頼性を担保してきました。しかし今後AIがプログラムを書くようになると、一方の軸が失われてしまいます。人間には常識や良心がありますが、AIは仕様をギリギリ満たすだけのプログラムを生成する可能性があります。とはいえ、生成されたプログラムをすべて人間が目で確認することも現実的ではありません。だからこそ、人間の意図と数学的な厳密さをつなぐ「プログラム意味論」を発展させ、その検証ツールを開発したいのです。
――人間の役割がプログラムを「書く」から「読む・検証する」へ変わっていきそうですね。
はい。これからのプログラマーはプログラムを読んで、その正しさを検証する役割がますます重要になっていくでしょう。私たちの研究分野はその基盤として貢献できると考えています。
「不可能だ」と証明されているからこその面白さ
――この研究分野の魅力を教えてください。
大学時代、恩師から「この分野は、1935年にイギリスの数学者アラン・チューリングによって『与えられたプログラムが停止するかどうかを “完璧に” 判定できるプログラムは存在しない』と証明されているからこそ、面白いんだ」と言われたことがあります。完全にはできないとわかっているからこそ、どこまでならできるのか、何ができるのかを探るのが楽しい、と。
実用上は、「完璧」な判定は実は必要ではありません。プログラマーが書くプログラムを扱えれば十分で、チューリングの証明に現れるような “いじわるな” プログラムは扱えなくとも困らないのです。むしろ限界を前提に、現実で役立つ仕組みを考えることに夢がある。そんな分野だと思います。
――今後の研究について教えてください。
今、関心があるのは「因果性」というテーマです。プログラミング言語における因果性とは、時間的な前後関係に近い概念で、命令の実行順序によって生じる問題を扱います。
たとえば、複数のプログラムを同時に実行したとき、命令の順序の相性が悪いと互いに待機状態になり処理が止まる「デッドロック」と呼ばれる現象が起こることがあります。このような複数のプログラムが同時に動く状況での因果性を対象とする研究に、これまでの成果が応用できる手応えを感じ、今まさに取り組んでいるところです。
――最後に、学生さんたちへのメッセージをお願いします。
研究テーマを見つけたいと思ったとき、ゼロから生み出すのはなかなか難しいものです。そんなときはいろいろな本や論文を読みながら、どんなところに引っかかるか、「気持ち悪さ」や「違和感」があるかを探してみてください。
その「気持ち悪さ」を突き詰めていくと、結局本に書いてある通りだったと納得することになるかもしれませんが、もしかしたら違和感を解消する新しい方向を見つけられるかもしれない。何に対してその違和感を持ち続けられるかがその人の個性であり、やがて研究テーマにもつながっていくと思います。
研究は、興味を持ち続けられなければ続けるのが難しい世界です。しかし誰かに背中を押されずとも「やりたい」と思えるテーマに出会えたなら、ぜひ頑張って欲しいです。
● ● Off Topic ● ●
技術者だったお父様の影響はあったと思われますか？
小学生の頃に買ってもらった「電気が交互に点滅する回路のキット」の仕組みが気になり、どうなってるのか知りたいと父に相談したところ、『実用電子回路ハンドブック』など数冊の教科書を渡されました。父は「それを全部読んで回路を丸暗記すればそのうちわかる。うちの新入社員なら3時間にらめっこすればわかる」と言って、答えを教えてくれないんです。それなりに本を読んだり考えたりしてみても結局わかりませんでした。でもそういう環境や、父の影響は大きかったと思います。
革新的な研究を続けるために意識していることはありますか？
私はどちらかというと技術者タイプで、与えられた課題に対してどうやって解決するかを考えるのは好きなのですが、戦略を立てることは苦手なんです。とにかく自分が興味あることだけをやっていたい（笑）。幸運だったのは、自分の力をより価値ある形で発揮させてくれる、素晴らしい研究パートナーに出会えたことかもしれません。
インタビュー / 執筆
谷本 明夢 / Meimu TANIMOTO
東京科学大学理学部物理学科宇宙物理学研究室卒。統計解析やシステム開発系企業にて4年半勤務後、数学者の夫とともに渡米・渡欧。
各地で地域調査やコミュニティ活動に携わる。2020年よりライター・作家として活動を開始。
科学や数学への苦手意識がある方にも届くよう、わかりやすく親しみのある記事作りを心がけている。得意分野は科学、数学、IT、人物インタビュー。
撮影
関 健作 / Kensaku SEKI
千葉県出身。順天堂大学・スポーツ健康科学部を卒業後、JICA青年海外協力隊に参加。 ブータンの小中学校で教師を3年務める。
日本に帰国後、2011年からフォトグラファーとして活動を開始。
「その人の魅力や内面を引き出し、写し込みたい」という思いを胸に撮影に臨んでいます。
