大規模言語モデル（LLM）は、数学的推論において顕著な進展を遂げており、これはAIの重要な検証環境となり得るだけでなく、さらなる発展によって科学的研究に影響を及ぼす可能性がある。強化学習を用いて正解の最終結果に報酬を与えることで、LLMは1年間でAIMEやHMMTといった定量的推論コンペティションで劣った成績から飽和状態にまで向上した。しかし、このアプローチには根本的な限界がある。より高い最終正解率を目指すだけでは、重要な問題である「正解が導かれたからといって、その推論が正しいとは限らない」という点には対処できない。さらに、定理証明のような多くの数学的タスクは、数値的な答えではなく、厳密な段階的導出を必要とするため、最終的な答えに対する報酬は適用できない。深層的推論の限界を押し広げるためには、数学的推論の包括性と厳密性を検証することが不可欠であると考える。特に、解が未知のオープンな問題に対しては、テスト時計算量のスケーリングにおいて自己検証（self-verification）が重要となる。自己検証可能な数学的推論の実現に向けて、本研究では、定理証明に適した正確かつ忠実なLLMベースの検証モデルの訓練方法を検討する。その後、この検証モデルを報酬モデルとして用いて証明生成器を訓練し、生成器が自身の証明において可能な限り多くの問題を事前に発見・修正するようインセンティブを与える。生成器の能力が向上するにつれて、生成と検証のギャップを維持するため、新しく検証が困難な証明に対して自動的にラベル付けを行うために検証用計算資源をスケーリングし、検証モデルのさらなる改善に資する訓練データを生成する手法を提案する。本研究で得られたモデル「DeepSeekMath-V2」は、強力な定理証明能力を示し、IMO 2025およびCMO 2024ではゴールドレベルの成績を達成し、Putnam 2024ではスケーリングされたテスト時計算量を用いて120点中118点（ほぼ完璧）の成績を収めた。なお、未解決の課題は依然として多数存在するが、これらの結果は、自己検証可能な数学的推論が現実可能な研究方向性であり、より高度な数学的AIシステムの開発に貢献する可能性を示唆している。