Fugu-MT 論文翻訳(概要): Hierarchical Attention Generates Better Proofs

論文の概要: Hierarchical Attention Generates Better Proofs

arxiv url: http://arxiv.org/abs/2504.19188v1
Date: Sun, 27 Apr 2025 10:35:05 GMT
ステータス: 翻訳完了
システム内更新日: 2025-05-02 19:15:54.171396
Title: Hierarchical Attention Generates Better Proofs
Title（参考訳）: 階層的注意がより良い証明を生成する
Authors: Jianlong Chen, Chao Li, Yang Yuan, Andrew C Yao,
Abstract要約: 注意機構を数学的推論構造に整合させる正規化手法であるtextbfHierarchical Attention を導入する。提案手法は,基礎要素から高レベル概念への5段階階層を確立し,証明生成における構造化情報の流れを確実にする。
参考スコア（独自算出の注目度）: 8.676187819105298
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Large language models (LLMs) have shown promise in formal theorem proving, but their token-level processing often fails to capture the inherent hierarchical nature of mathematical proofs. We introduce \textbf{Hierarchical Attention}, a regularization method that aligns LLMs' attention mechanisms with mathematical reasoning structures. Our approach establishes a five-level hierarchy from foundational elements to high-level concepts, ensuring structured information flow in proof generation. Experiments demonstrate that our method improves proof success rates by 2.05\% on miniF2F and 1.69\% on ProofNet while reducing proof complexity by 23.81\% and 16.50\% respectively. The code is available at https://github.com/Car-pe/HAGBP.
Abstract（参考訳）: 大型言語モデル (LLMs) は形式的定理の証明において有望であるが、それらのトークンレベルの処理は数学的な証明の本質的に階層的な性質を捉えるのに失敗することが多い。 LLMの注意機構を数学的推論構造に整合させる正規化手法である「textbf{Hierarchical Attention}」を導入する。提案手法は,基礎要素から高レベル概念への5段階階層を確立し,証明生成における構造化情報の流れを確実にする。実験の結果,ProofNetは25%,ProofNetは1.69%,ProofNetは23.81%,ProofNetは16.50%であった。コードはhttps://github.com/Car-pe/HAGBPで公開されている。

関連論文リスト

LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文参考訳（メタデータ） (2025-02-25T07:46:36Z)
Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs [6.65877320351217]
我々はLeanNavigatorを開発した。これはリーンの定理と証明の大規模なデータセットを生成する新しい方法だ。我々は10億のトークンを合計470万の定理で生成し、以前のデータセットを桁違いに上回った。この広範なデータセットを使用して、我々は、定理証明タスクにおいて最先端のReProverモデルより優れたAIモデルを訓練した。
論文参考訳（メタデータ） (2025-02-16T06:20:39Z)
Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文参考訳（メタデータ） (2025-02-11T15:27:35Z)
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)
Proof Automation with Large Language Models [6.587933406842906]
大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
論文参考訳（メタデータ） (2024-09-22T00:19:27Z)
Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。また,POETRYが検出した最大証明長は10～26。
論文参考訳（メタデータ） (2024-05-23T10:35:08Z)
Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method [1.8130068086063336]
本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。 ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
論文参考訳（メタデータ） (2023-12-20T09:55:21Z)
Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文参考訳（メタデータ） (2022-05-25T02:22:30Z)
PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文参考訳（メタデータ） (2020-10-06T15:47:53Z)

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