Abstract
ほとんどの自動定理証明アプローチは形式的な証明システムに依存していますが、非形式的な定理証明は、自然言語処理における大規模言語モデル（LLM）の強みとよりよく整合し得ます。本研究では、非形式的な定理証明における主要なボトルネックが「洞察の欠如」であること、つまり複雑な問題を解くために必要な中核となる手法を認識することが難しい点にあることを特定します。これに対処するために、必要不可欠な推論スキルを育成し、LLMが洞察に基づく推論を行えるようにする新しい枠組みを提案します。私たちは、最終的な証明とともに、コアとなる手法と証明スケッチを明示的に抽出して非形式的な証明を構造化する階層型データセットmathtt{DeepInsightTheorem}を提案します。このデータセットを最大限に活用するために、人間の学習プロセスを模倣するプログレッシブなマルチステージSFT戦略を設計し、モデルを基礎的な証明文の作成から洞察に基づく思考へ導きます。難しい数学的ベンチマークに対する実験の結果、洞察を意識した生成戦略がベースラインを大きく上回ることが示されました。これらの結果は、モデルにコアとなる手法を識別し適用するよう教えることで、数学的推論を大幅に改善できることを示しています。
