Can Computer be a Mathematician? Automated Theorem Proving in Undergraduate Mathematics

2020 Fiscal Year Research-status Report

• Project/Area Number: 20K11679
• Research Institution: Kyoto University
• Principal Investigator: 照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
• Project Period (FY): 2020-04-01 – 2025-03-31
• Keywords: 自動定理証明 / 数理論理学 / 実線形算術

Outline of Annual Research Achievements

本研究は、数学における自動定理証明（ATP）に関わるものである。現在主流なのはTPTP問題集やMizar・Flyspeck等、広範な数学分野をカバーする大規模ライブラリにのっとった研究である。一方で本研究はこれらとは一線を画し、数学の中でも特定分野（線形代数）に特化したATPの基礎理論を構築すること、そのために数学基礎論由来の深い成果を援用すること、そしてたとえ控えめであっても一般人の目にわかりやすい成果を挙げることを目標としている。
2020年度は、まず先行研究の分析を徹底的に行った。際立ったアプローチのひとつに、大規模数学ライブラリをデータセットとして用い深層学習や強化学習の手法を適用するものがあり、証明成功率の向上などの定量的成果を挙げている。本研究では、このアプローチに潜む問題点（中間補題の発見や帰納法・包括公理の適用が巧妙に避けられていることなど）を洗い出し、対応策を検討した。
また、独自ATPシステムの開発をめぐって試行錯誤を行っている。線形代数全般を対象とするのは時期尚早のため、まずは実線形算術部分をタブロー法に基づいて実装し、簡単な自動定理証明の実験を行った（連立一次方程式の解の存在条件等）。
最後に本研究の目標達成のためには、一般人にもわかりやすいATPの解説書を執筆し、多方面から関心を惹きつける必要がある。2020年度は、ラムダ計算（高階論理の基礎）と単一化アルゴリズム（一階ATPの核心）に関する部分をまとめあげた。

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

ATPシステム実装に難航している。比較的容易だと思っていた実線形算術部分ですでに大きな問題が発生しており、論理推論や等式推論の基盤部分でさらなる工夫が必要となっている。具体的には条件付き等式の取り扱いについてであり、これとタブロー法の相性の悪さは以前から認識していたが、実験を通してその問題点がいっそう明確になった。
本研究のアプローチの核心にある証明テンプレートのアイデアについては、基礎研究を進めているが未だ成果は出ておらず、ATPシステムにも組み込めていない。自動定理生成のアイデアについても、未だ試行錯誤の段階である。

Strategy for Future Research Activity

基本的には当初の研究計画通りに進める予定である。ATPシステムの設計においてまず考慮しなければならないのはタブロー法かsaturation法かの選択である。2020年度は高階論理と証明テンプレートとの親和性からタブロー法を選択したが、実線形算術における条件付き等式との相性の悪さが深刻であり、saturation系の手法も試すべきかもしれない。
理論面においては、証明テンプレート・循環証明系の研究を続ける予定である。それと同時に、今後のATP業界で注目されるであろうタクティクスベースの証明探索について、その基礎となる証明論を新たに構築できないか検討する。

Causes of Carryover

コロナ禍ですべての出張予定がキャンセルされたため、大幅に研究費を次年度に繰り越すことになった。これを機に50万円程度の計算用コンピュータを購入する予定である。これまでは研究機関のコンピュータを用いていたが、共用機器のため不便な点も多かった。研究室内に独自の計算環境を構築することで、ATPシステムの実装・実験に大いに役立つものと思われる。