論文の概要: Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge
- arxiv url: http://arxiv.org/abs/2606.11430v1
- Date: Tue, 09 Jun 2026 20:29:18 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-11 16:42:38.171979
- Title: Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge
- Title（参考訳）: 書誌と形式化された数学的知識の橋梁層を目指して
- Authors: A. Mayeux,
- Abstract要約: 出版メタデータを形式的なアーティファクトと整合させるブリッジデータベースを提案する。
本稿では,論文の形式化の程度を計測する紙面形式化スコアを導入する。
このフレームワークは、フォーマルな数学的エコシステムをスケーラブルなマシン操作可能な知識に統合する最初のステップである。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Mathematical knowledge is split between bibliographic databases (e.g., MathSciNet, zbMATH Open) and formal proof libraries (e.g., Lean mathlib), preventing unified access between published results and their formalizations. We propose a relational bridge-database that aligns publication metadata with formal artifacts, providing an interoperability layer between mathematical literature and machine-verifiable proofs. We introduce a paper-level formalization score that measures how much of a publication is covered in formal systems. As a feasibility study, we show how such scores can be estimated via cross-document alignment between informal texts and Lean formalizations, enabling large-scale analysis of formalization coverage. This framework is a first step toward integrating bibliographic and formal mathematical ecosystems into scalable, machine-actionable knowledge graphs linking publications to formal proof objects.
- Abstract（参考訳）: 数学的知識は書誌データベース(例:MathSciNet、zbMATH Open)と形式証明ライブラリ(例:Lean Mathlib)に分かれており、出版結果と形式化の間の統一的なアクセスを防いでいる。
本稿では,出版メタデータを形式的アーティファクトと整合させるリレーショナルブリッジデータベースを提案する。
本稿では,出版物が形式システムでどの程度カバーされているかを測定するための紙レベルの定式化スコアを導入する。
実現可能性調査として、非公式テキストとリーンフォーマライゼーションのクロスドキュメントアライメントによって、このようなスコアを推定する方法を示し、フォーマライゼーションカバレッジの大規模分析を可能にした。
このフレームワークは、書誌的および形式的な数学的エコシステムを、出版物を形式的証明オブジェクトにリンクするスケーラブルで機械操作可能な知識グラフに統合する最初のステップである。
関連論文リスト
- Lean-GAP: A Dataset of Formalized Graduate Algebra Problems [3.1963549333419388]
本稿では,PDF-to-La Algebra前処理,Lean 4への自動形式化,非公式な形式対応の検証などからなるスケーラブルなパイプラインを開発する。
コントリビューションには、(i)形式化された演習の構造化データセットの構築、(ii)教科書数学の形式化のための体系的方法論、(iii)形式化過程における繰り返しの課題の分析が含まれる。
論文 参考訳（メタデータ） (2026-05-20T08:15:43Z) - ABCD-LINK: Annotation Bootstrapping for Cross-Document Fine-Grained Links [57.514511353084565]
我々は、最高のパフォーマンスのアプローチを選択し、文書間リンクに注釈を付けるための新しいドメインに依存しないフレームワークを提案する。
当社のフレームワークを2つの異なるドメイン – ピアレビューとニュース – に適用しています。
結果として得られた新しいデータセットは、メディアフレーミングやピアレビューなど、数多くのクロスドキュメントタスクの基礎を築いた。
論文 参考訳（メタデータ） (2025-09-01T11:32:24Z) - Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。
1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。
自己形式化定理文の自動意味評価を行う。
論文 参考訳（メタデータ） (2024-05-27T14:35:10Z) - MLFMF: Data Sets for Machine Learning for Mathematical Formalization [0.18416014644193068]
MLFMF(MLFMF)は、証明アシスタントを用いた数学の形式化を支援するために使用されるベンチマークシステムのためのデータセットの集合である。
各データセットは、AgdaやLeanの証明アシスタントで書かれた形式化された数学のライブラリから導かれる。
合計25万ドル以上のエントリーがあり、これは現在、機械学習可能な形式における公式な数学的知識のコレクションとして最大である。
論文 参考訳（メタデータ） (2023-10-24T17:00:00Z) - A New Approach Towards Autoformalization [7.275550401145199]
オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。
研究論文は大量の背景と文脈を必要とする。
本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
論文 参考訳（メタデータ） (2023-10-12T00:50:24Z) - Scientific Paper Extractive Summarization Enhanced by Citation Graphs [50.19266650000948]
我々は、引用グラフを活用して、異なる設定下での科学的論文の抽出要約を改善することに重点を置いている。
予備的な結果は、単純な教師なしフレームワークであっても、引用グラフが有用であることを示している。
そこで我々は,大規模ラベル付きデータが利用可能である場合のタスクにおいて,より正確な結果を得るために,グラフベースのスーパービジョン・サムライゼーション・モデル(GSS)を提案する。
論文 参考訳（メタデータ） (2022-12-08T11:53:12Z) - Integrating Semantics and Neighborhood Information with Graph-Driven
Generative Models for Document Retrieval [51.823187647843945]
本稿では,周辺情報をグラフ誘導ガウス分布でエンコードし,その2種類の情報をグラフ駆動生成モデルと統合することを提案する。
この近似の下では、トレーニング対象がシングルトンまたはペアワイズ文書のみを含む用語に分解可能であることを証明し、モデルが非関連文書と同じくらい効率的にトレーニングできることを示す。
論文 参考訳（メタデータ） (2021-05-27T11:29:03Z) - Enhancing Scientific Papers Summarization with Citation Graph [78.65955304229863]
引用グラフを用いて科学論文の要約作業を再定義します。
我々は,141kの研究論文を異なる領域に格納した,新しい科学論文要約データセットセマンティックスタディネットワーク(ssn)を構築した。
我々のモデルは、事前訓練されたモデルと比較して競争性能を達成することができる。
論文 参考訳（メタデータ） (2021-04-07T11:13:35Z) - Leveraging Graph to Improve Abstractive Multi-Document Summarization [50.62418656177642]
我々は、文書のよく知られたグラフ表現を活用することができる、抽象的多文書要約(MDS)モデルを開発する。
本モデルでは,長い文書の要約に欠かせない文書間関係を捉えるために,文書の符号化にグラフを利用する。
また,このモデルでは,要約生成プロセスの導出にグラフを利用することが可能であり,一貫性と簡潔な要約を生成するのに有用である。
論文 参考訳（メタデータ） (2020-05-20T13:39:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。