論文の概要: Eliciting Specifications: When Does Interactive Clarification Help?
- arxiv url: http://arxiv.org/abs/2610.22382v1
- Date: Mon, 05 Oct 2026 16:49:27 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-26 00:37:12.120637
- Title: Eliciting Specifications: When Does Interactive Clarification Help?
- Title（参考訳）: 仕様の緩和: インタラクティブな明確化はいつ役に立つのか?
- Abstract要約: 提案手法は, 検証済みのリーン仕様を形式化する前に, リファレンスグラウンドのシミュレーション開発者から明確化を求めることにより, EAが検証済みのリーン仕様を改善できるかどうかを検討する。
エージェントはタスクを分解し、未解決の判断を特定し、有界な明確化の質問を行い、回答を使って洗練された自然言語仕様を書く。
- 参考スコア（独自算出の注目度）: 1.7376812477996522
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: LLMs can generate Lean specifications from task descriptions, but those descriptions are often underspecified or ambiguous and may omit verifier-relevant edge cases, yielding imperfect formal specifications. We study whether an elicitation agent (EA) can improve verifier-checked Lean specifications by seeking clarification from a reference-grounded simulated developer before formalization. The agent decomposes the task, identifies unresolved decisions, asks bounded clarification questions, and uses the answers to write a refined natural-language specification that an LLM formalizer then translates into Lean. On 189 Verina Lean 4 specification-generation tasks, we compare single-shot generation with elicitation under question budgets of k=3 and k=10, allowing at most three or ten EA questions per task, across same-model and cross-model configurations. The same-model Claude Sonnet 4.6 pipeline has negative strict pass@1 estimates at both budgets, showing elicitation is not a uniform accuracy booster. In contrast, the Sonnet 4.6-to-GPT-5.6 and Sonnet 4.6-to-Gemini 3.8 Flash pipelines have positive strict estimates. The largest strict result reaches 65.6%, a +6.3-point change (+12 tasks), in the Sonnet 4.6-to-GPT-5.6 pipeline. Six of eight conditions have positive compile-conditional estimates, with a maximum cross-model difference of +4.9 points among compiling outputs. Treatment estimates also differ across the basic and advanced splits; the largest advanced-task change occurs in the Sonnet 4.6-to-GPT-5.6 configuration at k=10, from 42.0% to 50.6%. Failure analysis identifies postconditions as the largest source of degradation. These findings suggest future autoformalization systems should treat elicited natural-language specifications as intermediate artifacts and optimize jointly for semantic correctness among compiling outputs and reliable translation of clarified information into Lean.
- Abstract（参考訳）: LLMはタスク記述からリーン仕様を生成することができるが、これらの記述はしばしば不明確あるいは曖昧であり、検証に関連のあるエッジケースを省略し、不完全な形式仕様をもたらす可能性がある。
提案手法は, 検証済みのリーン仕様を形式化する前に, リファレンスグラウンドのシミュレーション開発者から明確化を求めることにより, EAが検証済みのリーン仕様を改善できるかどうかを検討する。
エージェントはタスクを分解し、未解決の意思決定を特定し、境界付けられた明確化の質問を行い、答えを使って、LLMフォーミュラがリーンに翻訳する洗練された自然言語仕様を書きます。
189 Verina Lean 4 の仕様生成タスクでは、単一ショット生成と k=3 と k=10 の質問予算による適用を比較します。
同じモデルであるClaude Sonnet 4.6のパイプラインは、両方の予算で負の厳格なpass@1推定値を持つ。
対照的に、Sonnet 4.6-to-GPT-5.6とSonnet 4.6-to-Gemini 3.8のフラッシュパイプラインは、正の厳しい推定値を持つ。
最大の厳密な結果は65.6%に達し、Sonnet 4.6-to-GPT-5.6パイプラインでは+6.3ポイントの変更(+12タスク)となった。
8つの条件のうち6つは正のコンパイル条件の推定値を持ち、コンパイル出力の最大交叉モデル差は+4.9点である。
治療の見積もりは基本的な分割と高度な分割で異なり、ソネット4.6-to-GPT-5.6では42.0%から50.6%と最も大きく変化している。
障害解析は、ポストコンディションを最大の劣化源と特定する。
これらの結果から,今後の自動書式化システムでは,提案した自然言語仕様を中間成果物として扱い,コンパイル出力間の意味的正当性を共同で最適化し,情報からリーンへの信頼性の高い翻訳を行うことが示唆された。
関連論文リスト
- Repairing LLM-Generated Specifications with Deterministic Diagnosis [48.79311600023815]
大型言語モデル (LLM) はフォーミュラライザとしてますます使われている。
LLMは、シンボリック・ソルバが解決できる形式的な仕様を作成し、その仕様に対して保証する。
多くの仕様は実行可能であるが、意味的に間違っている。誤った制約、ドメイン、目的、述語、目標を符号化する。
DRAGOは、この未解決の批判を決定論的、フォーマリズム固有の診断に置き換える修復フレームワークである。
論文 参考訳（メタデータ） (2026-10-15T19:12:54Z) - Decomposing and Predicting Annotation Disagreement in Harmful Content Across Languages [48.69228180369574]
アノテーションの不一致は、主観的なタスクの有意義な性質として、ますます認識されている。
テキストの解釈可能な意味特性から不一致を予測することを提案する。
モデルとデータセット全体、デロゲーションに関する質問、コンテキストの欠如、決定境界が最強の予測要因として機能する。
論文 参考訳（メタデータ） (2026-10-13T15:49:44Z) - SpecRead: A Benchmark for Measuring Whether Language Models Understand Hardware Specifications [0.0]
生成能力から仕様理解を分離するベンチマークであるSpecReadを提案する。
Icarus Verilog シミュレーションが観測可能な振る舞いを変えるために示す突然変異のみを保持する。
SpecReadは、決定論的チェックによって自動的に修正可能で、グレーゾーンのケースは保守的なメインスコアで誤算される。
論文 参考訳（メタデータ） (2026-09-27T16:00:47Z) - An Empirical Evaluation of Cost-Efficient Large Language Models on Algorithmic Programming Tasks [0.0]
38.4%のメソッドは返却した値を計算せず、返却された回答の12.9%のみが正しい。
結果クラスの条件は、応答の信頼性と正しさが逆関係であることを示しているが、真の計算方法が最も多く答えられ、19.3%が正しかった。
論文 参考訳（メタデータ） (2026-09-16T02:55:03Z) - MemToC: Benchmarking Memory-Tool Conflict Resolution in Large Language Models [49.47300047353726]
MemToCは、実行時ツールによるポストツール-リターン仲裁のベンチマークである。
MemToCは、542の質制御された事実質問から構築された6,504回の評価エピソードで構成されている。
オープンウェイトな7-9Bモデルでは、ツールが強く支配的なクローズドブックの回答を返す。
論文 参考訳（メタデータ） (2026-08-26T18:22:03Z) - ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers [77.95933562142014]
ITPEvalは、4つの主要なIPP間で自動形式証明翻訳を評価するための最初のベンチマークである。
itpevalは、状態が分離されたウォームバックエンドを備えた、統合されたマルチITP認証インフラストラクチャです。
論文 参考訳（メタデータ） (2026-07-07T22:05:55Z) - Distributional Energy-Based Models for Uncertainty-Aware Structured LLM Reasoning [40.342912574072024]
大規模言語モデルは、旅行計画やコードソリューションのような構造化されたアウトプットを生成する。
個々の推論ステップは正しく見えるが、アウトプット全体が予算に違反したり、テストケースに失敗したり、あるいは以前の推論に矛盾することがある。
構造化LCM出力の検証のための決定論的解析制約付き学習品質スコアラを提案する。
論文 参考訳（メタデータ） (2026-05-15T17:08:27Z) - DiagnosticIQ: A Benchmark for LLM-Based Industrial Maintenance Action Recommendation from Symbolic Rules [4.124344125532972]
複雑な工業資産の監視は、センサーの条件に基づいて引き起こされるエンジニアによる象徴的な規則に依存している。
ルールをメンテナンスステップに変換するには、長年の実践を通じて得られた資産固有の知識が必要です。
このルール・ツー・アクション・ステップの意思決定支援としてLLMが有効か検討し,6,690名の専門家による複数選択質問をベンチマークした。
論文 参考訳（メタデータ） (2026-05-09T02:17:39Z) - ACAR: Adaptive Complexity Routing for Multi-Model Ensembles with Auditable Decision Traces [3.151184728006369]
本稿では,聴覚条件下でのマルチモデルオーケストレーションのための測定フレームワークACARを提案する。
ACARは、N=3プローブサンプルから計算した自己整合分散(sigma)を使用して、単一モデル、2モデル、3モデル実行モードでタスクをルーティングする。
我々は4つのベンチマークにまたがる1,510のタスクに対してACARを評価し、7,550以上の監査可能な実行を生成した。
論文 参考訳（メタデータ） (2026-02-06T23:27:17Z) - Faithful Chain-of-Thought Reasoning [51.21714389639417]
CoT(Chain-of-Thought)は言語モデル(LM)のパフォーマンスを様々な推論タスクで向上させる。
翻訳と問題解決という2つの段階を含む推論フレームワークであるFithful CoTを提案する。
このことは、推論連鎖が最終回答の忠実な説明を提供することを保証している。
論文 参考訳（メタデータ） (2023-01-31T03:04:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。