論文の概要: From Errors to Proofs: Minimal-Core-Guided Repair for Neuro-Symbolic Constraint Solving
- arxiv url: http://arxiv.org/abs/2608.14771v1
- Date: Fri, 14 Aug 2026 14:48:36 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-18 19:59:03.076526
- Title: From Errors to Proofs: Minimal-Core-Guided Repair for Neuro-Symbolic Constraint Solving
- Title（参考訳）: 誤りから証明へ:ニューロシンボリック制約解法における最小コアガイド修復法
- Abstract要約: 最小限のコアは、素のエラーではなく、より弱いモデルが解決策を作らずに実現不可能な問題に陥ることが示される。
強力なチェーンオブソートベースラインは、正確さでシンボルルートと一致しているため、ルートの値が正確ではなく、証明書と製造を拒否する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Making language models solve constraint problems reliably often means having them translate the problem into a formal specification and delegating the search to a sound solver. But the translation is itself a language-model task, and an unfaithful translation makes the solver faithfully solve the wrong problem. Existing pipelines repair only translations that crash, returning the solver's error message and falling silent when the program runs but is wrong. We replace the error message with a proof: when the generated program is unsatisfiable, we extract a minimal unsatisfiable core over the model's own constraints and hand it back the exact set that cannot hold together, a leakage-free signal that localizes the fault. On a new benchmark of 77 problems with an exact oracle, translation to Answer Set Programming is faithful on six of seven domains and fails only on aggregate coverage scheduling, which concentrates the translation tax in one diagnosable pattern. A minimal core, rather than a bare error, is what stops a weaker model from fabricating solutions to infeasible problems, cutting fabrication from 79% to 7%. A strong chain-of-thought baseline meanwhile matches the symbolic route on accuracy, so the route's value is not accuracy but certificates and its refusal to fabricate.
- Abstract（参考訳）: 言語モデルに制約問題を確実に解決させることは、問題を形式的な仕様に翻訳し、探索をサウンドソルバに委譲することを意味する。
しかし、翻訳自体が言語モデルタスクであり、不誠実な翻訳は、解決者が間違った問題を忠実に解決する。
既存のパイプラインは、クラッシュした翻訳のみを修復し、ソルバのエラーメッセージを返却し、プログラムの実行時にサイレントに落ちる。
生成されたプログラムが満足できない場合、モデル自身の制約に対して最小限の満足できないコアを抽出し、その欠陥をローカライズするリークフリー信号である、保持できない正確なセットを返します。
77の問題を厳密なオラクルでベンチマークした結果、Answer Set Programmingへの変換は7つのドメインのうち6つに忠実であり、総合的なカバレッジスケジューリングにのみ失敗し、翻訳税を1つの診断可能なパターンに集中させる。
最小限のコアは、最小限のエラーではなく、より弱いモデルが解決策を作らずに実現不可能な問題に陥り、製造を79%から7%に削減する。
強いチェーン・オブ・シンクのベースラインは、正確さでシンボルのルートと一致しているため、ルートの値が正確ではなく、証明書と製造を拒否する。
関連論文リスト
- Constrained Decoding for Diffusion Language Models via Efficient Inference over Finite Automata [57.27430779838529]
有限オートマトンとして表現可能な任意の制約の下で,制約付き平均場後部からサンプリングする,正確かつトラクタブルなアルゴリズムを提案する。
このアプローチは、構築による制約満足度を保証し、欲求とサンプリングベースのデコーディングの両方をサポートし、並列およびブロックワイドデコーディングと互換性がある。
Dream-7B と LLaDA-8 の実証的な評価は、様々なタスクにおいてかなりの精度の向上を示した。
論文 参考訳（メタデータ） (2026-07-08T05:48:57Z) - From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
大規模な言語モデルは、自動化されたソフトウェア工学における約束を示すが、その正しさの保証は、誤ったコードや幻覚的なコードによってしばしば損なわれる。
NaturalLanguage2VerifiedCodeデータセット:60の複雑なアルゴリズム問題の集合を提供する。
7個のオープンウェイト LLM でランダムに選択された11個の問題集合をタイレッドプロンプト戦略を用いて評価した。
以上の結果から,コンテキストレスなプロンプトがほぼユニバーサルの失敗につながる一方で,構造的アンカーと反復的自己修復が劇的なパフォーマンスの転換を促進することが示唆された。
論文 参考訳（メタデータ） (2026-04-24T14:28:10Z) - Project Prometheus: Bridging the Intent Gap in Agentic Program Repair via Reverse-Engineered Executable Specifications [14.657771106188115]
現在のソリューションは、自然言語の要約や敵のサンプリングに頼っているが、手術の修理に必要な決定論的制約を与えていないことが多い。
コード生成よりもtextitSpecification Inference を優先することで、このギャップを埋める新しいフレームワークである textscPrometheus を紹介します。
我々のフレームワークは textbf93.97% (639/680) の完全なパッチレートを達成した。
論文 参考訳（メタデータ） (2026-04-19T14:27:27Z) - Mitigating Legibility Tax with Decoupled Prover-Verifier Games [14.915295611754132]
検査可能性条件から正しさを分離した解を提案する。
我々は、平衡が忠実でチェック可能な翻訳者に対応する分離された証明検証ゲームを定式化する。
論文 参考訳（メタデータ） (2026-02-26T17:25:22Z) - Programming over Thinking: Efficient and Robust Multi-Constraint Planning [54.77940831026738]
SCOPEは、クエリ固有の推論をジェネリックコード実行から切り離すフレームワークである。
SCOPEは、コストとレイテンシを下げながら最先端のパフォーマンスを達成する。
論文 参考訳（メタデータ） (2026-01-14T02:58:07Z) - Probing for Arithmetic Errors in Language Models [86.8227317662622]
言語モデルの内部アクティベーションは、算術誤差を検出するために使用できる。
単純なプローブはモデルが予測した出力と正解の両方を隠蔽状態から正確に復号できることを示す。
モデル精度を90%以上の精度で予測する軽量エラー検出器を訓練する。
論文 参考訳（メタデータ） (2025-07-16T16:27:50Z) - 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) - GRACE: Discriminator-Guided Chain-of-Thought Reasoning [75.35436025709049]
本稿では, 正しい推論手順を導出するために, GRACE (CorrectnEss Discriminator) を用いたチェーン・オブ・シークレット・リAsoningを提案する。
GRACEは、正しいステップと間違ったステップに対して対照的な損失で訓練された判別器を採用しており、復号時に次のステップ候補を採点するために使用される。
論文 参考訳（メタデータ） (2023-05-24T09:16:51Z) - Towards Fine-Grained Information: Identifying the Type and Location of
Translation Errors [80.22825549235556]
既存のアプローチでは、エラーの位置と型を同期的に考慮することはできない。
我々はtextbf の追加と textbfomission エラーを予測するために FG-TED モデルを構築した。
実験により,本モデルではエラータイプと位置の同時同定が可能であり,最先端の結果が得られた。
論文 参考訳（メタデータ） (2023-02-17T16:20:33Z) - Leveraging Automated Unit Tests for Unsupervised Code Translation [34.84910520660154]
本稿では,無効翻訳をフィルタリングする自動単体テストシステムを提案する。
このフィルタデータセットを用いて教師なしモデルの微調整を行うことで,翻訳のノイズを著しく低減できることがわかった。
特に、Java $to$ Python と Python $to$ C++ は、それぞれ 16% と 24% よりも優れています。
論文 参考訳（メタデータ） (2021-10-13T15:08:43Z) - End-to-End Lexically Constrained Machine Translation for Morphologically
Rich Languages [0.0]
本研究は, 機械翻訳による単語の正しいインフレクションを許容する機構について検討する。
英語とチェコ語のペアを用いた実験により, 自動評価と手動評価の両方において, 制約付き単語の翻訳が改良されることが示唆された。
論文 参考訳（メタデータ） (2021-06-23T13:40:13Z) - Improving Translation Robustness with Visual Cues and Error Correction [58.97421756225425]
ノイズの多いテキストに対する翻訳の堅牢性を改善するビジュアルコンテキストのアイデアを紹介します。
また,誤り訂正を補助タスクとして扱うことで,新しい誤り訂正訓練手法を提案する。
論文 参考訳（メタデータ） (2021-03-12T15:31:34Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。