論文の概要: Neurosymbolic Auditing of Natural-Language Software Requirements

• arxiv url: http://arxiv.org/abs/2605.13817v1
• Date: Wed, 13 May 2026 17:43:13 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-14 23:30:28.213628
• Title: Neurosymbolic Auditing of Natural-Language Software Requirements
• Title（参考訳）: 自然言語ソフトウェア要件のニューロシンボリック監査
• Authors: Bethel Hall, William Eiers,
• Abstract要約: 本稿では,このアイデアを医療デバイスソフトウェア要求に対して運用するニューロシンボリックパイプラインであるVERIMEDを提案する。 VERIMED における LLM に基づくアプローチは曖昧さに敏感な要求を低減できることを示す。
• 参考スコア（独自算出の注目度）: 0.30079490585515345
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Natural-language software requirements are often ambiguous, inconsistent, and underspecified; in safety-critical domains, these defects propagate into formal models that verify the wrong specification and into implementations that ship unsafe behavior. We show that large language models, equipped with an SMT solver, can audit such requirements: translating them into formal logic, detecting ambiguity through stochastic variation in the generated formalization, and exposing inconsistency, vacuousness, and safety violations through solver queries on the resulting specification. We present VERIMED, a neurosymbolic pipeline that operationalizes this idea for medical-device software requirements, and report two findings. First, stochastic variation across independent formalizations is a signal of ambiguity: requirements that admit multiple plausible interpretations produce SMT-inequivalent formalizations, and bidirectional SMT equivalence checking turns this disagreement into a solver-checkable test. Second, the usefulness of symbolic feedback depends on its granularity: in counterexample-guided repair on a hemodialysis question-answering benchmark, concrete SMT counterexamples raise verified accuracy from 55.4% to 98.5%. Over an extensive experimental evaluation on open-source hemodialysis safety requirements, we show that the LLM-based approach in VERIMED successfully reduces ambiguity-sensitive requirements and enables rigorous auditing of software requirements through SMT-based queries.
• Abstract（参考訳）: 安全クリティカルなドメインでは、これらの欠陥は間違った仕様を検証した形式モデルに伝播し、安全でない振る舞いを出荷する実装へと伝播します。 SMTソルバを備えた大規模言語モデルは,形式論理への変換,生成した形式化の確率的変動によるあいまいさの検出,不整合性,空白性,安全性違反などの要件を,解決者クエリによる仕様書の公開などにより監査可能であることを示す。 本稿では,このアイデアを医療デバイスソフトウェア要求に対して運用するニューロシンボリックパイプラインであるVERIMEDを紹介し,その2つの知見を報告する。 まず、独立な形式化の確率的変動は曖昧さの信号である: 複数の可算解釈を許容する要件はSMT等価な形式化を生成し、双方向のSMT同値チェックは、この不一致をソルバチェック可能なテストに変換する。 第2に、シンボリックフィードバックの有用性は、その粒度に依存する:血液透析質問回答ベンチマークの逆例誘導修復において、具体的なSMT反例は55.4%から98.5%に精度を高めている。 オープンソースの血液透析の安全性要件に関する広範な実験的評価において,VERIMED における LLM ベースのアプローチはあいまいさに敏感な要求を減らし,SMT ベースのクエリによる厳密なソフトウェア要求の監査を可能にすることを示す。

関連論文リスト

• A Multimodal Dataset for Visually Grounded Ambiguity in Machine Translation [53.06004926782424]
  VIDA(Visually-Dependent Ambiguity)は2500の慎重にキュレートされたインスタンスのデータセットで、注釈付きソーススパンの解決には視覚的証拠が必要である。 また,LLM-as-a-judge分類器を用いて,アノテートされた曖昧な表現がスパンレベルで正しく解決されているかどうかを検証する。
  論文  参考訳（メタデータ） (2026-05-03T19:55:06Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• Beyond Prompt: Fine-grained Simulation of Cognitively Impaired Standardized Patients via Stochastic Steering [58.85421622061983]
  認知障害患者の微粒化シミュレーションのためのStsPatientを提案する。 対照的な命令と応答のペアからステアリングベクトルを抽出することにより、ドメイン固有の特徴を捉える。 StsPatientは、臨床の信頼性と重症度の両方において、ベースラインを著しく上回る。
  論文  参考訳（メタデータ） (2026-04-14T02:37:46Z)
• X-RAY: Mapping LLM Reasoning Capability via Formalized and Calibrated Probes [11.988348978958376]
  大規模言語モデル(LLM)は有望な性能を達成するが、その推論能力はいまだによく分かっていない。 我々は、校正された正式に検証されたプローブを用いてLCM推論能力をマッピングする説明可能な推論分析システムであるX線について述べる。 数学,物理学,化学の分野において,中等レベルから高度な問題に対する現状のLSMの評価を行った。
  論文  参考訳（メタデータ） (2026-03-05T15:34:22Z)
• Evaluating Robustness of Reasoning Models on Parameterized Logical Problems [20.78623024814435]
  LogicはLSMベースの推論を評価するための制御されたテストベッドを提供する。 SATスタイルの標準ベンチマークでは、表面の難易度(長さ、単語、節順)を実際に満足度を決定する構造現象と区別することが多い。 構造化2-CNF式をパラメータ化して構築した2-SATの診断ベンチマークを提案する。
  論文  参考訳（メタデータ） (2026-02-13T06:54:25Z)
• FactTest: Factuality Testing in Large Language Models with Finite-Sample and Distribution-Free Guarantees [41.78390564658645]
  幻覚や非現実的コンテンツを生成するための大規模言語モデル(LLM)は、高い領域での信頼性を損なう。 FactTest は LLM が与えられた質問に対する正しい回答を確実に提供できるかどうかを統計的に評価する新しいフレームワークである。 本研究では,FactTestが幻覚を効果的に検出し,未知の疑問に答えることを禁じるモデルの能力を向上させることにより,40%以上の精度向上を実現していることを示す。
  論文  参考訳（メタデータ） (2024-11-04T20:53:04Z)
• Decomposing Uncertainty for Large Language Models through Input Clarification Ensembling [69.83976050879318]
  大規模言語モデル(LLM)では、不確実性の原因を特定することが、信頼性、信頼性、解釈可能性を改善するための重要なステップである。 本稿では,LLMのための不確実性分解フレームワークについて述べる。 提案手法は,入力に対する一連の明確化を生成し,それらをLLMに入力し,対応する予測をアンサンブルする。
  論文  参考訳（メタデータ） (2023-11-15T05:58:35Z)

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

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