論文の概要: Semantic Search over 9 Million Mathematical Theorems
- arxiv url: http://arxiv.org/abs/2602.05216v1
- Date: Thu, 05 Feb 2026 02:16:20 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-02-06 18:49:08.716514
- Title: Semantic Search over 9 Million Mathematical Theorems
- Title（参考訳）: 数理理論が900万を超える意味探索
- Authors: Luke Alexander, Eric Leonen, Sophie Szeto, Artemii Remizov, Ignacio Tejeda, Giovanni Inchiostro, Vasily Ilin,
- Abstract要約: 我々は、arXivと他の7つの情報源から抽出された9.2億ドルの定理文の統一コーパス上で、意味定理の検索を大規模に導入、研究する。
それぞれの定理を,検索表現として短い自然言語記述で表現し,表現コンテキスト,言語モデルの選択,埋め込みモデル,探索戦略が検索品質にどのように影響するかを体系的に分析する。
- 参考スコア（独自算出の注目度）: 0.31229177276953496
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Searching for mathematical results remains difficult: most existing tools retrieve entire papers, while mathematicians and theorem-proving agents often seek a specific theorem, lemma, or proposition that answers a query. While semantic search has seen rapid progress, its behavior on large, highly technical corpora such as research-level mathematical theorems remains poorly understood. In this work, we introduce and study semantic theorem retrieval at scale over a unified corpus of $9.2$ million theorem statements extracted from arXiv and seven other sources, representing the largest publicly available corpus of human-authored, research-level theorems. We represent each theorem with a short natural-language description as a retrieval representation and systematically analyze how representation context, language model choice, embedding model, and prompting strategy affect retrieval quality. On a curated evaluation set of theorem-search queries written by professional mathematicians, our approach substantially improves both theorem-level and paper-level retrieval compared to existing baselines, demonstrating that semantic theorem search is feasible and effective at web scale. The theorem search tool is available at \href{https://huggingface.co/spaces/uw-math-ai/theorem-search}{this link}, and the dataset is available at \href{https://huggingface.co/datasets/uw-math-ai/TheoremSearch}{this link}.
- Abstract（参考訳）: ほとんどの既存のツールは全論文を検索するが、数学者や定理証明エージェントはクエリに答える特定の定理、補題、命題を求めることが多い。
セマンティックサーチは急速に進歩してきたが、研究レベルの数学的定理のような大規模で高度なコーパスの振る舞いはいまだに理解されていない。
本研究では,arXivと7つの情報源から抽出された920万ドルの定理文を統一したコーパス上で,大規模に意味定理を検索し,研究する。
それぞれの定理を,検索表現として短い自然言語記述で表現し,表現コンテキスト,言語モデルの選択,埋め込みモデル,探索戦略が検索品質にどのように影響するかを体系的に分析する。
プロの数学者が作成した定理探索クエリのキュレートされた評価セットにおいて,提案手法は,既存のベースラインと比較して,定理レベルの検索と紙レベルの検索の両方を大幅に改善し,セマンティックな定理探索がWebスケールで実現可能かつ効果的であることを実証した。
定理検索ツールは \href{https://huggingface.co/spaces/uw-math-ai/theorem-search}{this link} で利用可能であり、データセットは \href{https://huggingface.co/datasets/uw-math-ai/theoremSearch}{this link} で利用可能である。
関連論文リスト
- DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。
DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。
我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
論文 参考訳（メタデータ） (2025-05-29T17:59:39Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。
現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。
本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
論文 参考訳（メタデータ） (2024-05-05T02:06:37Z) - Considerations on Approaches and Metrics in Automated Theorem
Generation/Finding in Geometry [0.0]
我々は、幾何定理(と性質)の自動発見のための異なるアプローチを提示し、議論する。
定理証明者が興味深い定理を生成できるかどうかを判断することは、決定論的でない課題である。
論文 参考訳（メタデータ） (2024-01-22T12:51:19Z) - A New Approach Towards Autoformalization [7.275550401145199]
オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。
研究論文は大量の背景と文脈を必要とする。
本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
論文 参考訳（メタデータ） (2023-10-12T00:50:24Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳（メタデータ） (2023-05-21T17:51:35Z) - Representer Theorems for Metric and Preference Learning: Geometric Insights and Algorithms [1.370633147306388]
ヒルベルト空間における計量および選好学習の幅広いクラスに対処する枠組みを開発する。
計量学習の一般的な課題として、我々の枠組みは単純で自己完結した表現定理に導かれる。
最後に、我々の代表者定理は、計量と選好学習のための新しい非線形アルゴリズムに導かれる。
論文 参考訳（メタデータ） (2023-04-07T16:34:25Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳（メタデータ） (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。