論文の概要: A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation

• arxiv url: http://arxiv.org/abs/2502.17840v1
• Date: Tue, 25 Feb 2025 04:41:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-26 18:40:41.959876
• Title: A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
• Title（参考訳）: A Combinatorial Identities ベンチマークによる自動定理生成による定理証明
• Authors: Beibei Xiong, Hangyu Lv, Haojia Shan, Jianlin Wang, Zhengfeng Yang, Lihong Zhi,
• Abstract要約: コンビニティクスは数学の基盤であり、離散構造の分析と問題解決に不可欠なツールを提供する。 これを解決するために、手動でLeanCombを構築しました。 我々は,自己改善型大規模言語モデルによって提案される候補戦略と,予測のための強化学習木探索アプローチを組み合わせた,コンビニアル・アイデンティティのための自動定理ジェネレータATG4CIを開発した。
• 参考スコア（独自算出の注目度）: 3.003569769097376
• License:
• Abstract: Large language models (LLMs) have significantly advanced formal theorem proving, yet the scarcity of high-quality training data constrains their capabilities in complex mathematical domains. Combinatorics, a cornerstone of mathematics, provides essential tools for analyzing discrete structures and solving optimization problems. However, its inherent complexity makes it particularly challenging for automated theorem proving (ATP) for combinatorial identities. To address this, we manually construct LeanComb, combinatorial identities benchmark in Lean, which is, to our knowledge, the first formalized theorem proving benchmark built for combinatorial identities. We develop an Automated Theorem Generator for Combinatorial Identities, ATG4CI, which combines candidate tactics suggested by a self-improving large language model with a Reinforcement Learning Tree Search approach for tactic prediction. By utilizing ATG4CI, we generate a LeanComb-Enhanced dataset comprising 260K combinatorial identities theorems, each with a complete formal proof in Lean, and experimental evaluations demonstrate that models trained on this dataset can generate more effective tactics, thereby improving success rates in automated theorem proving for combinatorial identities.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、非常に高度な形式的定理を証明しているが、高品質な訓練データの不足は、複雑な数学的領域におけるそれらの能力を制限している。 数学の基礎であるコンビニティクスは、離散構造の解析と最適化問題の解決に不可欠なツールを提供する。 しかし、その固有の複雑さは、組合せ的同一性に対する自動定理証明(ATP)を特に困難にしている。 これに対処するため、私たちはLeanCombという組合せアイデンティティのベンチマークをLeanで手作業で構築しました。 我々は,自己改善型大規模言語モデルによって提案される候補戦略と,戦術予測のための強化学習木探索手法を組み合わせた,コンビニアル・アイデンティティのための自動定理生成器ATG4CIを開発した。 ATG4CIを利用することで、260Kの組合せ等式定理からなるLeanComb強化データセットを生成し、それぞれがLeanで完全な形式証明を持ち、実験的な評価により、このデータセットでトレーニングされたモデルがより効果的な戦術を生成できることを示し、組合せ等式を証明した自動定理の成功率を向上させる。

関連論文リスト

• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• Learning to Prove Trigonometric Identities [36.56548303496931]
  我々は三角法等式の自動証明システムを構築した。 私たちのゴールは、証明を完成させるだけでなく、できるだけ少数のステップで証明を完成させることです。 強化学習によってさらなる改善が加えられたAutoTrigは、BFSと同じくらいの短いステップで、アイデンティティの証明ステップを提供することができる。
  論文  参考訳（メタデータ） (2022-07-14T06:16:17Z)
• Training a First-Order Theorem Prover from Synthetic Data [50.23600875138756]
  自動定理証明に機械学習を適用する際の大きな課題は、トレーニングデータの不足である。 本稿では,人間のデータを公理によらずに,純粋に合成生成定理をトレーニングする手法を提案する。 私達の神経証明者は時間および検索のステップのこの総合的なデータで最先端のE-proverを上回っます。
  論文  参考訳（メタデータ） (2021-03-05T17:01:34Z)
• Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
  PACT(bf Proof bf Artifact bf Co-bf Training)は、カーネルレベルのコトレーニング用証明項から自己教師付きデータを抽出する一般的な手法である。 我々は、Transformer言語モデルによって駆動されるニューラル定理証明器でリーンを計測し、PACTがテスト定理の保留組における成功率を証明する定理を32%から48%に改善することを示す。
  論文  参考訳（メタデータ） (2021-02-11T18:59:24Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)
• INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving [36.194330645092634]
  本稿では,エージェントの一般化能力をテストするために,INequality Theorem Proving benchmarkを提案する。 Int は定理と証明を生成する手順に基づいており、この手順のノブは6つの異なる種類の一般化を測ることができる。 次に,モンテカルロ木探索(MCTS)で拡張したエージェントを試験時に評価し,MCTSが新たな定理を証明できることを示す。
  論文  参考訳（メタデータ） (2020-07-06T17:55:33Z)
• Learning to Prove from Synthetic Theorems [41.74768503409581]
  自動定理証明に機械学習を適用する上での大きな課題は、トレーニングデータの不足である。 本稿では,一組の公理から生成される合成定理による学習に依存するアプローチを提案する。 このような定理が自動証明器の訓練に利用でき、学習された証明器が人間の生成した定理にうまく移行できることが示される。
  論文  参考訳（メタデータ） (2020-06-19T17:48:09Z)

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

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