論文の概要: FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving
- arxiv url: http://arxiv.org/abs/2608.25220v1
- Date: Tue, 25 Aug 2026 23:19:41 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-27 14:15:15.491507
- Title: FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving
- Title（参考訳）: FLARE: LLMに基づく理論証明によるMILP改革の検証
- Abstract要約: 私たちは、リーンとマシンチェックで形式化できるMILP改革の構成的定義を開発します。
提案手法を評価するために,20の問題と109の定式化のデータセットであるFormulationBenchを紹介した。
FLAREは既存の手法より優れており、フォーミュレーションベンチのNPハード部分集合では100%精度が高い。
- 参考スコア（独自算出の注目度）: 15.609601435289973
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Mixed-Integer Linear Programming (MILP) is a fundamental tool for combinatorial optimization with extensive real-world applications. A central challenge is designing computationally efficient MILP formulations. Large Language Models (LLMs) offer new opportunities to automate the modeling process, from deriving formulations to strengthening them. Reliable automation requires robust methods for verifying that proposed formulations preserve the underlying optimization problem. However, existing approaches evaluate formulations numerically and fail to reason about general problem instances. We resolve this limitation by introducing a constructive definition of MILP reformulation that can be formalized in Lean and machine-checked. We develop FLARE (Formulation-Level Automated Reformulation Evaluation), a method that uses an LLM-based agent and the Lean proof assistant to verify proposed reformulations against a reference formulation. To evaluate our approach, we introduce FormulationBench, a challenging dataset of 20 problems and 109 formulations. FLARE outperforms existing methods, with 100% accuracy on the NP-hard subset of FormulationBench. Furthermore, FLARE produces a machine-checkable certificate for every reformulation it accepts. For cases where formal guarantees are not necessary, we introduce FLARE-NL, a fast and cheap LLM proxy that matches FLARE's accuracy but produces no certificate. These methods enable reliable verification in automated optimization modeling.
- Abstract（参考訳）: Mixed-Integer Linear Programming (MILP) は、大規模な実世界のアプリケーションと組み合わせ最適化のための基本的なツールである。
中心的な課題は、計算効率の良いMILPの定式化を設計することである。
大規模言語モデル(LLM)は、定式化の導出から強化に至るまで、モデリングプロセスを自動化する新たな機会を提供する。
信頼性の高い自動化には、提案された定式化が基礎となる最適化問題を保存することを検証する堅牢な方法が必要である。
しかし、既存の手法では、定式化を数値的に評価し、一般的な問題事例の推論に失敗する。
リーンやマシンチェックで形式化できるMILP改定の構成的定義を導入することで、この制限を解消します。
我々は,LLMエージェントとリーン証明アシスタントを用いて参照定式化に対する提案された改定の検証を行うFLARE(Formulation-Level Automated Reformulation Evaluation)を開発した。
提案手法を評価するために,20の課題と109の定式化の挑戦的データセットであるFormulationBenchを紹介した。
FLAREは既存の手法より優れており、フォーミュレーションベンチのNPハード部分集合では100%精度が高い。
さらに、FLAREは、それが受け入れる改革ごとに、マシンチェック可能な証明書を生成する。
正式な保証を必要としない場合、FLARE-NLは高速で安価なLCMプロキシで、FLAREの精度に適合するが証明書は生成しない。
これらの手法は、自動最適化モデリングにおける信頼性の高い検証を可能にする。
関連論文リスト
- 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) - Opt-Verifier: Unleashing the Power of LLMs for Optimization Modeling via Dual-Side Verification [53.763212981479455]
本稿では、構造と解の両方の観点から、デュアルサイド検証(Opt-Verifier)を用いた新しいフレームワークを提案する。
一般的なベンチマーク実験により、我々の手法は精度が20%以上向上していることが示された。
論文 参考訳（メタデータ） (2026-05-28T08:09:52Z) - VeriSimpl: Robust Optimization Modeling from Natural Language using Simplification-based Verification [0.43665049670577916]
自然言語から最適化への堅牢な形式化のためのフレームワークであるVeriSimplを紹介する。
我々のアプローチは、単純化に基づく検証という考え方に基づいている。
提案手法は既存の手法に比べて精度が一貫した改善を提供すると同時に,新しい高精度自己検証信号を提供する。
論文 参考訳（メタデータ） (2026-05-24T13:46:54Z) - Execution-Verified Reinforcement Learning for Optimization Modeling [49.171122807323634]
実行検証学習フレームワークは、数学的プログラミング解法を決定論的で対話的な検証器として扱う。
NL4OPT, MAMO, IndustryOR, OptiBenchをグロビ, OR-Tools, COPTで行った実験では, EVOMがプロセス管理SFTに適合または優れていた。
論文 参考訳（メタデータ） (2026-04-01T03:39:11Z) - LM4Opt-RA: A Multi-Candidate LLM Framework with Structured Ranking for Automating Network Resource Allocation [0.7933039558471408]
我々は,複雑な解析的および数学的推論タスクに,文脈的理解が不要であることに対処する。
既存のベンチマークデータセットは、動的な環境、変数、不均一な制約でそのような問題の複雑さに対処できない。
NL4RAは、LP、ILP、MILPとして定式化された50のリソース割り当て最適化問題からなるキュレートデータセットである。
次に,パラメータ数が異なるオープンソースのLLMの性能評価を行った。
論文 参考訳（メタデータ） (2025-11-13T23:19:43Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - Peering Inside the Black Box: Uncovering LLM Errors in Optimization Modelling through Component-Level Evaluation [0.0]
大規模言語モデル(LLM)のためのコンポーネントレベル評価フレームワークを提案する。
GPT-5、LLaMA 3.1命令、DeepSeek Mathを様々な複雑さの最適化問題で評価する。
その結果、GPT-5は他のモデルよりも一貫して優れており、チェーン・オブ・シンク、自己整合性、モジュール性がより効果的であることを証明している。
論文 参考訳（メタデータ） (2025-10-19T17:47:59Z) - From Natural Language to Solver-Ready Power System Optimization: An LLM-Assisted, Validation-in-the-Loop Framework [1.7136832159667206]
本稿では,Large Language Models (LLMs) を用いたエージェントを導入し,電力系統最適化シナリオの自然言語記述を,コンパクトで解決可能な定式化に自動変換する。
提案手法は,オフザシェルフ最適化解法により効率よく解ける数学的に互換性のある定式化の発見に重点を置いている。
論文 参考訳（メタデータ） (2025-08-11T16:22:57Z) - SPARE: Single-Pass Annotation with Reference-Guided Evaluation for Automatic Process Supervision and Reward Modelling [58.05959902776133]
私たちはSingle-Passを紹介します。
Reference-Guided Evaluation (SPARE)は、効率的なステップごとのアノテーションを可能にする新しい構造化フレームワークである。
数学的推論(GSM8K, MATH)、マルチホップ質問応答(MuSiQue-Ans)、空間推論(SpaRP)にまたがる4つの多様なデータセットにおけるSPAREの有効性を実証する。
ProcessBenchでは、SPAREがデータ効率のよいアウト・オブ・ディストリビューションの一般化を実証し、トレーニングサンプルの$sim$16%しか使用していない。
論文 参考訳（メタデータ） (2025-06-18T14:37:59Z) - Autoformulation of Mathematical Optimization Models Using LLMs [50.030647274271516]
本稿では,自然言語問題記述から解法対応最適化モデルを自動生成する,$textitautoformulation$の問題にアプローチする。
オートフォーミュレーションの3つの主要な課題を識別する: $textit(1)$ 巨大で問題に依存した仮説空間、および$textit(2)$ 不確実性の下でこの空間を効率的かつ多様に探索する。
我々は,$textitLarge Language Models$と$textitMonte-Carlo Tree Search$を併用した新しい手法を提案する。
論文 参考訳（メタデータ） (2024-11-03T20:41:38Z) - Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。
LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。
本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
論文 参考訳（メタデータ） (2024-10-05T05:21:48Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。