細分化と要約を通じた数学証明の詳細度制御

自然言語証明では、細かい推論過程や計算過程は省略されることが多い。しかし、何を「細かい」と見做すかは書き手が持つ知識や書き手が想定する読み手のレベルなどの様々な要因に依存して決まるため、同じ命題であっても証明ごとに詳細度は異なりうる。そのため、読み手と書き手との間で「細かい」と認識している操作に差があると、その違いは、説明が不足している場合には論理的な飛躍、すなわち「行間」として現れ、逆に説明が過剰な場合には冗長な操作として現れる。これらはいずれも読み手の理解を阻害する原因となる。近年、大規模言語モデル(LLM)の研究及び発展に伴い、LLMが自然言語で数学の推論過程を生成する能力を十分に持つことが示されている[1,2]。この能力を応用し、自然言語証明の詳細度を自由に調整することができれば、数学的推論データセットの生成や、教育分野への応用、自然言語証明を機械検証可能な形式証明へと変換する自動形式化分野への応用など、多方面での応用が期待できる。しかし、LLMはハルシネーションを引き起こすリスクを抱えており、特に数学証明のような複雑な推論を要する場面では、誤った推論や意味のない推論を生成する傾向が強い[3]。さらに、推論の詳細度制御には証明全体の構造や文脈を踏まえた判断が必要であるため、推論を適切に補完・削減しつつ論理的に正しく再構成するというタスクは、現在のLLMにとっても極めて複雑かつ困難であろう。これを解決するため、本研究では、「行間」を3種類に分類し、それらに対し段階的に推論を補っていくことによる、ハルシネーションのリスクを抑制した自然言語証明の推論詳細化手法をまず提案する。さらに、推論の詳しさの調整をマニュアルに基づいて立案を行うモデルと、実行を行うモデルの二つに分けて構成し、これら2モデルを用いて細分化された証明における行間を調整する手法を提案する。また、実解析の命題およびその自然言語証明から構成されるデータセットに対して本手法を適用し、その有効性を実験的に検証する。