論文の概要: Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deduction

• arxiv url: http://arxiv.org/abs/2510.10701v1
• Date: Sun, 12 Oct 2025 17:03:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-14 20:23:38.94133
• Title: Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deduction
• Title（参考訳）: 拡張三角法: 相関分離に基づく自動推論のための一般化アルゴリズム
• Authors: Yang Xu, Shuwei Chen, Jun Liu, Feng Cao, Xingxing He,
• Abstract要約: この研究は、矛盾分離の内部機構を形式化し拡張する一般化された矛盾構築アルゴリズムである拡張三角法(ETM)を提示する。 理論的抽象化と運用実装をブリッジすることで、EMMは矛盾分離パラダイムを、自動化推論のための一般化されたスケーラブルで実用的な競合モデルに進化させる。
• 参考スコア（独自算出の注目度）: 11.18154335347018
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated deduction lies at the core of Artificial Intelligence (AI), underpinning theorem proving, formal verification, and logical reasoning. Despite decades of progress, reconciling deductive completeness with computational efficiency remains an enduring challenge. Traditional reasoning calculi, grounded in binary resolution, restrict inference to pairwise clause interactions and thereby limit deductive synergy among multiple clauses. The Contradiction Separation Extension (CSE) framework, introduced in 2018, proposed a dynamic multi-clause reasoning theory that redefined logical inference as a process of contradiction separation rather than sequential resolution. While that work established the theoretical foundation, its algorithmic realization remained unformalized and unpublished. This work presents the Extended Triangular Method (ETM), a generalized contradiction-construction algorithm that formalizes and extends the internal mechanisms of contradiction separation. The ETM unifies multiple contradiction-building strategies, including the earlier Standard Extension method, within a triangular geometric framework that supports flexible clause interaction and dynamic synergy. ETM serves as the algorithmic core of several high-performance theorem provers, CSE, CSE-E, CSI-E, and CSI-Enig, whose competitive results in standard first-order benchmarks (TPTP problem sets and CASC 2018-2015) empirically validate the effectiveness and generality of the proposed approach. By bridging theoretical abstraction and operational implementation, ETM advances the contradiction separation paradigm into a generalized, scalable, and practically competitive model for automated reasoning, offering new directions for future research in logical inference and theorem proving.
• Abstract（参考訳）: 自動推論は人工知能(AI)の中核にある。 何十年にもわたる進歩にもかかわらず、導出的完全性と計算効率の整合性は持続的な課題である。 従来の推論計算は二項分解に基礎を置いており、推論を対の節間相互作用に制限し、それによって複数の節間の還元的相乗性を制限する。 2018年に導入されたコントラディション分離拡張(CSE)フレームワークは、逐次分解ではなく矛盾分離の過程として論理推論を再定義する動的多項推論理論を提案した。 この研究は理論の基礎を確立したが、アルゴリズム的実現は形式化されず、未発表のままであった。 この研究は、矛盾分離の内部機構を形式化し拡張する一般化された矛盾構築アルゴリズムである拡張三角法(ETM)を提示する。 ETMは、フレキシブルな節間相互作用と動的シナジーをサポートする三角形の幾何学的フレームワークにおいて、以前のStandard Extensionメソッドを含む複数の矛盾構築戦略を統一する。 ETMはCSE、CSE-E、CSI-E、CSI-Enigのアルゴリズムコアとして機能し、標準的な1次ベンチマーク(TPTP問題セットとCASC 2018-2015)で競合する結果が提案手法の有効性と一般化を実証的に検証している。 理論的抽象化と運用的実装をブリッジすることで、EMMは矛盾分離パラダイムを、自動推論のための一般化されたスケーラブルで実用的な競争モデルに進化させ、将来の論理的推論と定理証明の方向性を提供する。

関連論文リスト

• Step-Aware Policy Optimization for Reasoning in Diffusion Large Language Models [57.42778606399764]
  拡散言語モデル(dLLM)は、テキスト生成に有望で非自己回帰的なパラダイムを提供する。 現在の強化学習アプローチは、しばしばスパースで結果に基づく報酬に頼っている。 これは推論の自然な構造との根本的なミスマッチに由来すると我々は主張する。
  論文  参考訳（メタデータ） (2025-10-02T00:34:15Z)
