論文の概要: 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 14:58:42.093539
• 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:
• 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で公開されている。

関連論文リスト

• 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)
• RAVEN: In-Context Learning with Retrieval-Augmented Encoder-Decoder Language Models [57.12888828853409]
  RAVENは検索強化されたマスク付き言語モデリングとプレフィックス言語モデリングを組み合わせたモデルである。 フュージョン・イン・コンテキスト・ラーニング(Fusion-in-Context Learning)により、追加のトレーニングを必要とせずに、より多くのコンテキスト内サンプルを利用できる。 本研究は,テキスト内学習のためのエンコーダ・デコーダ言語モデルの構築の可能性を明らかにするものである。
  論文  参考訳（メタデータ） (2023-08-15T17:59:18Z)
• 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)
• 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)
• 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)
• Combining Federated and Active Learning for Communication-efficient Distributed Failure Prediction in Aeronautics [0.0]
  我々は,アクティブラーニングとフェデレートラーニングの学習パラダイムに依存する,新しい集中型分散学習アルゴリズムを提案する。 我々は,この手法を公開ベンチマークで評価し,その精度が非分散学習の最先端性能レベルに非常に近いことを示す。
  論文  参考訳（メタデータ） (2020-01-21T13:17:00Z)

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

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