論文の概要: Repairing LLM-Generated Specifications with Deterministic Diagnosis
- arxiv url: http://arxiv.org/abs/2610.22568v1
- Date: Thu, 15 Oct 2026 19:12:54 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-20 00:56:07.637715
- Title: Repairing LLM-Generated Specifications with Deterministic Diagnosis
- Title（参考訳）: 確定診断によるLCM生成仕様の修復
- Abstract要約: 大型言語モデル (LLM) はフォーミュラライザとしてますます使われている。
LLMは、シンボリック・ソルバが解決できる形式的な仕様を作成し、その仕様に対して保証する。
多くの仕様は実行可能であるが、意味的に間違っている。誤った制約、ドメイン、目的、述語、目標を符号化する。
DRAGOは、この未解決の批判を決定論的、フォーマリズム固有の診断に置き換える修復フレームワークである。
- 参考スコア（独自算出の注目度）: 48.79311600023815
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Large language models (LLMs) are increasingly used as formalizers: given a reasoning problem expressed in natural language, they produce a formal specification that a symbolic solver can then solve, with guarantees relative to that specification. Many specifications are runnable yet semantically wrong, encoding incorrect constraints, domains, objectives, predicates, or goals, and solver-error feedback dries up once execution succeeds. Purely LLM-based diagnosis, lacking a formal ground truth, often fails to spot these errors, and its ungrounded critiques cause regressions in 11.8% of initially correct specifications in our experiments. We propose DRAGO, a repair framework that replaces this ungrounded critique with deterministic, formalism-specific diagnosis, and retains a rewrite only when the diagnosed error weight strictly decreases under a reference-free acceptance predicate. Across five benchmarks spanning logical reasoning (SMT-LIB2), constraint programming (MiniZinc), and planning (PDDL), DRAGO cuts regressions by nearly an order of magnitude, to 1.3%, while improving answer accuracy by 12.9 percentage points over zero-shot formalization and 8.7 percentage points over LLM-diagnostic repair, averaged across benchmarks. We also uncover two rendering defects in Planetarium that cause 50% (3,086 instances) of its floor-tile split to be inconsistent with the reference formalizations, and release a corrected split.
- Abstract（参考訳）: 言語モデル (LLM) は、自然言語で表現される推論問題を前提として、シンボルソルバが解決できる形式仕様を作成し、その仕様と関連性を保証する。
多くの仕様は実行可能であるが、意味的に間違っている。誤った制約、ドメイン、目的、述語、目標をコードする。
正式な根拠を欠いたLSMベースの診断は、しばしばこれらの誤りを発見できず、その根拠のない批判は、実験で最初に正しい仕様の11.8%に回帰を引き起こす。
DRAGOは、この未解決の批判を決定論的、形式論的診断に置き換える修復フレームワークであり、診断された誤り重みが基準のない受容述語の下で厳密に減少する場合にのみ書き換えを保持する。
論理的推論(SMT-LIB2)、制約プログラミング(MiniZinc)、計画(PDDL)にまたがる5つのベンチマークにおいて、DRAGOは回帰を桁違いに1.3%削減し、ゼロショットの形式化よりも12.9ポイント、LLMの診断的修復よりも8.7ポイント改善した。
また、プラネタリウムの2つのレンダリング欠陥を発見し、フロアタイルのスプリットの50% (3,086 インスタンス) が基準形式と矛盾していることを発見し、修正されたスプリットを放出した。
関連論文リスト
- NovGauge: A Fine-Grained Benchmark for Diagnosing LLMs' Capability in Paper Novelty Assessment [54.4265627247104]
大規模言語モデル(LLM)は、主要なAIカンファレンスでピアレビューでますます使用されている。
既存のベンチマークでは、ノベルティを1つの総合的なスコアとして評価している。
本報告では,詳細なノベルティアセスメント診断のための人手によるベンチマークであるNovGaugeについて述べる。
論文 参考訳（メタデータ） (2026-09-10T08:34:56Z) - IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
研究のアイデアは、新しく、一貫性があり、科学的に妥当であるが、その提案された手法は、忠実な実装のために不十分に指定されている。
提案手法は,実装を対象とする研究手法仕様の体系化の可否を,有能な実装者やコーディングエージェントに十分な方法論的情報を提供して,前提条件を満たさずに目的とする手法を構築することができるかを検討する。
IdeaAMBIGは660のエビデンス基底インスタンスのベンチマークで、レポートとGitHubの問題から163の現実世界のギャップと、コーディフィケーション対応のリファレンスに注入される合成ギャップを497のコントロールで管理する。
論文 参考訳（メタデータ） (2026-09-09T17:59:04Z) - Wrong Prediction, Right Answer: Recovering Evidence from Collapsed LLM Sequence Scores [31.709549159768727]
多様な推論ベンチマーク間で一貫した読み出しギャップを観察する。
隠れ状態プローブは、ネイティブシークエンススコアが完全に崩壊しても正解を復号することに成功した。
以上の結果から,無作為な内部論理を隠蔽する表現障害が明らかにゼロショット推論の欠点であることが明らかとなった。
論文 参考訳（メタデータ） (2026-08-31T16:43:55Z) - A Constrained Natural-Language Interface for Variational Multi-Physics Finite Element Simulations in FEniCS [0.0]
本稿では,LLMをフロントエンドタスクに限定した制約付き自然言語生成有限要素解析を提案する。
FEniCSソルバテンプレートを書いたり、弱い形式を導いたり、数値ソルバコアを書いたりすることはない。
エンド・ツー・エンドのデモンストレーションとして、システムは1つの自然言語プロンプトからフィレットとボルトホールを備えた3次元弾塑性Lブラケットを生成し、分析する。
論文 参考訳（メタデータ） (2026-06-09T14:38:11Z) - LinAlg-Bench: A Forensic Benchmark Revealing Structural Failure Modes in LLM Mathematical Reasoning [0.0]
LinAlg-Benchは、構造化線形代数計算における10のフロンティア大言語モデルを評価する診断ベンチマークである。
ベンチマークは、6600モデルのアウトプットを徹底的に評価する。
論文 参考訳（メタデータ） (2026-05-15T22:30:57Z) - ReLoop: Structured Modeling and Behavioral Verification for Reliable LLM-Based Optimization [6.572539312871392]
大規模言語モデル(LLM)は、自然言語を最適化コードに変換することができるが、サイレント障害は重大なリスクをもたらす。
2つの相補的な方向からサイレント障害に対処するReLoopを紹介します。
論文 参考訳（メタデータ） (2026-02-17T20:20:33Z) - A Systematic Analysis of Large Language Models with RAG-enabled Dynamic Prompting for Medical Error Detection and Correction [8.312687115594512]
我々は、ゼロショットプロンプト、ランダムな例による静的プロンプト、検索強化された動的プロンプトを評価する。
精度,リコール,偽陽性率 (FPR) , ROUGE-1, BLEURT, BERTScore を用いて誤差補正を行った。
論文 参考訳（メタデータ） (2025-11-25T02:40:49Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。
プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。
また, GPT-4o miniが74.18%と高い修理成功率を示した。
論文 参考訳（メタデータ） (2025-07-04T15:36:12Z) - High Accuracy, Less Talk (HALT): Reliable LLMs through Capability-Aligned Finetuning [84.52940628494879]
大規模言語モデル(LLM)は現在、すべてのプロンプトに応答する。
LLMは、知識や能力の欠如によって、誤った答えを生み出すことができる。
本稿では,その正確性に自信を持った場合にのみコンテンツを生成するためのLCMのポストトレーニングを提案する。
論文 参考訳（メタデータ） (2025-06-04T15:16:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。