論文の概要: SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification
- arxiv url: http://arxiv.org/abs/2609.00728v1
- Date: Tue, 01 Sep 2026 05:05:12 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-02 16:31:36.343022
- Title: SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification
- Title（参考訳）: SOVER: LLM支援SMT検証による最適化改革の形式的認定
- Authors: Swapnil Bhattacharyya, Mayank Baranwal,
- Abstract要約: 我々は、意味マッピングと正式な認証を分離するLLM支援SMTフレームワークであるSOVERを紹介する。
また、NLEquiv-150は100の等価性と50の故意に非等価な非線形改質ペアの公的なベンチマークである。
- 参考スコア（独自算出の注目度）: 2.6426981014417046
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large Language Models (LLMs) have shown remarkable promise in translating and reformulating complex mathematical optimization problems across modeling languages. However, validating such transformations through empirical solver executions alone is unreliable, as solver outcomes may be affected by local minima, structural timeouts, numerical artifacts, and subtle semantic divergence between formulations. We introduce SOVER, an LLM-assisted SMT framework that separates semantic mapping from formal certification: Z3 checks domain cross-feasibility and global objective-order preservation for mixed-integer linear formulations, while dReal provides tolerance-aware feasibility/range and $ε$-argmin checks for continuous nonlinear formulations. We also introduce NLEquiv-150, a public benchmark of 100 equivalent and 50 deliberately hard non-equivalent nonlinear reformulation pairs. With LLM-extracted mappings, SOVER classifies 149/150 pairs (99.33%) correctly, including all 50 hard negatives; the sole error is an incomplete mapping extraction.
- Abstract（参考訳）: 大規模言語モデル(LLM)は、モデリング言語全体にわたる複雑な数学的最適化問題の翻訳と修正において、顕著な将来性を示している。
しかし、そのような変換を経験的解法の実行だけで検証することは信頼性に欠けており、解法の結果は局所的なミニマ、構造的タイムアウト、数値的アーティファクト、および定式化間の微妙な意味的分岐の影響を受けうる。
Z3は、混合整数線形定式化のためのドメインのクロスファシビリティとグローバルなオブジェクト順序保存をチェックし、dRealは、連続非線形定式化のためのトレランス・アウェア・ファシビリティ/レンジと$ε$-argminチェックを提供する。
また、NLEquiv-150は100の等価性と50の故意に非等価な非線形改質ペアの公的なベンチマークである。
LLMを抽出したマッピングでは、SOVERは50個の強陰性を含む149/150対(99.33%)を正しく分類する。
関連論文リスト
- FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving [15.609601435289973]
私たちは、リーンとマシンチェックで形式化できるMILP改革の構成的定義を開発します。
提案手法を評価するために,20の問題と109の定式化のデータセットであるFormulationBenchを紹介した。
FLAREは既存の手法より優れており、フォーミュレーションベンチのNPハード部分集合では100%精度が高い。
論文 参考訳（メタデータ） (2026-08-25T23:19:41Z) - FormuEvo: LLM-Guided Evolution for Discovering Solver-Efficient Mixed-Integer Programming Formulations [66.32852384262038]
混合整数プログラミング(MIP)は、運用研究と産業最適化の核心にある。
FormuEvoは、解法効率のMIP式の自動発見のための進化的フレームワークである。
FormuEvoは、MIP定式化のシンボル空間上の進化的最適化として、MIP定式化設計を行う。
論文 参考訳（メタデータ） (2026-08-24T15:01:28Z) - CktFormalizer: Autoformalization of Natural Language into Circuit Representations [23.44745731124114]
CktFormalizerは、Lean 4.0に組み込まれた依存型HDLを通じてハードウェア生成をリダイレクトするフレームワークである。
VerilogEval(156問題)、RTLLM(50問題)、ResBench(56問題)では、CktFormalizerは直接Verilog生成と競合するシミュレーションパスレートを達成する。
論文 参考訳（メタデータ） (2026-05-08T14:20:06Z) - OpenSanctions Pairs: Large-Scale Entity Matching with LLMs [0.9131359219276399]
我々は,実世界の国際制裁アグリゲーションとアナリストの重複から派生した,大規模エンティティマッチングベンチマークOpenSanctions Pairsをリリースした。
データセットには、31か国で293の異種源にまたがる755,540のラベル付きペアが含まれている。
オフザシェルフ LLM は生産ルールベースのベースラインを大幅に上回っている。
論文 参考訳（メタデータ） (2026-02-24T06:25:49Z) - ReLoop: Structured Modeling and Behavioral Verification for Reliable LLM-Based Optimization [6.572539312871392]
大規模言語モデル(LLM)は、自然言語を最適化コードに変換することができるが、サイレント障害は重大なリスクをもたらす。
2つの相補的な方向からサイレント障害に対処するReLoopを紹介します。
論文 参考訳（メタデータ） (2026-02-17T20:20:33Z) - Constructing Industrial-Scale Optimization Modeling Benchmark [26.61380804019141]
重要なボトルネックは、実際の最適化モデルに根ざした、自然言語仕様と参照定式化/解決コードとを一致させるベンチマークの欠如である。
実混合整数線形プログラムから構造を意識した逆構成手法により構築したMIPLIB-NLを提案する。
実験の結果,MIPLIB-NLは既存のベンチマークに強く依存するシステムに対して,大幅な性能低下を示した。
論文 参考訳（メタデータ） (2026-02-11T02:45:31Z) - From Abstract to Contextual: What LLMs Still Cannot Do in Mathematics [79.81905350372067]
我々は文脈的数学的推論を通してギャップを研究する。
AIMEとMATH-500の問題を2つのコンテキスト設定に再利用するベンチマークであるContextMATHを紹介する。
オープンソースモデルはSGとCSで13、34ポイント減少し、プロプライエタリモデルは13、20ポイント減少している。
論文 参考訳（メタデータ） (2026-01-30T14:56:04Z) - The Hidden Cost of Approximation in Online Mirror Descent [56.99972253009168]
オンラインミラー降下(OMD)は、最適化、機械学習、シーケンシャルな意思決定において多くのアルゴリズムの基盤となる基本的なアルゴリズムパラダイムである。
本研究では,不正確なOMDに関する系統的研究を開始し,正規化器の滑らかさと近似誤差に対する頑健さとの複雑な関係を明らかにする。
論文 参考訳（メタデータ） (2025-11-27T10:09:07Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - Decomposing Uncertainty for Large Language Models through Input Clarification Ensembling [69.83976050879318]
大規模言語モデル(LLM)では、不確実性の原因を特定することが、信頼性、信頼性、解釈可能性を改善するための重要なステップである。
本稿では,LLMのための不確実性分解フレームワークについて述べる。
提案手法は,入力に対する一連の明確化を生成し,それらをLLMに入力し,対応する予測をアンサンブルする。
論文 参考訳（メタデータ） (2023-11-15T05:58:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。