論文の概要: 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（参考訳）: 自然言語ソフトウェア要件のニューロシンボリック監査
- 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 ベースのクエリによる厳密なソフトウェア要求の監査を可能にすることを示す。
関連論文リスト
- CLAIM: Leading Open-domain Active Clarification of Large Language Models with Uncertainty Measurement [50.91045324738942]
CLAIMは、オープンドメイン環境でのアクティブな明確化学習のための不確実性駆動フレームワークである。
本研究では,不確実性推定とセマンティッククラスタリングと推論に基づく判断を統合したエントロピー駆動型合成データ生成パイプラインを提案する。
実験の結果,手動でラベル付けしたデータに頼ることなく,CLAIMが安定かつ一般化可能な明確化戦略を学習できることが確認された。
論文 参考訳（メタデータ） (2026-08-12T04:27:45Z) - SymboUQ: Symbolic Uncertainty Quantification for Spatial Reasoning in LLMs [5.676157325165344]
シンボル化可能性の識別により、推論トレースから最終回答信頼性を推定するシンボル的不確実性フレームワークであるSymboUQを紹介する。
その結果,SymboUQ は AUROC の約8% の相対的改善と,クラスバランスの強い Brier 損失の7% の相対的減少を達成できた。
論文 参考訳（メタデータ） (2026-08-01T03:36:09Z) - 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) - Efficient semantic uncertainty quantification in language models via diversity-steered sampling [46.23327887393273]
本稿では,デコード中に意味的に冗長な出力を回避できるダイバーシティステアリング・サンプリング手法を提案する。
主要なアイデアは、モデルの提案分布に連続的な意味-類似性ペナルティを注入することである。
モジュラーであり、ベースLSMへの勾配アクセスを必要としないため、このフレームワークは不確実性評価のためのドロップインエンハンスメントとして機能することを約束している。
論文 参考訳（メタデータ） (2025-10-24T10:06:21Z) - 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) - SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
パラメータ化マルチエージェントシステム(MAS)の検証について検討する。
特に、与えられた状態公式として特徴づけられる不要な状態が、所定のMASで到達可能かどうかについて検討する。
論文 参考訳（メタデータ） (2020-08-11T15:24:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。