論文の概要: Dependency Graphs of Mathematical Arguments: Representation, Structural Measurement, and Proof Review
- arxiv url: http://arxiv.org/abs/2610.36776v1
- Date: Tue, 27 Oct 2026 07:44:14 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-29 04:15:49.24227
- Title: Dependency Graphs of Mathematical Arguments: Representation, Structural Measurement, and Proof Review
- Title（参考訳）: 数学的論証の依存関係グラフ:表現、構造計測、証明
- Abstract要約: 本研究では,大規模言語モデルの助けを借りて数学的議論を表現・測定するための基盤となるフレームワークを提案する。
数式と無数のステートメント、方程式、仮定、構成が含まれており、発生元を文脈の状態や推測記録と区別している。
測定コントラクトは、原稿のバージョン、バウンダリ、粒度、証明の選択、マクロアンカーを修正する。
- 参考スコア（独自算出の注目度）: 2.495906039848052
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We propose a source-grounded framework for representing and measuring mathematical arguments with assistance from large language models. It includes numbered and unnumbered statements, equations, assumptions, and constructions, distinguishing source occurrences from contextual states and inference records. Proposed dependencies retain source evidence and review status. A measurement contract fixes manuscript versions, boundaries, granularity, proof choices, and macro anchors. On a selected finite directed acyclic graph, depth is the longest prerequisite-path length, and bulk counts distinct ancestor edges. We give a union recurrence that accounts for shared subarguments and identify reachability conditions preserving depth and the macro skeleton; unrestricted refinement need not preserve depth or bulk. A standardized, versioned prompt protocol separates annotation discovery, deterministic recomputation, and review assistance. Cross-paper links support a research agenda on theorem co-use, rare combinations, and connections between dependency communities. These patterns motivate probabilistic premise suggestions and review of possible omissions or unchecked application conditions in human-written and AI-generated proofs. Further applications include source-linked reading support and comparison of individual and collaborative argument shapes. We provide an evaluation design rather than empirical evidence of these benefits. Suggested premises require mathematical validation, and the measures describe a specified representation rather than intrinsic mathematical difficulty, originality, or importance.
- Abstract（参考訳）: 本研究では,大規模言語モデルの助けを借りて数学的議論を表現・測定するための基盤となるフレームワークを提案する。
数式と無数のステートメント、方程式、仮定、構成が含まれており、発生元を文脈の状態や推測記録と区別している。
提案された依存関係は、ソースエビデンスとレビューステータスを保持します。
測定コントラクトは、原稿のバージョン、バウンダリ、粒度、証明の選択、マクロアンカーを修正する。
選択された有限有向非巡回グラフ上では、深さは最も長い前提パス長であり、バルクは異なる祖先の縁を数えている。
我々は,共有された部分空間を考慮し,深度とマクロ骨格を保存した到達性条件を同定する団結再発を与える。
標準化されたバージョン付きプロンプトプロトコルは、アノテーション発見、決定論的再計算、レビュー支援を分離する。
クロスペーパーリンクは、定理のコユース、稀な組み合わせ、依存関係コミュニティ間の接続に関する研究の議題を支持している。
これらのパターンは、人間による記述とAI生成の証明において、確率論的前提の提案と、省略や未確認のアプリケーション条件のレビューを動機付けている。
さらに、ソースリンク読解支援や、個別および協調的な引数形状の比較などが含まれる。
これらの利点の実証的な証拠ではなく、評価設計を提供する。
提案された前提は数学的検証を必要とし、その尺度は固有の数学的困難、独創性、重要性よりも、特定の表現を記述する。
関連論文リスト
- MechAlign: Evaluating Semantic Alignment at the Project Level in Mathematical Formalization [18.986093919008827]
プロジェクトレベルのセマンティックアライメントレビューのためのフレームワークであるMechAlignを紹介します。
我々は173のOpenAI Mathプロジェクトから201の主要な成果の予備的なレビューを行う。
また、OpenAI Math、FermatのLast Theorem、Kakeyaの501の固定クレームステートメント-コンテキストトリプルで構成されたLeanReviewBenchを構築します。
論文 参考訳（メタデータ） (2026-10-26T11:44:26Z) - Lean Graph Search for Formal Theorem Proving [82.31440013289564]
グラフに基づくLean4の検索手法であるLeanGraphSearchを提案する。
Mathlibのフォワード依存関係からグラフを構築し、それをトラバースして、サポート対象の補題を明らかにする。
3つの定理証明ベンチマークで、LeanGraphSearchは8, 16, 32リフレクションのパスレートをバニラ証明よりも40%向上させる。
論文 参考訳（メタデータ） (2026-10-15T17:55:21Z) - When benchmark inferences do not compose: Projectibility in AI evaluation [0.0]
AIベンチマークの結果が1ステップで連続的なクレームに達することはめったにない。
評価者はそれをさらなるケースに一般化し、能力の証拠として解釈し、新しいタスクに外挿し、他のシステムやサイトへ輸送する。
保証リンクは保証チェーンを自動的に作らない。
論文 参考訳（メタデータ） (2026-07-28T18:07:04Z) - HiEviDR-Bench: A Benchmark for Hierarchical Evidence Aggregation in Deep Research [52.87128503345243]
我々は,Deep Researchにおける階層的エビデンス・アグリゲーションを評価するためのベンチマークであるHiEviDR-Benchを紹介する。
HiEviDR-Benchは、エビデンスの選択、クロスソースリンク、アグリゲーションをキャプチャする明示的なエビデンスグラフを持つ各インスタンスを表す。
報告品質,エビデンストレーサビリティ,引用精度,クレーム検証,回答正当性という5次元のトレーサビリティ指向評価フレームワークを開発した。
論文 参考訳（メタデータ） (2026-07-27T23:50:46Z) - Finite Certificates for In-Context Determinacy and a Threshold Theory of Emergence in Language Models [0.2864713389096699]
本稿では,文脈条件付き言語モデル行動を検証するためのモデル理論フレームワークを開発する。
有限コンテキスト証明書、ペアセパレータのヒットセット、クエリ教育のディメンション、プロンプト保存基準、スケール制限証人を提供する。
論文 参考訳（メタデータ） (2026-05-30T14:07:58Z) - Towards Verifiable Multimodal Deep Research: A Multi-Agent Harness for Interleaved Report Generation [74.0621258662676]
レポート生成のためのマルチエージェントハーネスであるPtahを提案する。
Ptahは計画、研究、執筆段階を通じて、ユーザクエリからレンダリングされたWebレポートまでのライフサイクルを編成する。
検証エージェントがハーネスの受け入れ機能として機能し、ワークフロー全体を通して事実的接地、引用の忠実性、相互の整合性を強制する。
論文 参考訳（メタデータ） (2026-05-28T12:40:34Z) - Prototype-based Aleatoric Uncertainty Quantification for Cross-modal
Retrieval [139.21955930418815]
クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。
しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。
本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
論文 参考訳（メタデータ） (2023-09-29T09:41:19Z) - Admissibility in Strength-based Argumentation: Complexity and Algorithms
(Extended Version with Proofs) [1.5828697880068698]
我々は、適応性に基づく意味論の強度に基づく論証フレームワーク(StrAF)への適応について研究する。
特に文献で定義された強い許容性は望ましい性質、すなわちDungの基本的な補題を満たさないことを示す。
計算(強弱)拡張に対する擬ブール制約の翻訳を提案する。
論文 参考訳（メタデータ） (2022-07-05T18:42:04Z) - Graph-based Retrieval for Claim Verification over Cross-Document
Evidence [0.6853165736531939]
グラフに基づくアプローチは、断片化された証拠を特定するのに役立つと推測する。
我々はこの仮説を、コーパス全体にわたって、上述したエンティティによってテキスト部分を相互接続する大きなグラフを構築して検証した。
実験により,グラフ構造を活用することは,クレームに関連する通路のごく一部を特定する上で有益であることが確認された。
論文 参考訳（メタデータ） (2021-09-13T14:54:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。