• Contradictions [9.602468627573215]
  本稿では,標準矛盾を体系的に構築することに焦点を当てる。 本稿では,最大標準矛盾による節集合の満足度と不満足度を決定する手法を提案する。 最大三角形標準矛盾と三角型標準矛盾の両方に埋め込まれた標準部分矛盾の数を計算するための公式を導出する。
  論文  参考訳（メタデータ） (2025-09-07T13:47:51Z)
• Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
  大規模言語モデル(LLM)は、幅広いタスクにまたがる強力な一般化を実証している。 最近の研究は、暗黙の推論に拍車をかけた、明示的な思考の連鎖から注意を向けている。 本調査では,表現形式から計算戦略へ焦点を移し,実行パラダイムを中心とした分類を紹介した。
  論文  参考訳（メタデータ） (2025-09-02T14:16:02Z)
• CTRLS: Chain-of-Thought Reasoning via Latent State-Transition [57.51370433303236]
  チェーン・オブ・シント(CoT)推論は、大規模な言語モデルで複雑な問題を解釈可能な中間ステップに分解することを可能にする。 我々は,遅延状態遷移を伴うマルコフ決定プロセス(MDP)としてCoT推論を定式化するフレームワークであるgroundingSを紹介する。 我々は、ベンチマーク推論タスクにおける推論精度、多様性、探索効率の改善を示す。
  論文  参考訳（メタデータ） (2025-07-10T21:32:18Z)
• PixelThink: Towards Efficient Chain-of-Pixel Reasoning [70.32510083790069]
  PixelThinkは、外部から推定されるタスクの難しさと内部で測定されたモデルの不確実性を統合する、シンプルで効果的なスキームである。 シーンの複雑さと予測信頼度に応じて推論の長さを圧縮することを学ぶ。 実験により,提案手法は推論効率と全体セグメンテーション性能の両方を改善した。
  論文  参考訳（メタデータ） (2025-05-29T17:55:49Z)
• On the Diagram of Thought [20.805936414171892]
  大規模言語モデル(LLM)は多くのタスクで優れているが、構造化された多段階の推論を必要とする複雑な問題に悩まされることが多い。 思考のダイアグラム(Diagram of Thought, DoT)は、1つのLCMがその推論のメンタルマップを構築し、ナビゲートすることを可能にする新しいフレームワークである。
  論文  参考訳（メタデータ） (2024-09-16T07:01:41Z)
• Answering Causal Queries at Layer 3 with DiscoSCMs-Embracing Heterogeneity [0.0]
  本稿では, 分散一貫性構造因果モデル (DiscoSCM) フレームワークを, 反事実推論の先駆的アプローチとして提唱する。
  論文  参考訳（メタデータ） (2023-09-17T17:01:05Z)
• Understanding and Constructing Latent Modality Structures in Multi-modal Representation Learning [53.68371566336254]
  優れたパフォーマンスの鍵は、完全なモダリティアライメントではなく、有意義な潜在モダリティ構造にある、と我々は主張する。 具体的には,1)モダリティ内正規化のための深い特徴分離損失,2)モダリティ間正規化のためのブラウン橋損失,3)モダリティ内正規化およびモダリティ間正規化のための幾何学的整合損失を設計する。
  論文  参考訳（メタデータ） (2023-03-10T14:38:49Z)
• Making Linear MDPs Practical via Contrastive Representation Learning [101.75885788118131]
  マルコフ決定過程(MDP)における次元性の呪いに、低ランク表現を利用することで対処することが一般的である。 本稿では,効率的な表現学習を可能にしつつ,正規化を自動的に保証する線形MDPの代替的定義について考察する。 いくつかのベンチマークにおいて、既存の最先端モデルベースおよびモデルフリーアルゴリズムよりも優れた性能を示す。
  論文  参考訳（メタデータ） (2022-07-14T18:18:02Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。