論文の概要: LLM-based Satisfiability Checking of String Requirements by Consistent Data and Checker Generation

• arxiv url: http://arxiv.org/abs/2506.16639v1
• Date: Thu, 19 Jun 2025 22:41:43 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-23 19:00:05.279227
• Title: LLM-based Satisfiability Checking of String Requirements by Consistent Data and Checker Generation
• Title（参考訳）: 一貫性データとチェッカ生成による文字列要求のLCMによる満足度チェック
• Authors: Boqi Chen, Aren A. Babikian, Shuzhao Feng, Dániel Varró, Gunter Mussbacher,
• Abstract要約: 大規模言語モデル(LLM)は、形式的推論タスクの代替手法として登場した。 本稿では,文字列上のNL要求の満足度を検証するハイブリッドアプローチを提案する。 LLMは、Pythonベースのチェッカーの完全なテスト精度さえ達成して、自然言語をチェッカーに効果的に翻訳する。
• 参考スコア（独自算出の注目度）: 2.892899073587433
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Requirements over strings, commonly represented using natural language (NL), are particularly relevant for software systems due to their heavy reliance on string data manipulation. While individual requirements can usually be analyzed manually, verifying properties (e.g., satisfiability) over sets of NL requirements is particularly challenging. Formal approaches (e.g., SMT solvers) may efficiently verify such properties, but are known to have theoretical limitations. Additionally, the translation of NL requirements into formal constraints typically requires significant manual effort. Recently, large language models (LLMs) have emerged as an alternative approach for formal reasoning tasks, but their effectiveness in verifying requirements over strings is less studied. In this paper, we introduce a hybrid approach that verifies the satisfiability of NL requirements over strings by using LLMs (1) to derive a satisfiability outcome (and a consistent string, if possible), and (2) to generate declarative (i.e., SMT) and imperative (i.e., Python) checkers, used to validate the correctness of (1). In our experiments, we assess the performance of four LLMs. Results show that LLMs effectively translate natural language into checkers, even achieving perfect testing accuracy for Python-based checkers. These checkers substantially help LLMs in generating a consistent string and accurately identifying unsatisfiable requirements, leading to more than doubled generation success rate and F1-score in certain cases compared to baselines without generated checkers.
• Abstract（参考訳）: 自然言語(NL)を用いて表現される文字列上の要求は、文字列データ操作に大きく依存しているため、特にソフトウェアシステムに関係している。 通常、個々の要求は手動で分析できるが、NL要求の集合に対する特性(例えば、満足度)の検証は特に困難である。 形式的アプローチ(例えば、SMTソルバ)は、そのような性質を効率的に検証することができるが、理論上の制限があることが知られている。 さらに、NL要求を形式的な制約に翻訳するには、通常、かなりの手作業が必要となる。 近年, 大規模言語モデル (LLM) が形式的推論タスクの代替手法として登場しているが, 文字列による要求検証の有効性は低い。 本稿では, LLMs (1) を用いて文字列に対する NL 要求の満足度を検証し, 満足度を導出する(可能であれば一貫した文字列)と, (2) 宣言型 (SMT) と命令型 (Python) チェッカーを生成し,(1) の正しさを検証するハイブリッド手法を提案する。 実験では,4つのLLMの性能評価を行った。 その結果、LLMは、Pythonベースのチェッカーの完全なテスト精度さえ達成して、自然言語をチェッカーに効果的に翻訳することを示した。 これらのチェッカーはLLMが一貫性のある文字列を生成し、満足できない要求を正確に識別するのに役立ち、生成されたチェッカーを持たないベースラインと比較して、特定のケースでは2倍以上の成功率とF1スコアとなる。

関連論文リスト

• RELIC: Evaluating Compositional Instruction Following via Language Recognition [37.49115450182637]
  大規模言語モデル(LLM)は、コンテキストで提供されるタスクの仕様に基づいてのみタスクを実行することがますます期待されている。 本稿では,言語認識を用いたインコンテキスト認識(RELIC)フレームワークについて紹介する。
  論文  参考訳（メタデータ） (2025-06-05T16:17:24Z)
• Self-Steering Language Models [113.96916935955842]
  DisCIPLは、"セルフステアリング(self-steering)"言語モデルのメソッドである。 DisCIPLはPlannerモデルを使用してタスク固有の推論プログラムを生成する。 我々の研究は、高度に並列化されたモンテカルロ推論戦略の設計空間を開く。
  論文  参考訳（メタデータ） (2025-04-09T17:54:22Z)
• $\texttt{SEM-CTRL}$: Semantically Controlled Decoding [53.86639808659575]
  $texttSEM-CTRL$は、LLMデコーダに直接、リッチなコンテキスト依存制約とタスクおよびインスタンス固有のセマンティクスを強制する統一的なアプローチである。 texttSEM-CTRL$は、小さな訓練済みのLLMがより大きな変種や最先端の推論モデルよりも効率的に性能を向上することを可能にする。
  論文  参考訳（メタデータ） (2025-03-03T18:33:46Z)
• Aligning Language Models to Explicitly Handle Ambiguity [22.078095273053506]
  我々は,あいまいなクエリを扱うために,言語モデルを整列する新しいパイプラインであるAlignment with Perceived Ambiguity (APA)を提案する。 質問応答データセットの実験結果から、APAはLLMに対して、あいまいなクエリを明示的に検出し、管理する権限を持つことが示された。 我々の発見は、APAがゴールドスタンダードラベルのトレーニング、特にアウト・オブ・ディストリビューションのシナリオで優れていることを証明している。
  論文  参考訳（メタデータ） (2024-04-18T07:59:53Z)
• Log Probabilities Are a Reliable Estimate of Semantic Plausibility in Base and Instruction-Tuned Language Models [50.15455336684986]
  意味的妥当性を評価するため,LogProbsの有効性と基本的なプロンプトを評価した。 LogProbsは、直接ゼロショットプロンプトよりも、より信頼性の高いセマンティックな妥当性を提供する。 我々は,プロンプトベースの評価の時代においても,LogProbsは意味的妥当性の有用な指標である,と結論付けた。
  論文  参考訳（メタデータ） (2024-03-21T22:08:44Z)
• Learning to Check: Unleashing Potentials for Self-Correction in Large Language Models [5.463333911506443]
  我々は,タスクチェックのためのトレーニングデータを構築することで,大規模言語モデル(LLM)の自己チェック能力を向上させることを目指している。 ステップCoTチェック(Step CoT Check)と呼ばれる特殊なチェックフォーマットを提案する。 実験により、"Step CoT Check"フォーマットによる微調整により、LCMの自己チェックと自己補正能力が大幅に向上することが示された。
  論文  参考訳（メタデータ） (2024-02-20T14:23:23Z)
• Grammar-Constrained Decoding for Structured NLP Tasks without Finetuning [27.59524153097858]
  文法制約付き復号法(GCD)は、大言語モデル(LM)の生成を制御するために用いられる。 GCDは一般に構造化NLPタスクの統一フレームワークとして機能する。 文法制約付きLMは、制約なしLMよりも大幅に優れるか、タスク固有の微調整モデルよりも優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-23T11:54:37Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)
• Large Language Models are Better Reasoners with Self-Verification [48.534270563880845]
  大規模言語モデル(LLM)は、いくつかの自然言語処理タスクにおいて強力な推論能力を示している。 思考の連鎖(CoT)を促進させるLLMは、個別のミスに非常に敏感な、多段階のプロンプトと多段階の予測を必要とする。 また,LLMにも同様な自己検証能力があることを示す。
  論文  参考訳（メタデータ） (2022-12-19T15:51:52Z)

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

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