論文の概要: Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization

• arxiv url: http://arxiv.org/abs/2501.13959v3
• Date: Wed, 16 Jul 2025 04:56:27 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-17 14:40:09.218543
• Title: Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization
• Title（参考訳）: 効率的な数学的形式化のための効果的な事前検索モデル学習
• Authors: Yicheng Tao, Haotian Liu, Shanwen Wang, Hongteng Xu,
• Abstract要約: 本研究では,Mathlibから抽出したデータを利用して,軽量で効果的な前提条件検索モデルを訓練する手法を提案する。 このモデルは、微粒な類似性計算法と再ランクモジュールを応用した、対照的な学習フレームワークで学習される。 実験により,本モデルが既存のベースラインより優れており,計算負荷の低減を図りながら高い精度を実現していることが示された。
• 参考スコア（独自算出の注目度）: 29.06255449960557
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formalized mathematics has recently garnered significant attention for its ability to assist mathematicians across various fields. Premise retrieval, as a common step in mathematical formalization, has been a challenge, particularly for inexperienced users. Existing retrieval methods that facilitate natural language queries require a certain level of mathematical expertise from users, while approaches based on formal languages (e.g., Lean) typically struggle with the scarcity of training data, hindering the training of effective and generalizable retrieval models. In this work, we introduce a novel method that leverages data extracted from Mathlib to train a lightweight and effective premise retrieval model. In particular, the proposed model embeds queries (i.e., proof state provided by Lean) and premises in a latent space, featuring a tokenizer specifically trained on formal corpora. The model is learned in a contrastive learning framework, in which a fine-grained similarity calculation method and a re-ranking module are applied to enhance the retrieval performance. Experimental results demonstrate that our model outperforms existing baselines, achieving higher accuracy while maintaining a lower computational load. We have released an open-source search engine based on our retrieval model at https://premise-search.com/. The source code and the trained model can be found at https://github.com/ruc-ai4math/Premise-Retrieval.
• Abstract（参考訳）: 形式化された数学は、様々な分野の数学者を支援する能力において、近年大きな注目を集めている。 数学的な形式化の一般的なステップであるPremise検索は、特に経験の浅いユーザーにとって課題となっている。 自然言語クエリを容易にする既存の検索手法では、ユーザから特定のレベルの数学的専門知識を必要とするが、形式言語(例えば、リーン)に基づくアプローチは、トレーニングデータの不足に悩まされ、効果的で一般化可能な検索モデルのトレーニングを妨げている。 本研究では,Mathlibから抽出したデータを利用して,軽量で効果的な前提条件検索モデルを訓練する手法を提案する。 特に、提案されたモデルは、クエリ(すなわち、リーンによって提供される証明状態)と前提を潜伏した空間に埋め込む。 比較学習フレームワークで学習し、詳細な類似性計算法と再ランクモジュールを適用して検索性能を向上させる。 実験により,本モデルが既存のベースラインより優れており,計算負荷の低減を図りながら高い精度を実現していることが示された。 われわれはhttps://premises-search.com/で検索モデルに基づいたオープンソースの検索エンジンをリリースした。 ソースコードとトレーニングされたモデルはhttps://github.com/ruc-ai4math/Premise-Retrieval.comにある。

関連論文リスト

• SPaRFT: Self-Paced Reinforcement Fine-Tuning for Large Language Models [51.74498855100541]
  大規模言語モデル(LLM)は、強化学習(RL)による微調整時に強い推論能力を示す。 トレーニング対象のモデルの性能に基づいて,効率的な学習を可能にする自己評価学習フレームワークである textbfSPaRFT を提案する。
  論文  参考訳（メタデータ） (2025-08-07T03:50:48Z)
