コンピュータは数学者になれるのか？――大学数学における自動定理証明

• 研究課題/領域番号: 20K11679
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分60010:情報学基礎論関連
• 研究機関: 京都大学
• 研究代表者: 照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
• 研究期間 (年度): 2020-04-01 – 2025-03-31
• 研究課題ステータス: 交付 (2022年度)
• 配分額: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円); 2024年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2023年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2022年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2021年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2020年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
• キーワード: 自動定理証明 / 線形論理 / 数理論理学 / 実線形算術 / 自動定理生成

研究開始時の研究の概要

数学における自動定理証明の成功例は、ごく限られている。この現状を打破するための第一歩として、大学数学、とくに線形代数に特化した自動定理証明の研究を行う。理論面では数学基礎論・コンピュータ科学論理（とくに最近の証明論）に由来するアイデアを援用する。また、有意味な定理を大量に自動生成する方法を考案し、機械学習に役立てる。最後に「楽しいコンピュータ証明」を実現するために、わかりやすい教科書を執筆し、簡易的な証明システムを公開することで多くの人に自動定理証明を身近なものとして体験してもらう。それにより、数学における自動定理証明の研究機運を次第に高めていきたいというのが目論見である。

研究実績の概要

本研究は、数学における自動定理証明（ATP）に関わるものである。現在主流なのはTPTP問題集、MizarやFlyspeck等、広範な数学分野をカバーする大規模ライブラリにのっとった研究である。一方で本研究はこれらとは一線を画し、数学の中でも特定分野（線形代数）に特化したATPの基礎理論を構築すること、そのために数学基礎論由来の深い成果を援用すること、そしてたとえ控えめであっても一般人の目にわかりやすい成果を挙げることを目標としている。

2022年度は、Satallax等の汎用型システムで採用されているSAT還元の手法についての研究を進め、線形算術との融合に取り組んだ。また派生的課題として、素代数的束の圏の線形分解により得られる線形論理のモデルに焦点を当て、単純型ラムダY計算の計算複雑性へ応用する手法を検討した。またクリーネ代数とトレースつきモノイダル圏の関係について調べ、線形論理の新たなモデルを得る研究に着手した。最後にATPの前処理において重要な役割を果たすスコーレム化について、実効的スコーレム化などの亜種の考察を行った。

現在までの達成度 (区分)

3: やや遅れている

理由

依然としてATPシステムの実装面における問題（SAT還元と単一化に基づく等式推論、および条件的等式の取り扱いを融合させる点）が解決していない。別のアプローチに取り組む必要があるかもしれない。
成果普及については、ATPのSAT還元を中心として執筆を進めているが、新規性を目指す一方、基礎知識も組み込まなくてはならないためその兼ね合いに苦慮している。
派生的テーマについては、クリーネ代数など専門外の知識が必要のため、調査を進めている段階である。

今後の研究の推進方策

ATPの実装面における問題を解決するため、別のアプローチも試みる。また昨年度台頭した派生的テーマにも重点をおき、クリーネ代数と線形論理の関係や精密なスコーレム化など専門外の分野へも研究範囲を広げる予定である。