論文の概要: LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification
- arxiv url: http://arxiv.org/abs/2610.30524v1
- Date: Wed, 21 Oct 2026 23:09:46 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-24 02:08:44.173975
- Title: LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification
- Title（参考訳）: LLM2Cert:SMT/Lean検証による証明書のLCM合成
- Abstract要約: リャプノフ関数とバリア証明書は、国家空間の安定性と安全性を保証する。
既存のパイプラインは、数値解法、区間法、あるいは満足度・モジュラー理論の候補を検証する。
- 参考スコア（独自算出の注目度）: 48.25461891128527
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Lyapunov functions and barrier certificates give state-space guarantees of stability and safety, but synthesizing and verifying them---especially for nonlinear, high-dimensional systems---remains an open challenge. Existing pipelines verify candidates with numerical solvers (sum-of-squares programs), interval methods, or satisfiability-modulo-theories (SMT) solvers, which often require relaxations, are conservative, or scale poorly with model dimension and nonlinearity. These limitations have also shaped benchmark design: standard test suites are dominated by low-dimensional polynomial systems chosen to suit what solvers can handle rather than what engineering applications require. We address both sides of this challenge. First, we introduce DynaCertBench, a benchmark of 105 instances: 80 non-redundant systems curated from the literature, extended with high-dimensional and control-constrained variants and new nonlinearly coupled systems, comprehensively spanning stability, region-of-attraction, forward-invariance, and safety tasks. Second, we present LLM2Cert, an LLM-driven framework that synthesizes candidate certificates and verifies them against their proof obligations: each obligation is routed to an SMT solver or directly to the Lean Proof-Repair agent. On DynaCertBench, LLM2Cert verifies 81 of 105 instances ($77.1\%$), a $17.1$ percentage point improvement over one-shot proposal without feedback. On the 81 fixed certificates, LLM2Cert verifies 22 that All-SMT leaves unresolved. Code and data are available at https://github.com/FormalCert-AI/llm2cert.
- Abstract（参考訳）: リャプノフ関数とバリア証明書は、安定性と安全性の国家空間保証を与えるが、それらの合成と検証は、特に非線形で高次元のシステムにとって、オープンな課題として残されている。
既存のパイプラインは数値解法 (sum-of-squares program, interval method, or satisfiability-modulo-theories, SMT) の候補を検証する。
標準的なテストスイートは、エンジニアリングアプリケーションに必要なものではなく、解決者が扱えるものに適合するように選択された低次元多項式システムによって支配される。
この課題の両面に対処する。
まず、文献から算出した80の非冗長系、高次元および制御制約付き変種と新しい非線形結合系、包括的安定性、領域抽出、前方不変性、安全タスクを含む105のインスタンスのベンチマークであるDynaCertBenchを紹介する。
第二に、LSM2Certは、候補証明書を合成し、それらの証明義務に反して検証するLLM駆動のフレームワークである。
DynaCertBench では LLM2Cert が 105 インスタンス中 81 インスタンス (77.1\%$) を検証する。
LLM2Certは、81の固定証明書で、全SMTが未解決のままであることを確認する。
コードとデータはhttps://github.com/FormalCert-AI/llm2cert.comで公開されている。
関連論文リスト
- CertMoE: Robustness Certification for Mixture-of-Experts LLMs via Routing-Aware Smoothing [50.77807239365757]
確率的堅牢性は、敵の摂動下でのモデル予測を保証することを目的として、信頼できる機械学習の基盤となる。
本稿では,MoE大言語モデルのための最初のルーティング対応認証フレームワークであるtextscCertMoEについて述べる。
論文 参考訳（メタデータ） (2026-10-21T08:25:15Z) - An Interactive Agent for Requirement-Driven Candidate Sourcing [75.63902836826038]
最初の要件駆動型候補ソーシングエージェントであるsysを提示する。
それは、あいまいな人々の要求を正当化されたスレートに導き、検証し、回収し、検証する。
広さ (100%$カバレッジ 2.5times$ the yield) を支配し、フィールドに直交する。
論文 参考訳（メタデータ） (2026-08-24T17:04:16Z) - LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean [22.962110170304594]
制約プログラミング(Constraint Programming)は、スケジューリング、計画、設定、検証といった複雑な問題を解決するための中核的な技術である。
リーン定理証明器では、両方の検証レベルに対処するフレームワークを導入します。
等式性、等式性、対称性を破る制約の正しさなどの定式化レベルの性質を証明するのに使うことができる。
論文 参考訳（メタデータ） (2026-07-30T16:21:58Z) - Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis [14.825615940318038]
ZkEVMは、オフチェーン実行の正しさを保証するゼロ知識を生成する。
微妙な実装上のバグは、意味的に欠陥のある状態を証明する有効な証明につながる可能性がある。
SMTソルバによる形式検証は、これを防止できるが、仕様によってボトルネックとなる。
Rustから実行可能なPython/Z3検証モデルを合成するフレームワークであるVeri Synthを提案する。
論文 参考訳（メタデータ） (2026-07-22T06:20:36Z) - Training LLMs for Multi-Step Tool Orchestration with Constrained Data Synthesis and Graduated Rewards [76.49428173793386]
LLMは、中間出力を伝搬しながら、正しい順序で複数の依存APIを呼び出す必要がある。
既存の環境は、シミュレーションデータを使った単純なターン毎の関数呼び出しとバイナリ報酬に重点を置いている。
まず、実APIレスポンスの大規模キャッシュを背景とした強化学習環境を構築し、有効なマルチステップオーケストレーショントレースをサンプリングするデータ合成パイプラインを実現する。
第二に、正当性を原子の妥当性とオーケストレーションに分解する、段階的な報酬設計を提案する。
論文 参考訳（メタデータ） (2026-03-25T18:31:39Z) - MCTS-Refined CoT: High-Quality Fine-Tuning Data for LLM-Based Repository Issue Resolution [18.314436803012434]
本稿では,モンテカルロ木探索(MCTS)に基づく中間推論ステップの動的検証と最適化を行うMCTS-INEを提案する。
SWE-bench LiteとSWE-bench Verifiedの実験は、我々のCoTデータセットで微調整されたLLMがベースラインよりも大幅に改善されたことを示す。
論文 参考訳（メタデータ） (2025-06-15T05:42:01Z) - APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。
エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。
この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
論文 参考訳（メタデータ） (2025-05-09T03:38:31Z) - CyberSecEval 2: A Wide-Ranging Cybersecurity Evaluation Suite for Large Language Models [6.931433424951554]
大規模言語モデル(LLM)は新たなセキュリティリスクを導入するが、これらのリスクを計測し、削減するための包括的な評価スイートはほとんどない。
LLMのセキュリティリスクと能力を定量化する新しいベンチマークであるBenchmarkNameを提案する。
我々は,GPT-4,Mistral,Meta Llama 370B-Instruct,Code Llamaを含む複数のSOTA (State-of-the-art) LLMを評価した。
論文 参考訳（メタデータ） (2024-04-19T20:11:12Z) - Decomposing Uncertainty for Large Language Models through Input Clarification Ensembling [69.83976050879318]
大規模言語モデル(LLM)では、不確実性の原因を特定することが、信頼性、信頼性、解釈可能性を改善するための重要なステップである。
本稿では,LLMのための不確実性分解フレームワークについて述べる。
提案手法は,入力に対する一連の明確化を生成し,それらをLLMに入力し,対応する予測をアンサンブルする。
論文 参考訳（メタデータ） (2023-11-15T05:58:35Z) - Learning Mixtures of Linear Dynamical Systems [94.49754087817931]
そこで我々は,2段階のメタアルゴリズムを開発し,各基底構造LPSモデルを誤り$tildeO(sqrtd/T)$.sqrtd/T)まで効率的に復元する。
提案手法の有効性を検証し,数値実験による理論的研究を検証する。
論文 参考訳（メタデータ） (2022-01-26T22:26:01Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。