論文の概要: COMPOSE: Composing Future Theorems from Citations and Formal Structure
- arxiv url: http://arxiv.org/abs/2605.30333v1
- Date: Thu, 28 May 2026 17:58:42 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-30 02:45:56.744362
- Title: COMPOSE: Composing Future Theorems from Citations and Formal Structure
- Title（参考訳）: COMPOSE:Citationsとフォーマルな構造から将来の理論を構成する
- Abstract要約: そこでは、アンカー紙に対する理論的な未来的主張を生成することを目的として、基礎となる未来の数学的生成を紹介する。
科学的な引用コンテキストと形式的定理構造の両方に言語モデルを条件づけた,二重グラフフレームワークComposeを提案する。
実験の結果,Composeは検索において,将来的な論文に対して高いベースラインを達成していることがわかった。
- 参考スコア（独自算出の注目度）: 2.0503162970534947
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: A plausible future mathematical claim must satisfy two constraints: it should follow the direction of prior work and respect the formal dependencies that constrain what can validly follow. Existing approaches typically model only one of these sources, producing claims that are either weakly grounded or insufficiently motivated. We introduce grounded future mathematical generation, where the goal is to generate a plausible future theorem-like claim for an anchor paper using two complementary sources of context: its scientific citation graph and aligned formal theorem dependency graph. To address this setting, we propose COMPOSE, a dual-graph framework that conditions a language model on both scientific citation context and formal theorem structure. To support this setting, we construct a dataset of 108K paired scientific-formal graph examples from arXiv and Mathlib, together with a benchmark of 47K future papers from 2024--2025. Experiments show that COMPOSE outperforms strong baselines on retrieval to real future papers and achieves the best overall performance under LLM-judge evaluation, producing more grounded and mathematically richer outputs. These results show that future mathematical generation benefits from combining scientific context with formal structure. Project page is available at https://david-busbib.github.io/COMPOSE-page/.
- Abstract（参考訳）: 有望な将来の数学的主張は2つの制約を満たさなければならない: 先行作業の方向性に従い、有効に従えるものを制約する形式的な依存関係を尊重しなければならない。
既存のアプローチは典型的にはこれらの情報源の1つしかモデル化せず、弱い根拠を持つか不十分な動機を持つ主張を生み出している。
そこでは, 理論的引用グラフと整列形式定理依存グラフの2つの相補的な情報源を用いて, アンカー紙に対する妥当な将来の定理的主張を生成することを目的とする。
この設定に対処するため、科学的な引用コンテキストと形式的な定理構造の両方に言語モデルを条件付けるデュアルグラフフレームワークComposEを提案する。
この設定をサポートするために、arXivとMathlibから108Kペアの科学形式グラフのデータセットを構築し、2024年から2025年までの47Kの将来の論文をベンチマークした。
実験により、Composeは将来の論文の検索において高いベースラインを達成し、LLM-judge評価の下で最高の総合的な性能を達成し、より基礎的で数学的にリッチな出力を生み出すことが示された。
これらの結果は、科学的な文脈と形式的な構造を組み合わせることにより、将来の数学的生成の利点が示される。
プロジェクトページはhttps://david-busbib.github.io/COMPOSE-page/.com/で公開されている。
関連論文リスト
- FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models [53.68149869349268]
大規模言語モデル(LLM)は、自動理論計算機科学(TCS)研究の可能性を増大させている。
我々は、最前線のエンドツーエンドのTCS研究でLSMを評価するための専門家検証ベンチマークである ourbenchmarkを紹介した。
論文 参考訳（メタデータ） (2026-08-20T15:13:41Z) - TheoremGraph: Bridging Formal and Informal Mathematics [1.353002745363665]
TheoremGraphは、非公式数学と形式数学の両方にまたがる統一されたステートメントレベル依存グラフである。
非公式な側面では、数学 arXiv から 11.7M の定理のような環境を解析し、18.3M の候補指向の依存関係を復元する。
正式な面では、LeanGraphをリリースしています。Lean 4のエラボレータレベルの抽出器で、388,105の宣言ノードと11.3Mの型付きエッジを生成します。
論文 参考訳（メタデータ） (2026-06-24T03:47:05Z) - LECTOR: Joint Optimization of Scientific Reasoning Graphs and Introduction Generation [57.70907667652966]
序文は特に難解であり、論理的な健全さと検証可能な忠実さを要求する。
ほとんどのAI支援手法は、推論や構造化ではなく、タスクをテキスト生成として扱うため、深刻な欠点が生じる。
我々は,科学者の論理を厳格に追従し,高品質な引用を加え,構造化された表現を維持できる新しい論理表現協調強化学習フレームワークであるLECTORを提案する。
論文 参考訳（メタデータ） (2026-05-25T15:41:16Z) - Matlas: A Semantic Search Engine for Mathematics [2.8548596155460024]
Matlasは数学的ステートメントのセマンティック検索エンジンである。
マトラスは1826年から2025年にかけて435万件の査読論文から870万件の文書を抽出した大規模コーパス上に構築されている。
このコーパスの上に,自然言語クエリを用いた数学的結果の効率的な検索を可能にする意味検索システムを構築する。
論文 参考訳（メタデータ） (2026-04-19T15:17:28Z) - DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
DRIFTは、非公式な数学的ステートメントをより小さく、より扱いやすい'サブコンポーネント'に分解するフレームワークである。
これは、モデルが形式化タスクにおいてより効果的に前提を使用するのを助けるために、イラストラティブな定理を回収する。
我々は,様々なベンチマーク(ProofNet,ConNF,MiniF2F-test)でDRIFTを評価し,前提条件の検索を継続的に改善することを発見した。
論文 参考訳（メタデータ） (2025-10-12T21:42:04Z) - 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) - CausalCite: A Causal Formulation of Paper Citations [80.82622421055734]
CausalCiteは紙の意義を測定するための新しい方法だ。
これは、従来のマッチングフレームワークを高次元のテキスト埋め込みに適応させる、新しい因果推論手法であるTextMatchに基づいている。
科学専門家が報告した紙衝撃と高い相関性など,各種基準におけるCausalCiteの有効性を実証する。
論文 参考訳（メタデータ） (2023-11-05T23:09:39Z) - A New Approach Towards Autoformalization [7.275550401145199]
オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。
研究論文は大量の背景と文脈を必要とする。
本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
論文 参考訳（メタデータ） (2023-10-12T00:50:24Z) - Enhancing Scientific Papers Summarization with Citation Graph [78.65955304229863]
引用グラフを用いて科学論文の要約作業を再定義します。
我々は,141kの研究論文を異なる領域に格納した,新しい科学論文要約データセットセマンティックスタディネットワーク(ssn)を構築した。
我々のモデルは、事前訓練されたモデルと比較して競争性能を達成することができる。
論文 参考訳（メタデータ） (2021-04-07T11:13:35Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳（メタデータ） (2020-09-07T19:50:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。