論文の概要: Detecting Inconsistencies in Model Specifications with LLM-as-Verifier Reasoning
- arxiv url: http://arxiv.org/abs/2610.01847v1
- Date: Thu, 01 Oct 2026 15:13:31 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-03 01:19:24.219161
- Title: Detecting Inconsistencies in Model Specifications with LLM-as-Verifier Reasoning
- Title（参考訳）: LLM-as-Verifier Reasoningによるモデル仕様の不整合検出
- Abstract要約: VeriSpecは、仕様テキスト自体を監査することで、モデル仕様の不整合を直接検出する最初のアプローチである。
我々の重要な洞察は、LLMを検証子として使用しながら、自然言語で仕様を維持することである。
VeriSpecをOpenAI Model Specに適用し、405のルールを抽出し、5つの矛盾を手作業で検証します。
- 参考スコア（独自算出の注目度）: 5.040391802660918
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Model specifications define how large language models (LLMs) should behave, guiding alignment training, inference-time behavior, and evaluation. Yet these specifications may themselves contain defects: two individually reasonable principles may prescribe incompatible behavior when applied to the same situation, leaving no response that satisfies both. Detecting such inconsistencies is challenging. Formalizing natural-language specifications risks losing subtle distinctions, while behavior-based testing cannot reliably distinguish specification defects from differences in model behavior. We introduce VeriSpec, the first approach to directly detect inconsistencies in model specifications by auditing the specification text itself. Our key insight is to preserve the specification in natural language while using an LLM as a verifier. VeriSpec extracts structured, context-aware rules, constructs a topic-guided graph to cluster behaviorally related rules at the same authority level, and applies LLM-as-verifier reasoning to detect inconsistencies. Applying VeriSpec to the OpenAI Model Spec, we extract 405 rules and manually validate five inconsistencies, all reported to its developers, who responded positively and have initiated internal discussions. Compared with five baselines, VeriSpec identifies the most validated inconsistencies, achieves the highest precision (38.5%), and incurs the lowest cost per validated inconsistency ($11.12). These results establish direct specification auditing as a practical complement to behavioral alignment evaluation, catching defects at the source before they shape any model. The code is available at https://github.com/HIPREL-Group/VeriSpec.
- Abstract（参考訳）: モデル仕様は、大規模言語モデル(LLM)がどのように振る舞うかを定義し、アライメントトレーニング、推論時の振る舞い、評価を導く。
個々に合理的な2つの原則は、同じ状況に適用した場合に互換性のない振る舞いを規定し、両方を満たす反応は残らない。
そのような矛盾を検出することは難しい。
自然言語仕様の形式化は、微妙な区別を失うリスクを冒す一方、振る舞いベースのテストは、仕様欠陥とモデルの振る舞いの違いを確実に区別することはできない。
VeriSpecは、仕様テキスト自体を監査することで、モデル仕様の不整合を直接検出する最初のアプローチである。
我々の重要な洞察は、LLMを検証子として使用しながら、自然言語で仕様を維持することである。
VeriSpecは構造化されたコンテキスト対応のルールを抽出し、同じ権限レベルで行動関連ルールをクラスタ化するためのトピック誘導グラフを構築し、不整合を検出するためにLLM-as-verifier reasoningを適用する。
VeriSpecをOpenAI Model Specに適用し、405のルールを抽出し、5つの矛盾を手作業で検証します。
5つの基準線と比較して、VeriSpecは最も検証された不整合を識別し、最も高い精度(38.5%)を達成し、検証された不整合当たりの最低コスト(11.12ドル)を発生させる。
これらの結果は、行動アライメント評価の実践的な補完として直接仕様監査を確立し、モデルを形成する前にソースの欠陥を捕捉する。
コードはhttps://github.com/HIPREL-Group/VeriSpecで入手できる。
関連論文リスト
- Can Formal Specifications Be Synthesized from Tests Alone? [6.705404088685053]
提案手法では,テストコードと動的実行トレースのみから候補仕様を推測するためにLLMを用いる。
候補仕様は有界モデルチェックを用いて局所的に検証され、フィードバックは反復的改善を導く。
SpecGenBenchベンチマークの最初の結果は、テストがLLMを意味のあるJavaモデリング言語仕様へと導くことができることを示唆している。
論文 参考訳（メタデータ） (2026-08-13T13:44:54Z) - BeSpec: Behavior-Level Specification Alignment for Code Generation [2.9611475619490633]
本稿では,行動モデルに基づく仕様アライメントアプローチであるBeSpecについて述べる。
BeSpecはタスク記述を、正しいプログラムの意図した振る舞いに関する部分的な証拠として扱う。
候補プログラムを生成し、プローブ入力で実行し、観測された振る舞いと予測された振る舞いを比較する。
論文 参考訳（メタデータ） (2026-07-03T04:48:45Z) - SpecAlign: Efficient Specification-Grounded Alignment of Large Language Models via Synthetic Data [46.83043333985018]
我々は、プロバイダが承認したモデル仕様を主アライメントターゲットとして扱う新しいアライメントパラダイムである仕様基底アライメントを提案する。
仕様文書から直接アライメントデータを合成するフレームワークであるSpecAlignを紹介する。
論文 参考訳（メタデータ） (2026-06-15T06:30:52Z) - Logic-Regularized Verifier Elicits Reasoning from LLMs [63.65875399266337]
論理規則で正規化された教師なしの検証器であるLOVERを提案する。
ローバーは、定理を二項潜在変数として扱い、内部の活性化を活用し、3つの論理的制約を課す。
ローバーは教師なしのベースラインを大幅に上回る。
論文 参考訳（メタデータ） (2026-05-07T09:03:49Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
SPECAは、明示的で分類されたセキュリティプロパティを自然言語仕様から導き出し、実装間で再利用する監査フレームワークである。
RepoAuditのベンチマークでは、SPECAは100%リコール(F1=0.94)で88.9%の精度に達し、著者が検証した12のバグを地上の真実を超えて表面化している。
Sherlock Fusaka Audit Contest(10のターゲット、366の応募)では、SPECAが専門家が強化した15の脆弱性をすべて回復し、4つの修正確認バグが浮上した。
論文 参考訳（メタデータ） (2026-04-29T09:57:07Z) - Defective Task Descriptions in LLM-Based Code Generation: Detection and Analysis [21.26459132144385]
大規模な言語モデルはコード生成に広く使われているが、タスク記述が十分に詳細で十分に表現されているという暗黙の仮定に依存している。
実際には、ユーザーは欠陥のある記述を提供し、それがコードの正確性に強い影響を与える可能性がある。
我々はパラメータ効率の良い小型モデルに基づく軽量分類器SpecValidatorを開発した。
論文 参考訳（メタデータ） (2026-04-27T17:07:08Z) - Validating Formal Specifications with LLM-generated Test Cases [1.2031796234206136]
本稿では,事前学習された大規模言語モデル(LLM)を用いて,自然言語要求からテストケースを生成する実験結果について報告する。
評価は最先端の GPT-5 モデルに焦点をあてるが,他のクローズドおよびオープンソース LLM の結果も報告する。
論文 参考訳（メタデータ） (2025-10-27T14:02:20Z) - CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。
数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。
我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
論文 参考訳（メタデータ） (2025-08-05T17:55:24Z) - Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。
AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
論文 参考訳（メタデータ） (2021-09-25T22:53:24Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。