• On the Usage of Gaussian Process for Efficient Data Valuation [3.688196752709501]
  機械学習では、与えられたダタムがモデルトレーニングに与える影響を知ることは、データバリュエーションと呼ばれる基本的なタスクである。 我々は,データ評価手法を2つの部品の組み合わせとして分析できる新しい標準分解法を設計した。 提案手法の強みは, ベイズ理論の理論的根拠と, 効率的な更新式により評価値の高速な推定を可能にした実用的到達性の両方に起因している。
  論文  参考訳（メタデータ） (2025-06-04T14:53:51Z)
• Exploring Training and Inference Scaling Laws in Generative Retrieval [50.82554729023865]
  生成検索は、検索を自己回帰生成タスクとして再構成し、大きな言語モデルがクエリから直接ターゲット文書を生成する。 生成的検索におけるトレーニングと推論のスケーリング法則を体系的に検討し,モデルのサイズ,トレーニングデータスケール,推論時間計算が協調的に性能に与える影響について検討した。
  論文  参考訳（メタデータ） (2025-03-24T17:59:03Z)
• Is a Good Foundation Necessary for Efficient Reinforcement Learning? The Computational Role of the Base Model in Exploration [32.77845864484552]
  本稿では,言語モデルを用いたRLの新しい計算フレームワークを提案する。 データ効率には必要ありませんが、フレームワーク内の任意のアルゴリズムのランタイムのバウンダリは低くなっています。 SpannerSamplingというアルゴリズムを導入し,事前学習したモデルが十分なカバレッジを享受するたびに,最適なデータ効率と計算効率を実現する。
  論文  参考訳（メタデータ） (2025-03-10T15:31:42Z)
• LoRE-Merging: Exploring Low-Rank Estimation For Large Language Model Merging [10.33844295243509]
  基本モデルであるtextscLoRE-Merging へのアクセスを必要とせず,タスクベクトルの低ランク推定に基づくモデルマージのための統一フレームワークを提案する。 我々のアプローチは、細調整されたモデルからのタスクベクトルは、しばしば支配的な特異値の限られた数しか示さず、低ランク推定が干渉しにくくなるという観察に動機づけられている。
  論文  参考訳（メタデータ） (2025-02-15T10:18:46Z)
