プログラミング言語と自動証明

廣川研究室　HIROKAWA Laboratory
准教授：廣川 直（HIROKAWA Nao）

E-mail：
［研究分野］
情報科学、情報科学基礎、項書換え、定理自動証明
［キーワード］
理論計算機科学、記号計算、関数型プログラミング言語、自動証明、停止性、計算量解析

研究を始めるのに必要な知識・能力

集合の基本的な知識、またはプログラミング能力のどちらか一方が必要です。前者に関しては授業科目のI120（基礎論理数学）で必要な知識を修得することができます。プログラミング言語やパズルの自動的解法などに興味があると楽しく研究できると思います。

この研究で身につく能力

当研究室では数学とプログラミングの両方ができる人材の育成を目指しています。研究者を目指す人はもちろん、企業の研究・開発職に行く人もJISやISOといった数学的に記述された文献を読みこなす力が求められています。数式を読み書きする能力、プログラムを数理的に理解し、説明できる能力を研究テーマを通して涵養します。

【就職先企業・職種】 情報通信関連の研究機関、システムエンジニアなど。

研究内容

　強力なプログラミング言語機能やプログラムの自動検証技術の実現は、情報社会の発展とその安全を支えるために不可欠です。本研究室では項書換えと呼ばれる等式に基づく計算モデルの研究を行っています。項書換えは関数型プログラミング言語や定理自動証明、Mathematicaのような数式処理システムの基盤理論であり、計算の原理や性質を解明することで、プログラム合成や解析、等式の自動証明や解の自動導出を目指しています。
　最近の研究テーマをいくつか紹介します。

1．自動証明

　数学的な定理を自動的に証明することは人工知能分野の夢といっても過言ではありません。私たちのグループでは特に等式の自動証明について研究を行っています。物理学の運動方程式や制御工学の状態方程式などをはじめ、多くの分野で等式によるモデル化が用いられています。情報科学も例外ではなく、例えば関数型言語ではプログラムを等式の集まりで構成します。ひとたび等式系で表せば、等式から導出される式や方程式の解を調べることで、対象を分析することが可能になります。
■等式の証明
　等式証明の基本は式変形です。式変形を繰り返し両辺が等号で結ばれれば、等号の成立を結論できますが、賢く行わないと変形が延々と続いてしまい証明が終わりません。自動化するには式変形を「賢く」行う必要があります。また証明に有益な補題をどう発見するのかも重要になります。他にも等号の不成立をどう検知するか、反例はどう生成するのかなど、様々な研究課題があり、取っ掛かりやすいテーマだと思います。
■方程式を解く
　実数の連立方程式はガウスの消去法により一般解を自動的に求めることができますが、情報科学分野では項や文字列を対象にした方程式を解きたいことが多々あります。例えば文字列に関する方程式ax = ybは （x,y） = （b,a）, （aab,aaa） などの解を無数に持ちますが、（zb, az）という一般解があります。解を持つ条件や効率的に一般解を導出する系統的な手法を模索しています。

2．計算理論

■停止性検証
　ソフトウェアが応答しなくなったり、突然リソースを使い果たしダウンすることがあります。多くの場合、それらはプログラムが意図せぬ非停止状態に陥ったことに起因します。停止性を自動検証する技術は今世紀に入り飛躍的な発展を遂げました。現在、コンパイラや定理証明システムに組み込めるような軽量かつ実装が容易な停止性検証手法を目標に研究を進めています。
■計算量解析
　停止性からさらに一歩踏み込み、プログラムがどれくらいの速さで動作するか、つまり時間的計算量がどれくらいかを自動的に解析する研究にも挑戦しています。たとえばクイックソートのプログラムを入力に与えると、その時間的計算量であるO（n2）と出力できるような解析技法とツールを目指しています。

主な研究業績

1. Teppei Saito and Nao Hirokawa: Weighted Path Orders are Semantic Path Orders. Proceedings of the 14th International Symposium on Frontiers of Combining Systems, LNAI, pp. 63-80, 2023. Best paper award.
2. Dominik Klein and Nao Hirokawa: Maximal Completion. Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, LIPIcs 10, pp. 71-80, 2011.
3. Kiraku Shintani and Nao Hirokawa: Compositional Confluence Criteria. Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, LIPIcs 228, pp. 28:1-28:19, 2022.