論文の概要: Learning to Reason with Insight for Informal Theorem Proving

• arxiv url: http://arxiv.org/abs/2604.16278v1
• Date: Fri, 17 Apr 2026 17:36:21 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-20 22:00:20.033246
• Title: Learning to Reason with Insight for Informal Theorem Proving
• Title（参考訳）: Informal Theorem Provingのためのインテリジェンスによる推論学習
• Authors: Yunhe Li, Hao Shi, Bowen Deng, Wei Wang, Mengzhe Ruan, Hanxu Hou, Zhongxiang Dai, Siyang Gao, Chao Wang, Shuang Qiu, Linqi Song,
• Abstract要約: この研究では、非公式な定理における主要なボトルネックを洞察の欠如として証明する。 我々は,この本質的な推論スキルを育成し,LLMが洞察に富んだ推論を行うことを可能にする新しいフレームワークを提案する。 問題となる数学ベンチマークの実験では、この洞察・認識型生成戦略がベースラインを著しく上回ることを示した。
• 参考スコア（独自算出の注目度）: 50.054221663394195
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Although most of the automated theorem-proving approaches depend on formal proof systems, informal theorem proving can align better with large language models' (LLMs) strength in natural language processing. In this work, we identify a primary bottleneck in informal theorem proving as a lack of insight, namely the difficulty of recognizing the core techniques required to solve complex problems. To address this, we propose a novel framework designed to cultivate this essential reasoning skill and enable LLMs to perform insightful reasoning. We propose $\mathtt{DeepInsightTheorem}$, a hierarchical dataset that structures informal proofs by explicitly extracting core techniques and proof sketches alongside the final proof. To fully exploit this dataset, we design a Progressive Multi-Stage SFT strategy that mimics the human learning process, guiding the model from basic proof writing to insightful thinking. Our experiments on challenging mathematical benchmarks demonstrate that this insight-aware generation strategy significantly outperforms baselines. These results demonstrate that teaching models to identify and apply core techniques can substantially improve their mathematical reasoning.
• Abstract（参考訳）: 自動定理証明アプローチのほとんどは形式的証明システムに依存しているが、非公式定理証明は自然言語処理における大きな言語モデル(LLM)の強みとよく一致する。 この研究は、非公式な定理における主要なボトルネックを洞察の欠如、すなわち複雑な問題を解決するのに必要な中核技術を認識することの難しさとして証明するものである。 そこで本研究では,この本質的な推論スキルを育成し,LLMが洞察に富んだ推論を行えるようにするための新しいフレームワークを提案する。 我々は,コア技術と証明スケッチを最終証明とともに明示的に抽出することにより,非公式な証明を構造化する階層的データセットである$\mathtt{DeepInsightTheorem}$を提案する。 このデータセットをフル活用するために,人間の学習プロセスを模倣したプログレッシブ・マルチステージSFT戦略を設計し,基本的証明書から洞察力のある思考へとモデルを導く。 問題となる数学ベンチマークの実験では、この洞察・認識型生成戦略がベースラインを著しく上回ることを示した。 これらの結果から,中核的手法を同定・適用するための学習モデルが数学的推論を大幅に改善できることが示唆された。

関連論文リスト

• Learning Temporal Abstractions via Variational Homomorphisms in Option-Induced Abstract MDPs [17.335266921332092]
  大規模言語モデル(LLMs)は、明示的なChain-of-Thoughtプロンプトを通じて、顕著な推論能力を示している。 モデルがすべてのステップに対して明示的なテキストを生成することなく、潜在空間で"考え"する、効率的で暗黙的な推論のためのフレームワークを開発する。
  論文  参考訳（メタデータ） (2025-07-22T11:22:58Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。