Fugu-MT 論文翻訳(概要): EZSMT Version 3, Matured

論文の概要: EZSMT Version 3, Matured

arxiv url: http://arxiv.org/abs/2607.13344v1
Date: Wed, 15 Jul 2026 00:07:15 GMT
ステータス: 翻訳完了
システム内更新日: 2026-07-16 16:39:12.612305
Title: EZSMT Version 3, Matured
Title（参考訳）: EZSMTバージョン3が完成
Abstract要約: 本稿では,SMTベースのCASPフレームワークであるEZSMTV3の設計と実装について述べる。 EZSMTV3は、EZSMT+システムの基礎の上に、より表現力のある入力言語を導入し、弱い制約による最適化をサポートし、新しい制約型の合理化の基礎を提供する。本稿では、EZSMTV3とClingCON、ClingO[DL]、ClingO[LP]などのCASPピアを比較したベンチマーク結果を提供する。
参考スコア（独自算出の注目度）: 2.4387391584956
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Constraint Answer Set Programming (CASP) is a hybrid reasoning paradigm that combines Answer Set Programming (ASP) with Constraint Processing and Satisfiability Modulo Theories (SMT), enabling powerful declarative encodings of complex combinatorial search problems. This paper presents the design and implementation of EZSMTV3, an extensible SMT-based CASP framework that advances the translational approach to CASP solving. Building upon the foundation of the EZSMT+ system, EZSMTV3 introduces a more expressive input language, supports optimization via weak constraints, and offers foundations for streamlined integration of new constraint types. Rather than implementing custom search procedures, EZSMTV3 leverages state-of-the-art SMT solvers, such as CVC5, YICES, and Z3 to perform reasoning. The paper provides benchmarking results comparing EZSMTV3 with its CASP peers such as CLINGCON, CLINGO[DL], and CLINGO[LP], while showcasing its ability to handle mixed-domain constraints involving both integers and reals. The system provides a robust platform for future extensions and theoretical exploration within the CASP domain.
Abstract（参考訳）: Constraint Answer Set Programming (CASP)は、Answer Set Programming (ASP)とConstraint Processing and Satisfiability Modulo Theories (SMT)を組み合わせたハイブリッド推論パラダイムである。本稿では,拡張可能なSMTベースのCASPフレームワークであるEZSMTV3の設計と実装について述べる。 EZSMTV3は、EZSMT+システムの基礎の上に、より表現力のある入力言語を導入し、弱い制約による最適化をサポートし、新しい制約型の合理化の基礎を提供する。 EZSMTV3は独自のサーチプロシージャを実装するのではなく、CVC5、YICES、Z3といった最先端のSMTソルバを活用して推論を行う。本稿では、EZSMTV3をClingCON、ClingO[DL]、ClingO[LP]などのCASPピアと比較し、整数と実数の両方を含む混合ドメイン制約を扱う能力を示すベンチマーク結果を提供する。このシステムは将来の拡張とCASPドメイン内の理論的探索のための堅牢なプラットフォームを提供する。

関連論文リスト

