論文の概要: Assisting Mathematical Formalization with A Learning-based Premise Retriever

• arxiv url: http://arxiv.org/abs/2501.13959v1
• Date: Tue, 21 Jan 2025 06:32:25 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-27 20:40:39.485588
• Title: Assisting Mathematical Formalization with A Learning-based Premise Retriever
• Title（参考訳）: 学習型Premise Retrieverによる数学的形式化支援
• Authors: Yicheng Tao, Haotian Liu, Shanwen Wang, Hongteng Xu,
• Abstract要約: 本稿では,数学の形式化を支援するために,前提レトリバーを訓練する革新的な手法を提案する。 我々のアプローチでは、証明状態と前提を共有潜在空間に埋め込むためにBERTモデルを採用しています。 形式化プロセスの合理化を図り,証明状態を用いてMathlibの定理を直接問合せできる検索エンジンをリリースする。
• 参考スコア（独自算出の注目度）: 29.06255449960557
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Premise selection is a crucial yet challenging step in mathematical formalization, especially for users with limited experience. Due to the lack of available formalization projects, existing approaches that leverage language models often suffer from data scarcity. In this work, we introduce an innovative method for training a premise retriever to support the formalization of mathematics. Our approach employs a BERT model to embed proof states and premises into a shared latent space. The retrieval model is trained within a contrastive learning framework and incorporates a domain-specific tokenizer along with a fine-grained similarity computation method. Experimental results show that our model is highly competitive compared to existing baselines, achieving strong performance while requiring fewer computational resources. Performance is further enhanced through the integration of a re-ranking module. To streamline the formalization process, we will release a search engine that enables users to query Mathlib theorems directly using proof states, significantly improving accessibility and efficiency. Codes are available at https://github.com/ruc-ai4math/Premise-Retrieval.
• Abstract（参考訳）: プリミゼの選択は、特に限られた経験を持つユーザーにとって、数学的形式化において決定的に難しいステップである。 形式化プロジェクトがないため、言語モデルを活用する既存のアプローチは、しばしばデータ不足に悩まされる。 本研究では,数学の形式化を支援するために,前提レトリバーを訓練する革新的な手法を提案する。 我々のアプローチでは、証明状態と前提を共有潜在空間に埋め込むためにBERTモデルを採用しています。 検索モデルは、対照的な学習フレームワーク内で訓練され、ドメイン固有のトークン化器と微粒な類似性計算手法が組み込まれている。 実験結果から,本モデルは既存のベースラインと比較して高い競争力を示し,計算資源の削減を図っている。 再ランクモジュールの統合により、パフォーマンスがさらに向上する。 形式化プロセスの合理化を目的として,ユーザが証明状態を使ってMathlibの定理を直接クエリできる検索エンジンをリリースし,アクセシビリティと効率を大幅に向上する。 コードは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)

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

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