論文の概要: Theta as a Horn Solver

• arxiv url: http://arxiv.org/abs/2510.26430v1
• Date: Thu, 30 Oct 2025 12:24:52 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-31 16:05:09.804864
• Title: Theta as a Horn Solver
• Title（参考訳）: ホーンソルバーとしてのテータ
• Authors: Levente Bajczi, Milán Mondok, Vince Molnár,
• Abstract要約: Thetaは、2023年からCHC-COMPコンペティションに参加している検証フレームワークである。 本稿では、Thetaが採用しているアルゴリズムの詳細な説明を行い、他のCHCソルバと区別するユニークな特徴を強調した。 また、CHC-COMPベンチマークの文脈でツールの長所と短所を分析する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Theta is a verification framework that has participated in the CHC-COMP competition since 2023. While its core approach -- based on transforming constrained Horn clauses (CHCs) into control-flow automata (CFAs) for analysis -- has remained mostly unchanged, Theta's verification techniques, design trade-offs, and limitations have remained mostly unexplored in the context of CHCs. This paper fills that gap: we provide a detailed description of the algorithms employed by Theta, highlighting the unique features that distinguish it from other CHC solvers. We also analyze the strengths and weaknesses of the tool in the context of CHC-COMP benchmarks. Notably, in the 2025 edition of the competition, Theta's performance was impacted by a configuration issue, leading to suboptimal results. To provide a clearer picture of Theta's actual capabilities, we re-execute the tool on the competition benchmarks under corrected settings and report on the resulting performance.
• Abstract（参考訳）: Thetaは、2023年からCHC-COMPコンペティションに参加している検証フレームワークである。 分析のために制約付きホーン節(CHC)を制御フローオートマトン(CFA)に変換するというその中核的なアプローチは、ほとんど変わっていないが、Thetaの検証技術、設計上のトレードオフ、制限は、CHCの文脈でほとんど探索されていない。 本稿では,そのギャップを埋める: Thetaが採用するアルゴリズムの詳細な説明を行い,他のCHCソルバと区別するユニークな特徴を強調した。 また、CHC-COMPベンチマークの文脈でツールの長所と短所を分析する。 2025年のコンペティションでは、セタのパフォーマンスは設定の問題の影響を受け、準最適結果となった。 Thetaの実際の機能をより明確にするために、私たちは、修正された設定の下で競合ベンチマーク上でツールを再実行し、その結果のパフォーマンスを報告します。

関連論文リスト

• CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses [0.0]
  制約付きホーンクロース(CHC)は、検証タスクの中間表現として広く採用されている。 本稿では,CHCを解くためのソフトウェア検証アプローチを採用するポートフォリオベースのCHCソルバを紹介する。
  論文  参考訳（メタデータ） (2025-10-30T12:25:06Z)
• Link Prediction for Event Logs in the Process Industry [4.139846693958609]
  Record Linking (RL) は、自然言語推論(NLI)と意味テキスト類似性(STS)によって強化されたクロスドキュメント・コア参照解決(CDCR)タスクである。 我々は、伝統的にニュースドメインに適用されるCDCRを、プロセス産業の特定のテキストフォーマットを調整しながら、NLIやSTSのような通過レベルで運用するために、RLモデルに適応する。 我々の研究は、推論能力によって強化された最先端CDCRモデルのドメイン適応が、プロセス産業に効果的に適合できることを示す。
  論文  参考訳（メタデータ） (2025-08-12T17:22:29Z)
• Sliding Window Informative Canonical Correlation Analysis [0.0]
  カノニカル相関解析(Canonical correlation analysis, CCA)は、2つのデータセット間の相関した特徴集合を見つける手法である。 Sliding Window Informative Canonical correlation Analysis (SWICCA) によるオンラインストリーミングデータ設定へのCCAの新たな拡張を提案する。
  論文  参考訳（メタデータ） (2025-07-23T20:35:15Z)
• Tuning for Trustworthiness -- Balancing Performance and Explanation Consistency in Neural Network Optimization [49.567092222782435]
  我々は,異なる特徴帰属法間の合意として定義された,XAI整合性という新しい概念を紹介する。 予測性能と説明のバランスをとる多目的最適化フレームワークを構築した。 本研究は、トレードオフゾーンバランス性能損失とXAI整合性による強靭性向上のモデルについて、今後の研究基盤を提供する。
  論文  参考訳（メタデータ） (2025-05-12T13:19:14Z)
• EFaR 2023: Efficient Face Recognition Competition [51.77649060180531]
  バイオメトリックス国際会議(IJCB 2023)における効率的な顔認識コンペティション(EFaR)の概要について述べる。 この競技会は6つの異なるチームから17の応募を受けた。 提案したソリューションは、様々なベンチマークで達成された検証精度の重み付けスコアと、浮動小数点演算数とモデルサイズによって与えられるデプロイ可能性に基づいてランク付けされる。
  論文  参考訳（メタデータ） (2023-08-08T09:58:22Z)
• Better Handling Coreference Resolution in Aspect Level Sentiment Classification by Fine-Tuning Language Models [4.2605449879340656]
  Aspect Level Sentiment Classification (ALSC) による顧客フィードバック監視の自動化 大規模言語モデル(LLM)は多くの最先端のALSCソリューションの中心であるが、Coreference Resolution (CR)を必要とするいくつかのシナリオでは性能が悪くなっている。 本稿では,CRを含むレビューにおけるLLMの性能向上のためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2023-07-11T12:43:28Z)
• CTC Alignments Improve Autoregressive Translation [145.90587287444976]
  我々はCTCが共同のCTC/アテンションフレームワークに適用された場合、実際に翻訳に意味があることを論じる。 提案した共同CTC/アテンションモデルは6つのベンチマーク翻訳タスクにおいて純粋アテンションベースラインを上回った。
  論文  参考訳（メタデータ） (2022-10-11T07:13:50Z)
• Performance Evaluation of Adversarial Attacks: Discrepancies and Solutions [51.8695223602729]
  機械学習モデルの堅牢性に挑戦するために、敵対攻撃方法が開発されました。 本稿では,Piece-wise Sampling Curving(PSC)ツールキットを提案する。 psc toolkitは計算コストと評価効率のバランスをとるオプションを提供する。
  論文  参考訳（メタデータ） (2021-04-22T14:36:51Z)
• Visual Alignment Constraint for Continuous Sign Language Recognition [74.26707067455837]
  ビジョンベースの継続的署名言語認識は、画像シーケンスから未分割ジェスチャーを認識することを目的とする。 本研究は,最近のCTCに基づくCSLRにおける過剰適合問題を再考し,特徴抽出器の訓練不足によるものである。 視覚アライメント制約(vac)により、よりアライメントの監督により特徴抽出器を強化する。
  論文  参考訳（メタデータ） (2021-04-06T07:24:58Z)
• CIF-based Collaborative Decoding for End-to-end Contextual Speech Recognition [14.815422751109061]
  コンテキストバイアスをより制御可能な方法でサポートするCIF(Continuous Integration-and-fire)ベースのモデルを提案する。 追加のコンテキスト処理ネットワークを導入し、コンテキスト埋め込みを抽出し、音響的に関連するコンテキスト情報を統合し、コンテキスト出力分布をデコードする。 提案手法は, 強ベースラインと比較して, 相対的文字誤り率 (CER) の8.83%/21.13%, 相対的名前付きエンティティ文字誤り率 (NE-CER) の40.14%/51.50%削減を実現する。
  論文  参考訳（メタデータ） (2020-12-17T09:40:11Z)

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

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