When LLMs Develop Languages: Symbolic Communication for Efficient Multi-Agent Reasoning [85.36421257648294]
CoT(Chain-of-Thought)は、難しい推論タスクにおいて、大きな言語モデル(LLM)を改善する。コミュニケーション言語シンボリズムルーティング(R)を提案する。 Rは、それぞれの言語シンボルフレームワークを、コンパクトなシンボル、使用規則、メッセージパス契約を備えた再利用可能なシンボルプロトコルとして扱います。 Rは、標準のCoTと比較してレイテンシ指向のトークンの補完を$3sim 6times$に削減する。
論文参考訳（メタデータ） (2026-06-28T12:02:42Z)
STAIF: A Stage-wise Optimization for Complex Instruction Following [50.48101504556211]
STAIFは、客観的に検証可能な(ハード)制約の最適化から主観的(ソフト)制約のアライメントを分離する段階的な最適化フレームワークである。この方法を支援するために,約31,000の複雑なマルチ制約命令からなる高品質なバイリンガル(英語,中国語)データセットであるSTAINSTRUCTを構築した。
論文参考訳（メタデータ） (2026-06-26T06:14:07Z)
ThinkBooster: A Unified Framework for Seamless Test-Time Scaling of LLM Reasoning [110.46431027868954]
ThinkBoosterは、大規模言語モデル(LLM)推論のシームレスなテスト時間計算スケーリングのためのフレームワークである。最新のTTCスケーリング戦略とスコアファミリを実装するモジュール型のPythonライブラリで構成されている。デプロイ可能なOpenAI互換プロキシサービスにより、現実のアプリケーションへの適応推論のドロップイン統合が可能になる。
論文参考訳（メタデータ） (2026-06-05T05:28:46Z)
Structured Prompt Optimization Meets Reinforcement Learning for Global and Local Interpretability over Complex Text [14.95562040863983]
LLMには高度なテキスト分類があるが、既存のパラダイムはトレードオフに直面している。我々は,eXTCを3段階に分けて導入し,SOPを学習し,LLMから小型LMへの蒸留を推理し,初期のSOPを超えて推論能力を拡張した。この設計は、(i)コンパクトなLMによる高速な推論を可能にし、(ii)推論時局所的推論トレースと、(ii)学習されたドメインルールのグローバルなモジュラーな説明と、(iii)分類性能と説明品質の両方において、既存のパラダイムを著しく上回り、ステージバイステージゲインを実現している。
論文参考訳（メタデータ） (2026-05-27T20:29:41Z)
Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models [10.962435384504301]
我々は、TLA+状態上でIC3スタイルのプロセスを実行することにより、誘導的不変量を合成する、ニューロシンボリックなフレームワークであるIC3Synを提案する。我々は、コンセンサス、再構成、クライアントサーバシステムにまたがる29の分散プロトコル上でIC3Synを評価する。
論文参考訳（メタデータ） (2026-05-23T15:06:15Z)
SGA-MCTS: Decoupling Planning from Execution via Training-Free Atomic Experience Retrieval [74.1918709002557]
我々は, LLM計画を非パラメトリック検索として活用するフレームワークである textbfSGA-MCTS を紹介する。オンラインでは、検索増強剤は、関連するステート-ゴール-アクション原子を取得するために、ハイブリッドシンボリック-セマンティック機構を使用する。 SGA-MCTSは、探索の重い計算コストを効果的に減らし、System 1推論速度におけるシステム2推論の深さを達成し、スケーラブルかつリアルタイムに自律的な計画が実現可能である。
論文参考訳（メタデータ） (2026-04-16T07:22:36Z)
Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
シンボルレベルのプリコーディングにおいて,推論の複雑さの低いエンドツーエンドディープラーニング(DL)フレームワークを提案する。提案手法は,従来の手法よりも約80倍の高速化を実現しつつ,SLPの大幅な性能向上を達成できることを示す。
論文参考訳（メタデータ） (2025-10-02T15:15:50Z)
System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers [3.677571687801579]
ASPMTは、解集合プログラミングと満足度モジュロ理論を組み合わせるためのアプローチである。 ASPMTプログラムのきつく断片をSMTインスタンスに変換することができる。本研究では,連続的な変化を推論するために,実数計算を効果的に処理できることを実証する。
論文参考訳（メタデータ） (2025-06-12T13:59:15Z)
Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
CoT(Chain-of-Thought)は、問題を逐次ステップに分解することで、大きな言語モデル(LLM)の推論を促進する。思考のシジー(Syzygy of Thoughts, SoT)は,CoTを補助的,相互関連的な推論経路を導入して拡張する新しいフレームワークである。 SoTはより深い論理的依存関係をキャプチャし、より堅牢で構造化された問題解決を可能にする。
論文参考訳（メタデータ） (2025-04-13T13:35:41Z)
MCP-Solver: Integrating Language Models with Constraint Programming Systems [23.191983095692223]
MCPソルバは、AIシステム統合のオープンソース標準であるModel Context Protocol(MCP)を通じて、シンボル解決器でLarge Language Modelsをブリッジする。我々の実装は制約プログラミング(Minizinc)、命題満足度(PySAT)、SATモジュラー理論(Python Z3)のためのインターフェースを提供する。このシステムは、修正中のモデルの一貫性を保証し、構造化された洗練を可能にするために、反復検証を伴う編集アプローチを採用している。
論文参考訳（メタデータ） (2024-12-31T16:49:27Z)
Semantic Probabilistic Layers for Neuro-Symbolic Learning [83.25785999205932]
我々は構造化出力予測(SOP)のための予測層を設計する。予測が事前に定義されたシンボリック制約のセットと一致していることを保証するため、任意のニューラルネットワークにプラグインすることができる。我々のセマンティック確率層(SPL)は、構造化された出力空間上で複雑な相関や制約をモデル化することができる。
論文参考訳（メタデータ） (2022-06-01T12:02:38Z)
Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches [2.0559497209595814]
制約応答セットプログラミング(Constraint answer set programming、略称CASP)は、自動推論におけるハイブリッドアプローチである。これは、解集合プログラミング、制約処理、満足度モジュラー理論など、異なる研究分野の進歩をまとめている。複雑な列車スケジューリング問題を解くなど、宣言型プログラミングアプリケーションのための新たな地平を開く。
論文参考訳（メタデータ） (2021-07-17T14:58:57Z)

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

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