論文の概要: Does My Embedding Reflect That $A = B$? Evaluating Mathematical Equivalence in Embedding Models
- arxiv url: http://arxiv.org/abs/2606.23959v1
- Date: Mon, 22 Jun 2026 21:37:58 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-24 22:16:48.694441
- Title: Does My Embedding Reflect That $A = B$? Evaluating Mathematical Equivalence in Embedding Models
- Title(参考訳): 私の埋め込みは$A = B$を反映しているか? 埋め込みモデルにおける数学的等価性の評価
- Authors: Jiaying Ye, Samarth Rao, Leo Carlin, Kedar Chintalapati, Saharsh Bhargava, Rachit Jaiswal, Michael Zhou, Jared Darlington, Jarod Alper, Vasily Ilin, Henry Kvinge,
- Abstract要約: 単一のステートメントは、どのサブフィールドがフレーム化されているかによって、非常に異なる形式を取ることができる。
現在の埋め込みモデルは、基礎となる数学の代わりにそれらを作るために使われる用語によってステートメントをグループ化する傾向がある。
本稿では,形式化の異なる文の整合性に着目した数学的テキストの埋め込み学習に対する対照的なアプローチを提案する。
- 参考スコア(独自算出の注目度): 4.58405745969332
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Because mathematics is highly abstract, a single statement can take very different forms depending on what subfield it is framed in. There are many examples where breakthroughs occurred after researchers discovered that a question had already been answered in a different field. At the same time, the growth of new resources related to formalization has increased the need for tools that enable efficient and reliable navigation between mathematical 'languages' (e.g., from Lean to natural language). In this paper, we investigate whether current embedding models capture mathematical equivalence. To do this, we introduce the Mathematically Equivalent but Lexically Different Pairs (MELD) Dataset, a collection of mathematically equivalent statements that are expressed in very different language. We show that current state-of-the-art embedding models tend to group statements by the terminology used to make them instead of the underlying math. Motivated by this, we propose a contrastive approach to learning embeddings of mathematical text that focuses on aligning informal statements with different formalizations. Our experiments demonstrate that this leads to improvements not only on informal-formal retrieval tasks but also on MELD, which only contains natural language statements.
- Abstract(参考訳): 数学は非常に抽象的であるため、単一のステートメントは、どのサブフィールドがフレーム化されているかによって、非常に異なる形式をとることができる。
研究者が、ある質問がすでに別の分野で答えられていることを発見した後に、ブレークスルーが発生した例は多数ある。
と同時に、形式化に関連する新たなリソースの増加は、数学的'言語'(例えば、リーンから自然言語)間の効率的で信頼性の高いナビゲーションを可能にするツールの必要性を高めています。
本稿では,現在の埋め込みモデルが数学的等価性を捉えているかどうかを考察する。
そこで我々は, 数学的に等価な文の集合であるMELD(Mathematically Equivalent but Lexically Different Pairs)データセットを導入する。
現在の最先端の埋め込みモデルは、基礎となる数学ではなく、それらを作るために使われる用語によって、ステートメントをグループ化する傾向があることを示す。
そこで本研究では,形式化の異なる非公式な文の整合性に着目した数学的テキストの埋め込みを学習するための対照的なアプローチを提案する。
実験の結果,これは形式的検索タスクだけでなく,自然言語文のみを含むMELDにも改善をもたらすことが示された。
関連論文リスト
- An Algebraic View of the Expressivity of Recurrent Language Models [50.88598486616582]
本稿では、繰り返しニューラルネットワークの表現性に関する統一的代数的記述法を開発する。
同じアーキテクチャでは、浮動小数点反復が強制されると偶モジュラーカウンタを実装することはできないが、符号付き整数量子化の下ではすべての偶モジュラーカウンタを実現する。
論文 参考訳(メタデータ) (2026-06-01T06:47:58Z) - The Unreasonable Effectiveness of Model Merging for Cross-Lingual Transfer in LLMs [45.08958917457921]
大規模言語モデル(LLM)は、ハイソース言語以外のタスクで依然として苦戦している。
本研究では,タスク固有のポストトレーニングデータが不足している低リソース言語への言語間移動について検討する。
論文 参考訳(メタデータ) (2025-05-23T20:28:31Z) - LemmaHead: RAG Assisted Proof Generation Using Large Language Models [0.0]
我々は、関連する数学的文脈でモデルにクエリを補足する知識ベースであるLemmaHeadを開発した。
数学的推論におけるモデルの性能を測定するため、我々のテストパラダイムは自動定理証明の課題に焦点を当てている。
論文 参考訳(メタデータ) (2025-01-27T05:46:06Z) - TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative
Language Models [68.65075559137608]
本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。
我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。
我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
論文 参考訳(メタデータ) (2023-10-16T08:42:39Z) - A New Approach Towards Autoformalization [7.275550401145199]
オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。
研究論文は大量の背景と文脈を必要とする。
本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
論文 参考訳(メタデータ) (2023-10-12T00:50:24Z) - Tree-Based Representation and Generation of Natural and Mathematical
Language [77.34726150561087]
科学コミュニケーションと教育シナリオにおける数学的言語は重要であるが、比較的研究されている。
数学言語に関する最近の研究は、スタンドアローンな数学的表現や、事前訓練された自然言語モデルにおける数学的推論に焦点をあてている。
テキストと数学を共同で表現・生成するために,既存の言語モデルに対する一連の修正を提案する。
論文 参考訳(メタデータ) (2023-02-15T22:38:34Z) - Towards a Mathematics Formalisation Assistant using Large Language
Models [5.485439959027125]
リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。
コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。
新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
論文 参考訳(メタデータ) (2022-11-14T16:52:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。