論文の概要: Reset Early, Reset Often, Eliminate Models

• arxiv url: http://arxiv.org/abs/2610.18204v1
• Date: Tue, 13 Oct 2026 11:39:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-15 21:06:15.605222
• Title: Reset Early, Reset Often, Eliminate Models
• Title（参考訳）: Reset Early, Reset Often, Elimination Models
• Abstract要約: SATResetCoPは、非生産的なテーブル上でのバックトラックを行わず、この永続的なSAT状態に依存します。 TPTPでは、SATResetCoPはリーンCoPスタイルのベースラインを54%改善し、SATCoPスタイルのベースラインを18%改善しました。 MPTP2078ベンチマークでは、616の問題を解決し、LeanCoPスタイルのベースラインを49%改善し、SATCoPスタイルのベースラインを12%改善しました。
• 参考スコア（独自算出の注目度）: 0.6537940428724028
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Connection-tableau provers typically construct closed tableaux by backtracking search. This gives lightweight proof procedures, but their low-memory search state leaves little derived information to reuse after a failed attempt. SATCoP addresses this by retaining grounded tableau clauses in an incremental SAT solver, allowing the prover to refute the problem once the accumulated ground clauses become propositionally unsatisfiable. We introduce SATResetCoP, which relies more directly on this persistent SAT state by not backtracking on unproductive tableaux and instead starting new ones to generate further ground clauses for the SAT solver. On TPTP, SATResetCoP improves over our leanCoP-style baseline by 54% and our SATCoP-style baseline by 18%. On the bushy MPTP2078 benchmark, it solves 616 problems, a 49% improvement over our leanCoP-style baseline and a 12% improvement over our SATCoP-style baseline. These results suggest that changing tableau guidance to accumulate useful ground clauses faster improves the performance of the prover.
• Abstract（参考訳）: Connection-tableau Proversは通常、検索をバックトラックすることでクローズドなテーブルローを構築する。 これにより、軽量な証明プロシージャが提供されるが、その低メモリの検索状態は、試行錯誤後に再利用される情報はほとんど残らない。 SATCoPは増分SATソルバに接地されたテーブルー節を保持することでこの問題に対処し、累積された接地節が命題的に満足できないものになると、証明者が問題を解消することを可能にする。 SATResetCoPは、非生産的なテーブルローをバックトラックせず、SATソルバのさらなる基底節を生成するために新しいものを開始することによって、この永続SAT状態に依存している。 TPTPでは、SATResetCoPはリーンCoPスタイルのベースラインを54%改善し、SATCoPスタイルのベースラインを18%改善しました。 派手なMPTP2078ベンチマークでは、616の問題を解決し、LeanCoPスタイルのベースラインを49%改善し、SATCoPスタイルのベースラインを12%改善しました。 これらの結果から,有用な接地節を蓄積するために表のガイダンスを変更することにより,証明者の性能が向上することが示唆された。

関連論文リスト

• CORE-T: COherent REtrieval of Tables for Text-to-SQL [91.76918495375384]
  CORE-Tはスケーラブルでトレーニング不要なフレームワークで、テーブルに目的のメタデータを付加し、軽量なテーブル互換キャッシュをプリコンプリートする。 バード、スパイダー、MMQAを越えて、CORE-Tはテーブル選択F1を最大22.7ポイント改善し、最大42%のテーブルを検索する。
  論文  参考訳（メタデータ） (2026-01-19T14:51:23Z)
• ExCoT: Optimizing Reasoning for Text-to-SQL with Execution Feedback [49.21833666405111]
  大規模言語モデル(LLM)は、多くの推論タスクにおいて優れているが、Chain-of-Thought(CoT)推論を活用する能力はいまだに未定である。 我々は,オープンソース LLM を反復的に最適化する新しいフレームワークである ExCoT を提案する。
  論文  参考訳（メタデータ） (2025-03-25T18:17:36Z)
• RSL-SQL: Robust Schema Linking in Text-to-SQL Generation [51.00761167842468]
  本稿では、双方向スキーマリンク、コンテキスト情報拡張、バイナリ選択戦略、マルチターン自己補正を組み合わせたRSLと呼ばれる新しいフレームワークを提案する。 ベンチマークの結果,オープンソースのソリューション間でのSOTA実行精度は67.2%,BIRDは87.9%,GPT-4オクルージョンは87.9%であった。 提案手法は,DeepSeekを同一のプロンプトで適用した場合,GPT-4ベースのテキスト・ツー・シークシステムよりも優れている。
  論文  参考訳（メタデータ） (2024-10-31T16:22:26Z)
• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。 これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。 私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
  論文  参考訳（メタデータ） (2024-10-18T22:25:54Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  分解硬度(d硬度)の概念を導入する。 d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
  論文  参考訳（メタデータ） (2023-12-16T12:44:36Z)
• Explaining SAT Solving Using Causal Reasoning [30.469229388827443]
  本稿では、因果推論を用いて、現代のSATソルバの機能に関する洞察を得るCausalSATを紹介する。 われわれはCausalSATを用いて,これまで「親指のルール」や経験的発見と考えられていた仮説を定量的に検証した。
  論文  参考訳（メタデータ） (2023-06-09T22:53:16Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。 そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
  論文  参考訳（メタデータ） (2022-10-04T09:19:13Z)
• A Neural Network-based SAT-Resilient Obfuscation Towards Enhanced Logic Locking [3.076761061950216]
  本稿では,ニューラルネットワークを用いた unSAT 節変換器 SATConda を提案する。 SATCondaは最小限の領域と電力オーバーヘッドを発生させ、元の機能を不必要なセキュリティで保存する。 SATCondaをISCAS85およびISCAS89ベンチマークで評価した。
  論文  参考訳（メタデータ） (2022-09-13T07:59:27Z)
• SATformer: Transformer-Based UNSAT Core Learning [0.0]
  本稿では,SAT 問題に対する Transformer ベースのアプローチである SATformer を紹介する。 SATformerは、問題を直接解決するのではなく、満足できないことに焦点をあてて、その問題を反対方向からアプローチする。 SATformerは、シングルビットの満足度結果と最小限の不満コアを使用して、マルチタスク学習アプローチでトレーニングされる。 実験の結果,SATformerは既存のソルバのランタイムを平均21.33%削減できることがわかった。
  論文  参考訳（メタデータ） (2022-09-02T11:17:39Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)

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

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