Fugu-MT 論文翻訳(概要): Combining Textual and Structural Information for Premise Selection in Lean

論文の概要: Combining Textual and Structural Information for Premise Selection in Lean

arxiv url: http://arxiv.org/abs/2510.23637v1
Date: Fri, 24 Oct 2025 14:24:13 GMT
ステータス: 翻訳完了
システム内更新日: 2025-10-29 15:35:36.304865
Title: Combining Textual and Structural Information for Premise Selection in Lean
Title（参考訳）: リーンにおける前提選択のためのテキスト情報と構造情報の組み合わせ
Authors: Job Petrovčič, David Eliecer Narvaez Denis, Ljupčo Todorovski,
Abstract要約: 本稿では、リーン形式化の高密度テキスト埋め込みと、不均一依存グラフ上のグラフニューラルネットワークを組み合わせたグラフ拡張手法を提案する。 LeanDojo Benchmarkでは、標準の検索指標でReProver言語ベースのベースラインを25%以上上回ります。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Premise selection is a key bottleneck for scaling theorem proving in large formal libraries. Yet existing language-based methods often treat premises in isolation, ignoring the web of dependencies that connects them. We present a graph-augmented approach that combines dense text embeddings of Lean formalizations with graph neural networks over a heterogeneous dependency graph capturing both state--premise and premise--premise relations. On the LeanDojo Benchmark, our method outperforms the ReProver language-based baseline by over 25% across standard retrieval metrics. These results demonstrate the power of relational information for more effective premise selection.
Abstract（参考訳）: プリミズ選択は、大きな形式ライブラリーで証明される定理のスケーリングの鍵となるボトルネックである。しかし、既存の言語ベースのメソッドは、しばしば前提を分離して扱い、それらを接続する依存関係のウェブを無視します。本稿では、リーン形式化の高密度テキスト埋め込みとグラフニューラルネットワークを組み合わせたグラフ拡張手法を提案する。 LeanDojo Benchmarkでは、標準の検索指標でReProver言語ベースのベースラインを25%以上上回ります。これらの結果は、より効果的な前提選択のための関係情報のパワーを示す。

関連論文リスト

Knowledge Graph Completion with Relation-Aware Anchor Enhancement [50.50944396454757]
関係認識型アンカー強化知識グラフ補完法(RAA-KGC)を提案する。まず、ヘッダーのリレーショナル・アウェア・エリア内でアンカー・エンティティを生成します。次に、アンカーの近傍に埋め込まれたクエリを引っ張ることで、ターゲットのエンティティマッチングに対してより差別的になるように調整する。
論文参考訳（メタデータ） (2025-04-08T15:22:08Z)
Optimized Feature Generation for Tabular Data via LLMs with Decision Tree Reasoning [53.241569810013836]
本稿では,大規模言語モデル(LLM)を用いて,効率的な特徴生成ルールを同定するフレームワークを提案する。我々は、自然言語で容易に表現できるため、この推論情報を伝達するために決定木を使用します。 OCTreeは様々なベンチマークで様々な予測モデルの性能を継続的に向上させる。
論文参考訳（メタデータ） (2024-06-12T08:31:34Z)
Unsupervised Extractive Summarization with Heterogeneous Graph Embeddings for Chinese Document [5.9630342951482085]
中国語文書にヘテロジニアスグラフ埋め込み (HGE) を組み込んだ教師なし抽出サマリザイトン法を提案する。実験結果から,本手法は3つの要約データセットにおいて,強いベースラインを一貫して上回ることを示した。
論文参考訳（メタデータ） (2022-11-09T06:07:31Z)
Towards Realistic Low-resource Relation Extraction: A Benchmark with Empirical Baseline Study [51.33182775762785]
本稿では,低リソース環境下での関係抽出システムを構築するための実証的研究について述べる。低リソース環境での性能を評価するための3つのスキームについて検討する。 (i) ラベル付きラベル付きデータを用いた異なるタイプのプロンプトベース手法、 (ii) 長期分布問題に対処する多様なバランシング手法、 (iii) ラベル付きインドメインデータを生成するためのデータ拡張技術と自己学習。
論文参考訳（メタデータ） (2022-10-19T15:46:37Z)
Incorporating Linguistic Knowledge for Abstractive Multi-document Summarization [20.572283625521784]
ニューラルネットワークに基づく抽象的多文書要約(MDS)モデルを開発した。依存関係情報を言語誘導型注意機構に処理する。言語信号の助けを借りて、文レベルの関係を正しく捉えることができる。
論文参考訳（メタデータ） (2021-09-23T08:13:35Z)
Dependency Induction Through the Lens of Visual Perception [81.91502968815746]
本稿では,単語の具体性を利用した教師なし文法帰納モデルと,構成的視覚に基づく構成的文法を共同学習する手法を提案する。実験により,提案した拡張は,文法的サイズが小さい場合でも,現在最先端の視覚的接地モデルよりも優れた性能を示すことが示された。
論文参考訳（メタデータ） (2021-09-20T18:40:37Z)
Nutribullets Hybrid: Multi-document Health Summarization [36.95954983680022]
本稿では,入力文書の類似性と矛盾を強調する比較要約を生成する手法を提案する。私たちのフレームワークは、より忠実で関連性があり、集約に敏感な要約につながります。
論文参考訳（メタデータ） (2021-04-08T01:44:29Z)
Coordinate Constructions in English Enhanced Universal Dependencies: Analysis and Computational Modeling [1.9950682531209154]
拡張ユニバーサル依存(UD)における座標構成の表現に対処する。手動で編集した構文グラフの大規模なデータセットを作成する。元のデータにおけるいくつかの系統的誤りを識別し、結合の伝播も提案する。
論文参考訳（メタデータ） (2021-03-16T10:24:27Z)
Keyphrase Extraction with Dynamic Graph Convolutional Networks and Diversified Inference [50.768682650658384]
キーワード抽出(KE)は、ある文書でカバーされている概念やトピックを正確に表現するフレーズの集合を要約することを目的としている。最近のシークエンス・ツー・シークエンス(Seq2Seq)ベースの生成フレームワークはKEタスクで広く使われ、様々なベンチマークで競合性能を得た。本稿では,この2つの問題を同時に解くために,動的グラフ畳み込みネットワーク(DGCN)を採用することを提案する。
論文参考訳（メタデータ） (2020-10-24T08:11:23Z)
Heavy-tailed Representations, Text Polarity Classification & Data Augmentation [11.624944730002298]
所望の正則性を持つ重み付き埋め込みを学習するための新しい手法を開発した。提案した埋め込みの尾部専用の分類器が得られ、性能がベースラインを上回っている。合成および実テキストデータに関する数値実験により,提案手法の妥当性が示された。
論文参考訳（メタデータ） (2020-03-25T19:24:05Z)

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