論文の概要: LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean
- arxiv url: http://arxiv.org/abs/2607.28459v1
- Date: Thu, 30 Jul 2026 16:21:58 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-31 21:37:00.658
- Title: LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean
- Title（参考訳）: LeanCSP: リーンにおける制約改革と解決の認定のためのフレームワーク
- Abstract要約: 制約プログラミング(Constraint Programming)は、スケジューリング、計画、設定、検証といった複雑な問題を解決するための中核的な技術である。
リーン定理証明器では、両方の検証レベルに対処するフレームワークを導入します。
等式性、等式性、対称性を破る制約の正しさなどの定式化レベルの性質を証明するのに使うことができる。
- 参考スコア（独自算出の注目度）: 22.962110170304594
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Constraint programming is a core technology for solving complex combinatorial problems in scheduling, planning, configuration, and verification. Trusting its results therefore demands guarantees at two levels: that reformulations applied beforehand are semantics-preserving, and that solvers produce correct answers. In this work, we introduce a framework that addresses both verification levels in the Lean theorem prover: it can be used to prove formulation-level properties, such as equivalence, equisatisfiability, and the correctness of symmetry-breaking constraints, parametrically for entire problem families; and to check solver-produced certificates for individual instances via translation backends to external formats such as MiniZinc, SMT-LIB, and OPB. Combining both levels yields an end-to-end workflow that establishes the satisfiability or unsatisfiability of a constraint problem without trusting the external solver. Experimental results show that our framework's verified symmetry breaking also pays off in practice: a single parametric proof per problem family, reused across all instance sizes, reduces solver search effort by a factor of up to 2x10^7, while the entire in-Lean certification stays affordable, taking at most a few minutes for our largest instances.
- Abstract（参考訳）: 制約プログラミング(Constraint Programming)は、スケジューリング、計画、設定、検証において複雑な組合せ問題を解くための中核技術である。
したがって、その結果を信頼することは、前もって適用された改革がセマンティックス保存であり、解決者が正しい答えを生み出すという2つのレベルで保証を要求する。
本稿では,Leanの定理証明器における検証レベルの両方に対処するフレームワークを紹介する。同値性や適合性,および問題ファミリ全体のパラメトリックな対称性破り制約の正しさなどの定式化レベルの特性を証明し,MiniZinc,SMT-LIB,OCBといった外部フォーマットへの変換バックエンドを介して個々のインスタンスに対するソルバ生成証明書をチェックする。
両方のレベルを組み合わせることで、外部の解決者を信頼せずに制約問題の満足度や不満足性を確立するエンドツーエンドのワークフローが得られる。
問題族ごとのパラメトリック証明は、すべてのインスタンスサイズで再利用され、最大2x10^7の係数でソルバ探索の労力を削減します。
関連論文リスト
- Constraint-First Reasoning: A Training-Free Protocol for Exploiting Answer-Space Constraints in Mathematical Problem Solving [11.900982999786287]
Routed-CFRは、テキストのみのルータが制限キューを検出する場合にのみ、2段階のプロトコルを起動する。
AIME、CMIMC、BRUMO、AIMO_AMCを通して、複数のバックボーン上で直接CoTを改善する。
論文 参考訳（メタデータ） (2026-08-05T16:18:41Z) - STAIF: A Stage-wise Optimization for Complex Instruction Following [50.48101504556211]
STAIFは、客観的に検証可能な(ハード)制約の最適化から主観的(ソフト)制約のアライメントを分離する段階的な最適化フレームワークである。
この方法を支援するために,約31,000の複雑なマルチ制約命令からなる高品質なバイリンガル(英語,中国語)データセットであるSTAINSTRUCTを構築した。
論文 参考訳（メタデータ） (2026-06-26T06:14:07Z) - Certified Program Synthesis with a Multi-Modal Verifier [5.998029529040967]
LeetProofは、Leanに埋め込まれたマルチモーダル検証ツールであるVelvet上に構築されたエージェントパイプラインである。
動的検証、自動証明、インタラクティブな証明スクリプティングを1つの基礎フレームワークで組み合わせる。
我々は、認定合成に関する先行研究から得られたベンチマークに基づいてLeetProofを評価する。
論文 参考訳（メタデータ） (2026-04-17T14:56:45Z) - Training LLMs for Multi-Step Tool Orchestration with Constrained Data Synthesis and Graduated Rewards [76.49428173793386]
LLMは、中間出力を伝搬しながら、正しい順序で複数の依存APIを呼び出す必要がある。
既存の環境は、シミュレーションデータを使った単純なターン毎の関数呼び出しとバイナリ報酬に重点を置いている。
まず、実APIレスポンスの大規模キャッシュを背景とした強化学習環境を構築し、有効なマルチステップオーケストレーショントレースをサンプリングするデータ合成パイプラインを実現する。
第二に、正当性を原子の妥当性とオーケストレーションに分解する、段階的な報酬設計を提案する。
論文 参考訳（メタデータ） (2026-03-25T18:31:39Z) - Conformal Mixed-Integer Constraint Learning with Feasibility Guarantees [0.3058340744328236]
Conformal Mixed-Integer Constraint Learningは、最適化問題におけるデータ駆動制約の確率論的実現可能性を保証する。
我々は,C-MICLが目標レートを一貫して達成し,競争目標性能を維持し,既存の手法に比べて計算コストを大幅に削減することを示す。
論文 参考訳（メタデータ） (2025-06-04T03:26:31Z) - Fully Stochastic Trust-Region Sequential Quadratic Programming for
Equality-Constrained Optimization Problems [62.83783246648714]
目的と決定論的等式制約による非線形最適化問題を解くために,逐次2次プログラミングアルゴリズム(TR-StoSQP)を提案する。
アルゴリズムは信頼領域半径を適応的に選択し、既存の直線探索StoSQP方式と比較して不確定なヘッセン行列を利用することができる。
論文 参考訳（メタデータ） (2022-11-29T05:52:17Z) - Symmetric Tensor Networks for Generative Modeling and Constrained
Combinatorial Optimization [72.41480594026815]
ポートフォリオ最適化からロジスティクスに至るまで、制約付き最適化問題は業界に多い。
これらの問題の解決における主要な障害の1つは、有効な検索空間を制限する非自明なハード制約の存在である。
本研究では、Ax=bという形の任意の整数値等式制約をU(1)対称ネットワーク(TN)に直接エンコードし、それらの適用性を量子に着想を得た生成モデルとして活用する。
論文 参考訳（メタデータ） (2022-11-16T18:59:54Z) - Tensor Completion with Provable Consistency and Fairness Guarantees for
Recommender Systems [5.099537069575897]
非負・正の行列とテンソル完備問題を定義・解決するための新しい一貫性に基づくアプローチを導入する。
単一特性/制約: 単位スケールの一貫性を保ち、解の存在を保証し、比較的弱いサポート仮定の下では、一意性を示す。
論文 参考訳（メタデータ） (2022-04-04T19:42:46Z) - Certified Symmetry and Dominance Breaking for Combinatorial Optimisation [13.333957453318744]
本研究では,対称性と支配的破壊が容易に表現可能な最適化問題に対する認証手法を開発した。
提案手法は,提案手法が幅広い問題に適用可能であることを示す概念実証として,最大斜め解法と制約法に適用する。
論文 参考訳（メタデータ） (2022-03-23T08:45:35Z) - An Efficient Diagnosis Algorithm for Inconsistent Constraint Sets [68.8204255655161]
過制約問題における最小限の障害制約を識別する分割・分散型診断アルゴリズム(FastDiag)を提案する。
ヒットセットの競合指向計算とfastdiagを比較し,詳細な性能解析を行う。
論文 参考訳（メタデータ） (2021-02-17T19:55:42Z) - Combining Deep Learning and Optimization for Security-Constrained
Optimal Power Flow [94.24763814458686]
セキュリティに制約のある最適電力フロー(SCOPF)は、電力システムの基本である。
SCOPF問題におけるAPRのモデル化は、複雑な大規模混合整数プログラムをもたらす。
本稿では,ディープラーニングとロバスト最適化を組み合わせた新しい手法を提案する。
論文 参考訳（メタデータ） (2020-07-14T12:38:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。