論文の概要: The Axiom-Based Atlas: A Structural Mapping of Theorems via Foundational Proof Vectors
- arxiv url: http://arxiv.org/abs/2504.00063v1
- Date: Mon, 31 Mar 2025 15:12:57 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-04-03 13:19:58.904845
- Title: The Axiom-Based Atlas: A Structural Mapping of Theorems via Foundational Proof Vectors
- Title（参考訳）: 公理に基づくアトラス:基礎証明ベクトルによる定理の構造マッピング
- Authors: Harim Yoo,
- Abstract要約: 公理ベースアトラス(Axiom-Based Atlas)は、数学的定理を公理系上の証明ベクトルとして構造的に表現するフレームワークである。
数学的知識を可視化し、比較し、分析する新しい方法を提供する。
自然言語の定理を解釈するプロトタイプアシスタントを導入し、おそらく証明ベクトルを提案する。
- 参考スコア（独自算出の注目度）: 0.0
- License:
- Abstract: The Axiom-Based Atlas is a novel framework that structurally represents mathematical theorems as proof vectors over foundational axiom systems. By mapping the logical dependencies of theorems onto vectors indexed by axioms - such as those from Hilbert geometry, Peano arithmetic, or ZFC - we offer a new way to visualize, compare, and analyze mathematical knowledge. This vector-based formalism not only captures the logical foundation of theorems but also enables quantitative similarity metrics - such as cosine distance - between mathematical results, offering a new analytic layer for structural comparison. Using heatmaps, vector clustering, and AI-assisted modeling, this atlas enables the grouping of theorems by logical structure, not just by mathematical domain. We also introduce a prototype assistant (Atlas-GPT) that interprets natural language theorems and suggests likely proof vectors, supporting future applications in automated reasoning, mathematical education, and formal verification. This direction is partially inspired by Terence Tao's recent reflections on the convergence of symbolic and structural mathematics. The Axiom-Based Atlas aims to provide a scalable, interpretable model of mathematical reasoning that is both human-readable and AI-compatible, contributing to the future landscape of formal mathematical systems.
- Abstract（参考訳）: 公理ベース・アトラス(Axiom-Based Atlas)は、数学的定理を基本公理系上の証明ベクトルとして構造的に表現する新しいフレームワークである。
定理の論理的依存関係をヒルベルト幾何学、ペアノ算術、ZFCなどの公理によってインデックスされたベクトルにマッピングすることで、数学的知識を視覚化し、比較し、分析する新しい方法を提供する。
このベクトルベースの形式主義は、定理の論理的基礎を捉えるだけでなく、数学的結果の間のコサイン距離のような量的類似度の測定を可能にし、構造比較のための新しい分析層を提供する。
このアトラスは、熱マップ、ベクトルクラスタリング、AI支援モデリングを用いて、数学的領域だけでなく論理構造によって定理をグループ化することができる。
また、自然言語の定理を解釈し、おそらく証明ベクトルを提案するプロトタイプアシスタント(Atlas-GPT)を導入し、自動推論、数学的教育、形式検証における将来の応用を支援する。
この方向は、テレンス・タオの記号数学と構造数学の収束に関する最近の考察に部分的にインスピレーションを受けている。
Axiom-Based Atlasは、人間の可読性とAI互換性の両方を備えた、スケーラブルで解釈可能な数学的推論モデルを提供することを目標としている。
関連論文リスト
- One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [57.48325300739872]
証明生成のための数学的大規模言語モデルを活用することは、LLM研究の基本的なトピックである。
現状のLCMが証明できる能力は、学習中に関連する証明プロセスに遭遇したかどうかに大きく依存していると論じる。
人間の数学教育で一般的に用いられる「反例による防御」の教育的手法に触発されて,我々の研究は,反例を通して数学的推論と証明を行うLLMの能力を高めることを目的としている。
論文 参考訳（メタデータ） (2025-02-12T02:01:10Z) - Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
ミニモ(Minimo)は、自分自身に問題を起こし、それを解決することを学ぶエージェント(理論実証)である。
制約付き復号法と型指向合成法を組み合わせて、言語モデルから有効な予想をサンプリングする。
我々のエージェントは、ハードだが証明可能な予想を生成することを目標としています。
論文 参考訳（メタデータ） (2024-06-30T13:34:54Z) - Machine learning and information theory concepts towards an AI
Mathematician [77.63761356203105]
人工知能の現在の最先端技術は、特に言語習得の点で印象的だが、数学的推論の点ではあまり重要ではない。
このエッセイは、現在のディープラーニングが主にシステム1の能力で成功するという考えに基づいている。
興味深い数学的ステートメントを構成するものについて質問するために、情報理論的な姿勢を取る。
論文 参考訳（メタデータ） (2024-03-07T15:12:06Z) - Beyond Operator Systems [0.0]
作用素系は作用素代数、自由半代数幾何学、量子情報理論を結合する。
この研究において、作用素系とその定理の多くを一般化する。
論文 参考訳（メタデータ） (2023-12-21T16:16:27Z) - Pregeometry, Formal Language and Constructivist Foundations of Physics [0.0]
我々は、量子幾何学の新しい概念と既存の概念が基礎となる前幾何学構造のメタ物理について論じる。
我々は、形式言語、特にホモトピー型理論の枠組みが前幾何学理論の概念的構成要素を提供することを示す証拠に注意を向ける。
論文 参考訳（メタデータ） (2023-11-07T13:19:29Z) - math-PVS: A Large Language Model Framework to Map Scientific
Publications to PVS Theories [10.416375584563728]
本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。
我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
論文 参考訳（メタデータ） (2023-10-25T23:54:04Z) - From axioms over graphs to vectors, and back again: evaluating the
properties of graph-based ontology embeddings [78.217418197549]
埋め込みを生成するアプローチの1つは、名前付きエンティティと論理公理構造のためのノードとエッジのセットを導入することである。
グラフに埋め込む方法(グラフ射影)は、それらが利用する公理の種類と異なる性質を持つ。
論文 参考訳（メタデータ） (2023-03-29T08:21:49Z) - OntoMath${}^{\mathbf{PRO}}$ 2.0 Ontology: Updates of the Formal Model [68.8204255655161]
主な関心は、Open Linked Dataクラウドにおける数学的ステートメントを表現するための形式モデルの開発である。
提案モデルは、自然言語の数学的テキストから数学的事実を抽出し、これらの事実をLinked Open Dataとして表現するアプリケーションを対象としている。
このモデルは OntoMath$mathrmPRO$ ontology of professional mathematics の新バージョンの開発に使用される。
論文 参考訳（メタデータ） (2023-03-17T20:29:17Z) - Formalising Concepts as Grounded Abstractions [68.24080871981869]
このレポートは、表現学習が生データから概念を誘導する方法を示しています。
このレポートの主な技術的目標は、表現学習のテクニックが概念空間の格子理論的定式化とどのように結婚できるかを示すことである。
論文 参考訳（メタデータ） (2021-01-13T15:22:01Z) - Noisy Deductive Reasoning: How Humans Construct Math, and How Math
Constructs Universes [0.5874142059884521]
本稿では,数学が基本的な過程である数学的推論の計算モデルを提案する。
この枠組みが数学的実践のいくつかの側面について説得力のある説明を与えることを示す。
論文 参考訳（メタデータ） (2020-10-28T19:43:14Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳（メタデータ） (2020-09-07T19:50:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。