論文の概要: ORSMT: Unleashing the Potential of Satisfiability Modulo Theories for Semantic Verification and Repair in LLM-Based Optimization
- arxiv url: http://arxiv.org/abs/2610.29145v1
- Date: Wed, 21 Oct 2026 03:27:02 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-23 00:40:06.191277
- Title: ORSMT: Unleashing the Potential of Satisfiability Modulo Theories for Semantic Verification and Repair in LLM-Based Optimization
- Title（参考訳）: ORSMT: LLM最適化における意味的検証と修復のための満足度モデュロ理論の可能性
- Abstract要約: ORSMTは型付きセマンティックインタフェースと正確なSMT関係クエリを提供する。
ORSMTは選択前の72のベンチマークとジェネレータの組み合わせのモデルコードマッチング率を改善する。
別個の1ラウンドのソース修正と、正確な再構築により、反証されたペアの84.4%のモデルコードマッチングが復元される。
- 参考スコア（独自算出の注目度）: 34.593904557353206
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Large language models increasingly automate optimization modeling from natural language problems, producing written mathematics, solver code and a returned report. Verifying one optimization problem across these artifacts requires semantic comparison: unequal models can attain the same objective, equivalent models can use different auxiliary variables, and mutually consistent artifacts can omit the same source requirement. ORSMT provides a typed semantic interface and exact SMT relation queries. It aligns observable decisions, projects auxiliary variables, proves or refutes feasible region and objective relations, localizes refutations to implicated rows or domains and links source texts when available. It then reconstructs one artifact from another, and each adopted candidate passes the required relation checks. Across 3,034 problems and six generator sizes, ORSMT improves the model-code match rate in all 72 benchmark and generator combinations before selection. Protected selection raises the aggregate rate from 43.2% to 88.2% and the share that are both correct and matched from 25.2% to 40.2%. On the 1,905 refuted outputs, certified voting under the shared fallback makes 50.9% of outputs correct and matched, compared with 44.8% for ReLoop and 49.4% for Opt-Verifier. A separate one-round source revision followed by exact reconstruction restores a model-code match for 84.4% of the refuted pairs.
- Abstract（参考訳）: 大規模言語モデルは、自然言語問題からの最適化モデリングを自動化し、記述された数学、ソルバコード、返却されたレポートを生成する。
不平等モデルは同じ目的を達成することができ、等価モデルは異なる補助変数を使用することができ、相互に一貫性のあるアーティファクトは同じソース要求を省略することができる。
ORSMTは型付きセマンティックインタフェースと正確なSMT関係クエリを提供する。
観測可能な決定、補助変数のプロジェクト、実現可能な領域と客観的な関係の証明または論証、関連する行やドメインへの論拠のローカライズ、利用可能なソーステキストのリンクなどと整合する。
その後、別のアーティファクトから1つのアーティファクトを再構築し、それぞれの採用候補が要求される関係チェックをパスする。
3,034問題と6つのジェネレータサイズにまたがって、ORSMTは選択前の72のベンチマークとジェネレータの組み合わせのモデルコードマッチング率を改善する。
保護選択率は43.2%から88.2%に上昇し、それぞれ25.2%から40.2%に一致している。
1,905票の反対票は50.9%が正当であり、ReLoopは44.8%、Opt-Verifierは49.4%である。
別個の1ラウンドのソース修正と、正確な再構築により、反証されたペアの84.4%のモデルコードマッチングが復元される。
関連論文リスト
- Bayesian Test-Time Inference of Task-Aligned Similarity from Weak Interactive Feedback [50.42640957891911]
言語モデルシステムは、類似性を比較することで、繰り返しテスト時の決定を行う。
しかし、類似性はユニークではない:語彙、意味、構造、類似性はNの選択点を取得することができる。
本稿では,現在の意思決定を統括するトレーニングフリーベイズ手法であるAxis Interactive Signalsを紹介する。
論文 参考訳（メタデータ） (2026-10-13T16:19:49Z) - DV-Lens: Revealing the Functional Organization of Language Model Parameters [53.18682247752397]
本稿では,ネイティブパラメータの方向と下流語彙の応答を関連付けるパラメータレベルの解釈可能性フレームワークを提案する。
語彙読み出しによるパラメータ列の分類と下流語彙複雑性(DV-複雑度)の導入
これらの結果は、DV-複雑度解釈の介入に基づく証拠を提供し、DV-複雑度とモデル能力の関係を明らかにする。
論文 参考訳（メタデータ） (2026-10-03T12:45:07Z) - Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations [0.0]
大規模言語モデル(LLM)は、SystemVerilog Assertion(SVA)の自動生成のために、ますます研究されている。
ほとんどの評価では、入力の単一の構文表現に正確さを報告している。
そのような点の精度は、モデルの正しい出力が同じRTLの振る舞いが異なる場合に安定であるかどうかを明らかにしない。
論文 参考訳（メタデータ） (2026-09-04T18:41:58Z) - ModelEquivBench: Certifying Multi-Relational Evaluation of LLM-Generated Optimization Models [6.820882579439242]
マルチリレーショナル評価システムであるModelEquivBenchを提案する。
それぞれのエントリは、E0--E1、正のE2--E6結論の正確な有理証明のための関係適切なトレースまたは明示的なマップを持っている。
結果として得られるプロファイルは、粗いベースラインが表現しない区別を明らかにする。
論文 参考訳（メタデータ） (2026-07-31T13:55:09Z) - Efficient Visual Pointing for Embodied AI:Agent-Driven Data Synthesis, Cross-Block Attention, and Iterative Correction [55.11480729304395]
PointArena 2026は77.2%の精度でベンチマークで2位である。
ap proachは3つの障害モードをターゲットにしている。第一に、エージェント駆動のシンセシスは大きなセマンティクスとアンカー相対的な候補プールを構築する。
次に、determinis tic steerable-dataパイプラインは、認証された10,000サンプルのメインセットと、マスク、テンプレート、パス検証を使用するリザーブサンプルを生成する。
論文 参考訳（メタデータ） (2026-06-29T06:39:03Z) - Selective QA over Conflicting Multi-Source Personal Memory: A Diagnostic Testbed and Method Comparison [11.187819120306825]
既存のベンチマークでは、メソッドに与えられたエビデンスやメソッドのコンフリクト解決ステップからエラーが生じたかどうかはほとんど示されていない。
我々はこれをマルチソース・パーソナルメモリの競合に対する選択的QAとして検討する。
8種類の推論型,480のペルソナ,4つのランダムシード,34,560のインスタンスを対象とした18の質問テンプレートを含むベンチマークを作成した。
論文 参考訳（メタデータ） (2026-05-28T15:33:39Z) - Models Can Model, But Can't Bind: Structured Grounding in Text-to-Optimization [54.749573452394664]
定式化自体が単純である場合でも、インスタンスデータが大きくなるにつれて精度が低下する。
我々は, 数値データを構造化ファイルに外部化する単純な推論時アプローチであるBINDを用いて, モデルがプロンプトプロンプトからではなく, データをバインドする。
我々は,モデルのみをバインディングのみに微調整することで仮説を検証し,3つの構造的に異なる最適化カテゴリにおいて,エンドツーエンドのSFTおよびRLよりも優れていることを示す。
論文 参考訳（メタデータ） (2026-05-20T21:25:41Z) - ReLoop: Structured Modeling and Behavioral Verification for Reliable LLM-Based Optimization [6.572539312871392]
大規模言語モデル(LLM)は、自然言語を最適化コードに変換することができるが、サイレント障害は重大なリスクをもたらす。
2つの相補的な方向からサイレント障害に対処するReLoopを紹介します。
論文 参考訳（メタデータ） (2026-02-17T20:20:33Z) - EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。
このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。
19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
論文 参考訳（メタデータ） (2025-02-18T02:54:25Z) - Entropy Adaptive Decoding: Dynamic Model Switching for Efficient Inference [0.0]
本稿では,効率的な言語モデル推論のための新しいアプローチであるEntropy Adaptive Decoding (EAD)を提案する。
EADは予測の不確実性に基づいて、異なるサイズのモデル間で切り替える。
異なるモデルファミリー間で顕著な効率向上を示す。
論文 参考訳（メタデータ） (2025-02-05T22:15:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。