• BRiTE: Bootstrapping Reinforced Thinking Process to Enhance Language Model Reasoning [78.63421517563056]
  大規模言語モデル(LLM)は複雑な推論タスクにおいて顕著な機能を示した。 本稿では,新しいグラフィカルモデルを用いてLLM推論を定式化する統一確率的フレームワークを提案する。 本稿では,Bootstrapping Reinforced Thinking Process (BRiTE)アルゴリズムについて述べる。
  論文  参考訳（メタデータ） (2025-01-31T02:39:07Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• Retrieval-Oriented Knowledge for Click-Through Rate Prediction [29.55757862617378]
  クリックスルー率(CTR)予測は、パーソナライズされたオンラインサービスにとって不可欠である。 underlineretrieval-underlineoriented underlineknowledge(bfname)フレームワークは、実際の検索プロセスをバイパスする。 nameは、検索および集約された表現を保存および模倣する知識ベースを特徴とする。
  論文  参考訳（メタデータ） (2024-04-28T20:21:03Z)
• DIMAT: Decentralized Iterative Merging-And-Training for Deep Learning Models [21.85879890198875]
  Decentralized Iterative Merging-And-Training (DIMAT) は、新しい分散深層学習アルゴリズムである。 DIMATは, 独立・同一分散(IID)および非IIDデータを用いて, 通信オーバヘッドの低減を図ることにより, より高速かつ高い初期ゲインが得られることを示す。 このDIMATパラダイムは未来の分散学習に新たな機会を与え、疎結合な通信計算で現実世界への適応性を高める。
  論文  参考訳（メタデータ） (2024-04-11T18:34:29Z)
• Back to Basics: A Simple Recipe for Improving Out-of-Domain Retrieval in Dense Encoders [63.28408887247742]
  得られたモデルにおいて,より優れた一般化能力を得るために,トレーニング手順の改善が可能であるかを検討する。 我々は、高密度エンコーダをトレーニングするための簡単なレシピを推奨する: LoRAのようなパラメータ効率のよいMSMARCOのトレーニング。
  論文  参考訳（メタデータ） (2023-11-16T10:42:58Z)
• CodeGen2: Lessons for Training LLMs on Programming and Natural Languages [116.74407069443895]
  我々はエンコーダとデコーダベースのモデルを単一のプレフィックスLMに統一する。 学習方法は,「フリーランチ」仮説の主張を考察する。 データ配信においては,混合分布と多言語学習がモデル性能に及ぼす影響について検討した。
  論文  参考訳（メタデータ） (2023-05-03T17:55:25Z)
• Exploring validation metrics for offline model-based optimisation with diffusion models [50.404829846182764]
  モデルベース最適化(MBO)では、マシンラーニングを使用して、(基底真理)オラクルと呼ばれるブラックボックス関数に対する報酬の尺度を最大化する候補を設計することに興味があります。 モデル検証中に基底オラクルに対する近似をトレーニングし、その代わりに使用することができるが、その評価は近似的であり、敵の例に対して脆弱である。 本手法は,外挿量を測定するために提案した評価フレームワークにカプセル化されている。
  論文  参考訳（メタデータ） (2022-11-19T16:57:37Z)
• Generalization Properties of Retrieval-based Models [50.35325326050263]
  検索ベースの機械学習手法は、幅広い問題で成功をおさめた。 これらのモデルの約束を示す文献が増えているにもかかわらず、そのようなモデルの理論的基盤はいまだに解明されていない。 本稿では,その一般化能力を特徴付けるために,検索ベースモデルの形式的処理を行う。
  論文  参考訳（メタデータ） (2022-10-06T00:33:01Z)
• CorpusBrain: Pre-train a Generative Retrieval Model for Knowledge-Intensive Language Tasks [62.22920673080208]
  単一ステップ生成モデルは、検索プロセスを劇的に単純化し、エンドツーエンドで最適化することができる。 我々は、事前学習された生成検索モデルをCorpsBrainと名付け、コーパスに関する全ての情報が、追加のインデックスを構築することなく、そのパラメータにエンコードされる。
  論文  参考訳（メタデータ） (2022-08-16T10:22:49Z)
• Benchopt: Reproducible, efficient and collaborative optimization benchmarks [67.29240500171532]
  Benchoptは、機械学習で最適化ベンチマークを自動化、再生、公開するためのフレームワークである。 Benchoptは実験を実行、共有、拡張するための既製のツールを提供することで、コミュニティのベンチマークを簡単にする。
  論文  参考訳（メタデータ） (2022-06-27T16:19:24Z)
• HyperImpute: Generalized Iterative Imputation with Automatic Model Selection [77.86861638371926]
  カラムワイズモデルを適応的かつ自動的に構成するための一般化反復計算フレームワークを提案する。 既製の学習者,シミュレータ,インターフェースを備えた具体的な実装を提供する。
  論文  参考訳（メタデータ） (2022-06-15T19:10:35Z)
• Deep Efficient Continuous Manifold Learning for Time Series Modeling [11.876985348588477]
  対称正定値行列はコンピュータビジョン、信号処理、医療画像解析において研究されている。 本稿では,リーマン多様体とコレスキー空間の間の微分同相写像を利用する枠組みを提案する。 時系列データの動的モデリングのために,多様体常微分方程式とゲートリカレントニューラルネットワークを体系的に統合した連続多様体学習法を提案する。
  論文  参考訳（メタデータ） (2021-12-03T01:38:38Z)
• 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)
• Monotonic Cardinality Estimation of Similarity Selection: A Deep Learning Approach [22.958342743597044]
  類似度選択の基数推定にディープラーニングを活用する可能性について検討する。 本稿では,任意のデータ型や距離関数に適用可能な,新規で汎用的な手法を提案する。
  論文  参考訳（メタデータ） (2020-02-15T20:22:51Z)

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

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