自動形式化とは、自然言語で書かれた数学証明を機械検証可能な形式証明に自動翻訳する技術のことである。この技術は近年の大規模言語モデルの発展に伴って盛んに研究されているが、学習に用いる自然言語証明-形式証明ペアデータの不足が課題となっている。本研究ではLLMの逆形式化能力を活用した形式証明の自然言語翻訳手法を提案する。また、自然言語証明の表現に沿って作成した形式証明データに対して本手法を適用し、生成された自然言語証明の品質を分析及び評価する。

形式証明とは、コンピューター上で検証可能な形式言語によって表された数学証明のことを指す。形式証明は主にIsabelle[1]やCoq[2]、Lean[3]に代表される定理証明支援系の言語で記述される。自動形式化とは、人間が書く証明(自然言語証明)を形式証明の形に自動変換するタスクである。自動形式化技術は高コストな人手による形式化作業の負荷を軽減するだけでなく、正確な動作が要求されるシステムの自動検証([4]など)や自動定理証明の実現にも応用できる。近年の大規模言語モデル(LargeLanguageModel;LLM)の発展により、機械翻訳タスクとしての自動形式化技術の研究は活発に進められている。しかし、モデルの学習データに用いる自然言語証明と形式数学のペアデータが不足していることや、自動形式化の結果を評価するための有効な指標がないことが課題になり十分な成果を上げることが出来ていないという実情がある。本研究では、形式証明のステップベースの逆形式化、即ち形式証明から自然言語証明への方向の証明ステップごとの翻訳と、証明ステップ間の構造解析を踏まえた要約の2段階からなる、形式証明と自然言語証明のペアデータの作成手法を提案する。また、大学学部レベルの数学証明から証明構造に沿って形式化し作成された形式証明データに対して提案手法を適用し、生成結果の分析及び評価を行う。