論文の概要: Learning to Disprove: Formal Counterexample Generation with Large Language Models
- arxiv url: http://arxiv.org/abs/2603.19514v1
- Date: Thu, 19 Mar 2026 22:42:49 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-23 19:48:38.911656
- Title: Learning to Disprove: Formal Counterexample Generation with Large Language Models
- Title（参考訳）: 解き放つ学習:大規模言語モデルを用いた形式的反例生成
- Abstract要約: 数学における現在のAIの取り組みは、ほとんど証明構築にのみ焦点をあてている。
我々はこのタスクを形式的な逆例生成として定式化する。
多様なトレーニングデータを合成するシンボリックな突然変異戦略を導入する。
- 参考スコア（独自算出の注目度）: 26.262810717227108
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Mathematical reasoning demands two critical, complementary skills: constructing rigorous proofs for true statements and discovering counterexamples that disprove false ones. However, current AI efforts in mathematics focus almost exclusively on proof construction, often neglecting the equally important task of finding counterexamples. In this paper, we address this gap by fine-tuning large language models (LLMs) to reason about and generate counterexamples. We formalize this task as formal counterexample generation, which requires LLMs not only to propose candidate counterexamples but also to produce formal proofs that can be automatically verified in the Lean 4 theorem prover. To enable effective learning, we introduce a symbolic mutation strategy that synthesizes diverse training data by systematically extracting theorems and discarding selected hypotheses, thereby producing diverse counterexample instances. Together with curated datasets, this strategy enables a multi-reward expert iteration framework that substantially enhances both the effectiveness and efficiency of training LLMs for counterexample generation and theorem proving. Experiments on three newly collected benchmarks validate the advantages of our approach, showing that the mutation strategy and training framework yield significant performance gains.
- Abstract（参考訳）: 数学的推論は、真言の厳密な証明を構築し、偽の証明を否定する反例を発見するという、2つの重要な補完的なスキルを要求する。
しかし、現在の数学におけるAIの取り組みは、ほとんど証明構築に焦点を合わせており、しばしば反例を見つけるという同様に重要なタスクを無視している。
本稿では,大言語モデル(LLM)を微調整し,逆例を生成することで,このギャップに対処する。
我々は、このタスクを形式的な反例生成として形式化し、LSMは候補となる反例を提案するだけでなく、Lean 4定理証明器で自動的に検証できる形式的な証明を生成する必要がある。
効果的な学習を可能にするために,定理を体系的に抽出し,選択された仮説を捨て,多様な逆例を生成することによって,多様なトレーニングデータを合成するシンボリック突然変異戦略を導入する。
この戦略は、キュレートされたデータセットとともに、逆例生成と定理証明のためのLLMのトレーニングの有効性と効率を大幅に向上するマルチリワード専門家の反復フレームワークを実現する。
新たに収集された3つのベンチマーク実験により,本手法の利点が検証され,変異戦略とトレーニングフレームワークが大きなパフォーマンス向上をもたらすことが示された。
関連論文リスト
- INSPIRE: An Internalize-Then-Improve Approach for Example-Driven Mathematical Reasoning [61.60016491769943]
人間の数学教育において、定理境界をテストするために反例を構築するような例に基づく推論は、深い概念的理解を反映している。
本稿では,RGSI(Reference-Guided Students Internalization)と段階的選好学習戦略を組み合わせた内在化・内在化アプローチであるINSPIREを提案する。
複数のモデルスケールとファミリーにわたる実験は、大規模なオープンソースモデルを超えながら、一貫した改善を示している。
論文 参考訳（メタデータ） (2026-08-27T03:24:03Z) - Counterexample Guided Learning in the Large using Reasoning Agents [15.424030391880677]
検証器のフィードバックは,課題抽出作業におけるサンプル効率を大幅に向上させ,必要なラベル付き例の数を削減し,標準のプロンプトが失敗する複雑なターゲット表現の学習を可能にすることを示す。
これらの結果から,LSMを付加的なデータとして扱うこと以外に,LLMに基づくプログラム合成と形式推論のための堅牢な検証者誘導手法の扉を開くことのメリットが示唆された。
論文 参考訳（メタデータ） (2026-06-09T23:46:46Z) - Learning to Reason with Insight for Informal Theorem Proving [50.054221663394195]
この研究では、非公式な定理における主要なボトルネックを洞察の欠如として証明する。
我々は,この本質的な推論スキルを育成し,LLMが洞察に富んだ推論を行うことを可能にする新しいフレームワークを提案する。
問題となる数学ベンチマークの実験では、この洞察・認識型生成戦略がベースラインを著しく上回ることを示した。
論文 参考訳（メタデータ） (2026-04-17T17:36:21Z) - Learning from Equivalence Queries, Revisited [62.46207559138802]
本研究は,全情報と帯域幅の両方のフィードバックに基づいて等価クエリから学習する。
本分析では,対称逆数に対するゲーム理論的視点と適応重み付け法とミニマックス引数を組み合わせる。
論文 参考訳（メタデータ） (2026-04-06T08:55:41Z) - ExVerus: Verus Proof Repair via Counterexample Reasoning [8.819482630789217]
大規模言語モデル(LLM)のための逆例誘導フレームワークであるEXVERUSを提案する。
証明が失敗すると、EXVERUSは反例を自動生成して検証し、LSMを誘導して誘導不変量に一般化し、これらの障害を阻止する。
評価の結果,EXVERUSは最先端のプロンプトベースのVerus証明生成器よりも証明精度,堅牢性,トークン効率を著しく向上することがわかった。
論文 参考訳（メタデータ） (2026-03-26T18:14:34Z) - LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving [6.220998637943786]
LeanConjecturerは、Large Language Models(LLMs)を使用して、Lean 4で大学レベルの数学予想を自動的に生成するパイプラインである。
反復生成と評価により、LeanConjecturerは40のMathlibシードファイルから12,289の予想を生成し、3,776は構文的に有効で非自明であると同定された。
論文 参考訳（メタデータ） (2025-06-27T08:17:18Z) - 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) - Steering LLMs for Formal Theorem Proving [1.083373217040891]
我々は,非公式な推論トレースに関連する残効活性化における線形方向を同定する推論時間介入を開発する。
このメカニズムはまた、大規模言語モデルのアクティベーション空間において、推論がどのように内部的にエンコードされているかについての解釈可能な情報を与える。
1) LLM の証明合成を導くための新しいアクティベーションベースの介入,(2) この介入が2つの復号化戦略の下で性能を向上させることの実証である。
論文 参考訳（メタデータ） (2025-02-21T15:04:48Z) - One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [75.95179490687018]
証明生成のための数学的大規模言語モデルを活用することは、LLM研究の基本的なトピックである。
現状のLCMが証明できる能力は、学習中に関連する証明プロセスに遭遇したかどうかに大きく依存していると論じる。
人間の数学教育で一般的に用いられる「反例による防御」の教育的手法に触発されて,我々の研究は,反例を通して数学的推論と証明を行うLLMの能力を高めることを目的としている。
論文 参考訳（メタデータ） (2025-02-12T02:01:10Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - A Critical Analysis of the Theoretical Framework of the Extreme Learning Machine [1.9503475832401784]
ELM学習アルゴリズムに反例を与える2つの主要な文とデータセットの証明を論じる。
我々は、いくつかの理論的ケースにおいて、EMMの効率を正当化する基礎の代替的なステートメントを提供する。
論文 参考訳（メタデータ） (2024-06-25T10:06:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。