論文の概要: Foundational Constraint Solving for Expressive Refinement Typing
- arxiv url: http://arxiv.org/abs/2607.12226v1
- Date: Tue, 14 Jul 2026 00:15:23 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-15 17:08:29.995556
- Title: Foundational Constraint Solving for Expressive Refinement Typing
- Title（参考訳）: 表現型リファインメントタイピングのための基礎的制約解法
- Abstract要約: LEANで実装された制約付きホーンクロース(CHC)ソルバであるFLEXについて述べる。
FLEXは,信頼性の高いベースをカーネルのみに還元し,LEANの証明エコシステム全体を低レベルシステムコードの検証に利用することができることを示す。
- 参考スコア（独自算出の注目度）: 0.9624643581968987
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: SMT-based program verifiers are hamstrung by two problems: expressiveness, because predictable verification restricts to the boundaries of SMT decidability, and trust, because the solver is a large, unverified artifact whose soundness bugs may quietly compromise every tool built on it. We present FLEX, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, that reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code, via three contributions. First, FLEX encodes CHCs as plain LEAN propositions where the Horn variables are existentially bound predicates, and shows how to implement CHC solvers as tactics (meta-programs) that compute kernel checkable proofs of the CHC propositions. Second, we show how to implement two verified CHC generators in LEAN: a Floyd-Hoare style generator for an imperative language, and a refinement-type-based generator for a functional calculus, which can be composed with the solving tactics to yield the first end-to-end foundational CHC-based verifiers. Finally, we show how FLEX allows us to leapfrog the expressiveness limitations of SMT by unleashing LEAN's entire ecosystem of proof machinery to prove arbitrary functional correctness properties of various low-level Rust libraries using the FLUX refinement type checker, and demonstrate the viability of FLEX as a trustworthy CHC backend, by showing it automatically discharges 95.7% of the CHCs from FLUX's benchmark suite.
- Abstract（参考訳）: SMTベースのプログラム検証は、表現性、予測可能な検証は、SMT決定可能性の境界に制限されるため、信頼という2つの問題によって妨げられている。
本稿では、LEANで実装された基礎的制約付きホーンクロース(CHC)解決器であるFLEXを紹介し、信頼基盤をカーネルのみに還元し、3つのコントリビューションを通じてLEANの証明エコシステム全体の検証を可能にする。
まず、FLEXはCHCを通常のLEAN命題としてエンコードし、Horn変数が存在的有界な述語であり、CHC命題のカーネルチェック可能な証明を計算する戦術(メタプログラム)としてCHCソルバを実装する方法を示している。
次に、命令型言語のためのFloyd-Hoareスタイルジェネレータと、関数型計算機のための改良型ジェネレータという2つの検証済みCHCジェネレータをLEANで実装する方法を示す。
最後に、FLEXは、LEANの証明機械のエコシステム全体を開放して、FLUXリファインメント型チェッカーを使用して様々な低レベルなRustライブラリの任意の機能正当性を証明し、FLUXのベンチマークスイートから自動的に95.7%のCHCを排出し、信頼性の高いCHCバックエンドとしてFLEXが実現可能であることを示すことによって、SMTの表現性限界を飛躍させる方法を示す。
関連論文リスト
- Evidence-Driven LLM Agent for C-to-Synthesizable-C Conversion and Verification [3.285367305212235]
Cプログラムは、高レベル合成(HLS)ツールチェーンの4段階のパイプラインを完了できない。
我々は,HLSツール上でのC-to-HLS-C変換をクローズドループ生成-検証-診断-修復問題として定式化する。
論文 参考訳（メタデータ） (2026-06-25T02:55:02Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
本稿では,学習モデルを一級数学的対象として扱うフレームワークであるTorchLeanを紹介する。
我々はTorchLeanのエンドツーエンドを、証明された堅牢性、PINNの物理インフォームド残差、Lyapunovスタイルのニューラルコントローラ検証で検証する。
論文 参考訳（メタデータ） (2026-02-26T05:11:44Z) - Plug-and-Play Benchmarking of Reinforcement Learning Algorithms for Large-Scale Flow Control [61.155940786140455]
強化学習(RL)は,アクティブフロー制御(AFC)において有望な結果を示した。
現在のAFCベンチマークは、外部計算流体力学(CFD)の解法に依存しており、完全には微分不可能であり、3Dとマルチエージェントのサポートが限られている。
AFCにおけるRLのための最初のスタンドアロンで完全に差別化可能なベンチマークスイートであるFluidGymを紹介する。
論文 参考訳（メタデータ） (2026-01-21T14:13:44Z) - CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses [0.0]
制約付きホーンクロース(CHC)は、検証タスクの中間表現として広く採用されている。
本稿では,CHCを解くためのソフトウェア検証アプローチを採用するポートフォリオベースのCHCソルバを紹介する。
論文 参考訳（メタデータ） (2025-10-30T12:25:06Z) - ImCoref-CeS: An Improved Lightweight Pipeline for Coreference Resolution with LLM-based Checker-Splitter Refinement [45.01372641622595]
InmCoref-CeSは,拡張教師付きモデルとLarge Language Models(LLM)ベースの推論を統合する新しいフレームワークである。
まず、教師付きニューラルネットワークの性能境界を押し上げる改良CR法(textbfImCoref)を提案する。
マルチロールチェッカースプリッターエージェントとして機能するLCMを用いて、候補参照とコア参照結果の検証を行う。
論文 参考訳（メタデータ） (2025-10-11T14:48:08Z) - Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
生成のための教師なし共形推論フレームワークを提案する。
我々のゲートは、分断されたUPPよりも厳密で安定した閾値を提供する。
その結果は、ラベルのない、API互換の、テスト時間フィルタリングのゲートになる。
論文 参考訳（メタデータ） (2025-09-26T23:40:47Z) - HALT-RAG: A Task-Adaptable Framework for Hallucination Detection with Calibrated NLI Ensembles and Abstention [0.0]
HALT-RAGは、Retrieval-Augmented Generationパイプラインの出力における幻覚を特定するために設計されたポストホック検証システムである。
我々のフレキシブルでタスク適応性のあるフレームワークは、2つのフリーズ・オフ・ザ・シェルフ自然言語推論(NLI)モデルと軽量語彙信号のアンサンブルから導かれる普遍的な特徴セットを使用する。
HALT-RAGは軽量・タスク適応型・高精度制約型決定ポリシーと組み合わせることで,要約,QA,対話における強いOOF F1スコア0.7756,0.9786,0.7391を達成する。
論文 参考訳（メタデータ） (2025-09-09T07:58:46Z) - Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning [7.574481956683386]
この研究は、新しいエンドツーエンド合成フレームワークであるProof2Siliconを提示する。
以前提案されたPreFACEフローを組み込んで、自然言語仕様から直接、正確性バイコンストラクションハードウェアを生成する。
論文 参考訳（メタデータ） (2025-09-07T23:04:15Z) - Rectified Diffusion Guidance for Conditional Generation [94.83538269086613]
CFGの背後にある理論を再検討し、不適切な組合せ係数(textiti.e.)が生成分布を期待的にシフトさせることを厳密に確認する。
提案手法は, 強みを考慮すれば, textbftextitform ソリューションが有効であることを示す。
実世界のデータに関する実証的な証拠は、我々の設計と既存の最先端拡散モデルとの整合性を実証している。
論文 参考訳（メタデータ） (2024-10-24T13:41:32Z) - General Cutting Planes for Bound-Propagation-Based Neural Network
Verification [144.7290035694459]
任意の切削平面制約を加えることができるような境界伝搬手順を一般化する。
MIPソルバは、境界プロパゲーションベースの検証器を強化するために高品質な切削面を生成することができる。
本手法は,oval20ベンチマークを完全解き,oval21ベンチマークの2倍のインスタンスを検証できる最初の検証器である。
論文 参考訳（メタデータ） (2022-08-11T10:31:28Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。