論文の概要: Portus: Linking Alloy with SMT-based Finite Model Finding

• arxiv url: http://arxiv.org/abs/2411.15978v1
• Date: Sun, 24 Nov 2024 20:43:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-03 14:34:58.706345
• Title: Portus: Linking Alloy with SMT-based Finite Model Finding
• Title（参考訳）: Portus:Linking Alloy with SMT-based Finite Model Finding
• Authors: Ryan Dancy, Nancy A. Day, Owen Zila, Khadija Tariq, Joseph Poremba,
• Abstract要約: ポータス(Portus)は、合金を等価な多種一階論理問題(MSFOL)に変換する方法である。 Fortress は MSFOL の有限モデル探索問題を等式付き非解釈関数の論理に変換する(EUF)
• 参考スコア（独自算出の注目度）: 0.24466725954625887
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Alloy is a well-known, formal, declarative language for modelling systems early in the software development process. Currently, it uses the Kodkod library as a back-end for finite model finding. Kodkod translates the model to a SAT problem; however, this method can often handle only problems of fairly low-size sets and is inherently finite. We present Portus, a method for translating Alloy into an equivalent many-sorted first-order logic problem (MSFOL). Once in MSFOL, the problem can be evaluated by an SMT-based finite model finding method implemented in the Fortress library, creating an alternative back-end for the Alloy Analyzer. Fortress converts the MSFOL finite model finding problem into the logic of uninterpreted functions with equality (EUF), a decidable fragment of first-order logic that is well-supported in many SMT solvers. We compare the performance of Portus with Kodkod on a corpus of 49 expert Alloy models. Our method is fully integrated into the Alloy Analyzer.
• Abstract（参考訳）: Alloyはソフトウェア開発プロセスの初期にシステムをモデリングするための、よく知られた、形式的で宣言的な言語です。 現在は、有限モデル探索のバックエンドとしてKodkodライブラリを使用している。 コドコッドはモデルをSAT問題に変換するが、この方法は比較的小さな集合の問題のみを扱うことができ、本質的に有限である。 本稿では,合金を等価な多種一階述語論理問題(MSFOL)に変換する手法であるPortusを提案する。 MSFOLでは、この問題をFortressライブラリに実装されたSMTベースの有限モデル探索法で評価することができ、アロイ・アナライザーの代替バックエンドを作成することができる。 Fortress は MSFOL の有限モデル探索問題を、多くの SMT ソルバでよく支持されている一階述語論理の決定可能な断片である等式付き非解釈関数(EUF)の論理に変換する。 49種類の専門合金モデルを用いて,PortusとKodkodの性能を比較した。 本手法はアロイ・アナライザーに完全に統合されている。

関連論文リスト

• Syntactic and Semantic Control of Large Language Models via Sequential Monte Carlo [90.78001821963008]
  広い範囲のLMアプリケーションは、構文的制約や意味論的制約に適合するテキストを生成する必要がある。 我々は、連続モンテカルロ(SMC)に基づく制御LM生成のためのアーキテクチャを開発する。 我々のシステムはLew et al. (2023) のフレームワーク上に構築されており、言語モデル確率型プログラミング言語と統合されている。
  論文  参考訳（メタデータ） (2025-04-17T17:49:40Z)
• 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)
• Sample, Don't Search: Rethinking Test-Time Alignment for Language Models [55.2480439325792]
  新しいテストタイムアライメントアプローチであるQAlignを紹介します。 テスト時間計算をスケールする際、QAlignは各プロンプトの最適配向分布からのサンプリングに収束する。 マルコフ連鎖モンテカルロのテキスト生成における最近の進歩を取り入れることで、基礎となるモデルを変更したり、ロジットアクセスを必要とせずに、より良い整合出力を可能にする。
  論文  参考訳（メタデータ） (2025-04-04T00:41:40Z)
• Logic.py: Bridging the Gap between LLMs and Constraint Solvers [0.8192907805418583]
  本稿では,大規模言語モデルを用いた探索に基づく問題の定式化と解法について述べる。 論理パズルベンチマークZebraLogicBenchにおいて,本手法の有効性を示す。
  論文  参考訳（メタデータ） (2025-02-17T00:36:54Z)
• Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
  不確実性定量化(英: Uncertainty Quantification、UQ)は、機械学習(ML)アプリケーションにおいて重要なコンポーネントである。 最新のUQベースラインの集合を実装した新しいベンチマークを導入する。 我々は、9つのタスクにわたるUQと正規化技術に関する大規模な実証的研究を行い、最も有望なアプローチを特定した。
  論文  参考訳（メタデータ） (2024-06-21T20:06:31Z)
• Set-Based Prompting: Provably Solving the Language Model Order Dependency Problem [18.020492646988746]
  本稿では,LLMの出力が指定されたサブシーケンスのセットに順序依存しないことを保証する手法であるSet-Based Promptingを提案する。 我々の入力が分布外であるにもかかわらず、期待される精度への影響は小さく、予測は、一様に選択された応答のシャッフルの順序を超える。
  論文  参考訳（メタデータ） (2024-06-04T16:09:13Z)
• Adversarial Schrödinger Bridge Matching [66.39774923893103]
  反復マルコフフィッティング(IMF)手順は、マルコフ過程の相互射影と相互射影を交互に交互に行う。 本稿では、プロセスの学習を離散時間でほんの少しの遷移確率の学習に置き換える新しい離散時間IMF(D-IMF)手順を提案する。 D-IMFの手続きは、数百ではなく数世代のステップで、IMFと同じ品質の未完成のドメイン翻訳を提供できることを示す。
  論文  参考訳（メタデータ） (2024-05-23T11:29:33Z)
• Small Language Models Fine-tuned to Coordinate Larger Language Models improve Complex Reasoning [41.03267013352519]
  大きな言語モデル(LLM)は、印象的な推論能力を示すチェーン・オブ・シントを生成するように促された。 本稿では、分解生成器を用いて複雑な問題をより少ない推論ステップを必要とするサブプロブレムに分解するDaSLaMを紹介する。 本稿では,DaSLaMがスケール関数としての解の能力に制限されないことを示す。
  論文  参考訳（メタデータ） (2023-10-21T15:23:20Z)
• An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes [4.393684402895834]
  Algebraic Data Types (ADT) は関数型プログラミング言語で古典的に見られる構造である。 我々は,基本的に異なるアプローチ,エフェーガーアプローチを採るSMTソルバを提案する。
  論文  参考訳（メタデータ） (2023-10-18T18:14:18Z)
• Sorted LLaMA: Unlocking the Potential of Intermediate Layers of Large Language Models for Dynamic Inference [32.62084449979531]
  SortedNet を Sorted Fine-Tuning (SoFT) に置き換えることで生成 NLP タスクに拡張する。 我々のアプローチはモデル効率を向上し、推論中に様々なシナリオに対する複数のモデルの必要性を排除します。 以上の結果から,SFT+ICT(Early-Exit)と標準ファインチューニング(SFT+ICT)と比較して,サブモデルの優れた性能を示す。
  論文  参考訳（メタデータ） (2023-09-16T11:58:34Z)
• Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
  一般に、fMTは、任意の決定可能な一階述語理論(例えば、線形算術)に対して、テーブルーベースの半決定手順で半決定可能であることが示されている。 有限メモリと呼ぶ抽象的意味条件を満たす任意のfMT式に対して、新しい規則で拡張されたテーブルーもまた終了することが保証されていることを示す。
  論文  参考訳（メタデータ） (2023-07-31T17:02:23Z)
• Interpretability at Scale: Identifying Causal Mechanisms in Alpaca [62.65877150123775]
  本研究では、Boundless DASを用いて、命令に従う間、大規模言語モデルにおける解釈可能な因果構造を効率的に探索する。 私たちの発見は、成長し、最も広くデプロイされている言語モデルの内部構造を忠実に理解するための第一歩です。
  論文  参考訳（メタデータ） (2023-05-15T17:15:40Z)
• A Template-based Method for Constrained Neural Machine Translation [100.02590022551718]
  本稿では,デコード速度を維持しつつ,高い翻訳品質と精度で結果が得られるテンプレートベースの手法を提案する。 テンプレートの生成と導出は、1つのシーケンスからシーケンスまでのトレーニングフレームワークを通じて学習することができる。 実験結果から,提案手法は語彙的,構造的に制約された翻訳タスクにおいて,いくつかの代表的ベースラインを上回り得ることが示された。
  論文  参考訳（メタデータ） (2022-05-23T12:24:34Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)

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

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