論文の概要: Formal Verification of Romanov's Triplet Logic: A Verified Filter for Sliding-window 3-CNF with Application to Structured Formulas
- arxiv url: http://arxiv.org/abs/2608.18445v3
- Date: Tue, 25 Aug 2026 16:37:46 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-26 14:09:33.681323
- Title: Formal Verification of Romanov's Triplet Logic: A Verified Filter for Sliding-window 3-CNF with Application to Structured Formulas
- Title（参考訳）: ロマノフの三重項論理の形式的検証:スライディングウインドウ3CNFの検証フィルタと構造化公式への応用
- Authors: Dmitry V. Alexandrov,
- Abstract要約: Rocqの開発には23,000行以上のコードが含まれ、424の証明済みのsと未証明の仮定がない。
ロマノフのトリプルト論理(TLS)の最初の機械的形式化をRocq証明アシスタントに提示する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present the first mechanised formalisation of Romanov's Triplet Logic (TLS) in the Rocq proof assistant. TLS is a combinatorial framework originally motivated by Boolean satisfiability, based on triplet structures and a filter that we call Simple Vertex Intersection (SVI). We formalise the core of TLS, including its translation from 3-CNF, the clearing procedure, and the SVI algorithm. For the well-formed sliding-window fragment, we prove explicit polynomial-time bounds for the filter stages and verify the translation and intersection operations. Our main contribution is a precise correctness boundary: for general formulas, SVI non-emptiness is necessary but not sufficient for satisfiability; for aligned structures, we prove a full bi-implication, extended to systems of structures. We also formalise the grouped-window translation and provide a formal counterexample to its completeness. We introduce VFR (Verified Filter for Romanov's triplet logic), an extracted OCaml prototype that implements a verified decision procedure for the sliding-window fragment and a sound filter for general 3-CNF, with a Python runtime and Docker packaging. Benchmarks corroborate the predicted behaviour, and the complete toolchain is available as a curated Zenodo artifact. The Rocq development comprises over 23,000 lines of code, with 424 proved lemmas and no unproved assumptions.
- Abstract（参考訳）: ロマノフのトリプルト論理(TLS)の最初の機械的形式化をRocq証明アシスタントに提示する。
TLSは,3重構造とSVI(Simple Vertex Intersection)と呼ばれるフィルタをベースとした,ブール充足性(Boolean satisfiability)をモチベーションとした組合せフレームワークである。
我々はTLSのコアを3-CNFからの翻訳、クリアリング手順、SVIアルゴリズムを含む形式化する。
良好な形状のスライディングウインドウフラグメントに対して、フィルタ段に対する明示的な多項式時間境界を証明し、翻訳および交叉操作を検証する。
我々の主な貢献は正確な正当性境界であり、一般の式では、SVIの不空性は必要だが満足には十分ではない。
また,グループウィンドウ翻訳の形式化や,その完全性に対する公式な反例も提供する。
VFR(Verified Filter for Romanov's Threet logic)は,スライディングウィンドウフラグメントの確定決定手順を実装したOCamlプロトタイプであり,PythonランタイムとDockerパッケージを備えた一般的な3CNFのためのサウンドフィルタである。
ベンチマークは予測された振る舞いを相関付け、完全なツールチェーンはZenodoアーティファクトとして利用できる。
Rocqの開発には23,000行以上のコードが含まれ、424の証明された補題があり、未証明の仮定はない。
関連論文リスト
- Probing Structural Mathematical Reasoning in Language Models with Algebraic Trapdoors [0.0]
言語モデルにおける構造的数学的推論を評価するためのベンチマークスイートを提案する。
各インスタンスは有限生成された部分群を整数行列のリストとして提示する。
本稿では,2つの最先端モデルから得られた5つの代表的な推論指標について実験結果について報告する。
論文 参考訳（メタデータ） (2026-05-05T23:16:30Z) - Rethinking Reinforcement Fine-Tuning in LVLM: Convergence, Reward Decomposition, and Generalization [3.579200789027982]
RLVR(Reinforcement fine-tuning with verible rewards)は、大きな視覚言語モデル(LVLM)にツールの使用や多段階推論などのエージェント機能を持たせるための強力なパラダイムとして登場した。
顕著な経験的成功にもかかわらず、特に視覚エージェント強化細管(Visual Agentic Reinforcement Fine-Tuning, Visual-ARFT)は、このパラダイムの理論的基盤は理解されていない。
EmphTool-Augmented Markov Decision Process (TA-MDP)を導入する。
論文 参考訳（メタデータ） (2026-04-21T17:21:08Z) - TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
本稿では,学習モデルを一級数学的対象として扱うフレームワークであるTorchLeanを紹介する。
我々はTorchLeanのエンドツーエンドを、証明された堅牢性、PINNの物理インフォームド残差、Lyapunovスタイルのニューラルコントローラ検証で検証する。
論文 参考訳（メタデータ） (2026-02-26T05:11:44Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings [9.764411884491052]
ProofBridgeは、NLの定理と証明を自動的にリーン4に翻訳するフレームワークです。
中心となるのは、NL と FL (NL-FL) の定理対を共有意味空間で整列する合同埋め込みモデルである。
我々の訓練は、NL-FL 対が意味論的に同値である場合に限り、この空間において NL-FL の定理が密接にマッピングされることを保証する。
論文 参考訳（メタデータ） (2025-10-17T14:20:50Z) - Selmer-Inspired Elliptic Curve Generation [0.0]
楕円曲線暗号(ECC)は、現代のセキュア通信の基礎となっている。
既存の標準曲線は不透明なパラメータ生成プラクティスに対して精査されている。
この研究は、透明かつ監査可能な楕円曲線を構築するためのセルマーに着想を得たフレームワークを導入する。
論文 参考訳（メタデータ） (2025-09-30T17:33:36Z) - Fast and Accurate Blind Flexible Docking [79.88520988144442]
小分子(配位子)のタンパク質標的への結合構造を予測する分子ドッキングは、薬物発見において重要な役割を果たす。
本研究では,現実的な視覚的フレキシブルドッキングシナリオを対象とした,高速かつ高精度な回帰ベースマルチタスク学習モデルであるFABFlexを提案する。
論文 参考訳（メタデータ） (2025-02-20T07:31:13Z) - Squeezeformer: An Efficient Transformer for Automatic Speech Recognition [99.349598600887]
Conformerは、そのハイブリッドアテンション・コンボリューションアーキテクチャに基づいて、様々な下流音声タスクの事実上のバックボーンモデルである。
Squeezeformerモデルを提案する。これは、同じトレーニングスキームの下で、最先端のASRモデルよりも一貫して優れている。
論文 参考訳（メタデータ） (2022-06-02T06:06:29Z) - Fold2Seq: A Joint Sequence(1D)-Fold(3D) Embedding-based Generative Model
for Protein Design [70.27706384570723]
Fold2Seqは特定の標的に条件付きタンパク質配列を設計するための新しいフレームワークである。
Fold2Seqの性能は, シーケンス設計の速度, カバレッジ, 信頼性において向上したか, 同等であったかを示す。
フォールドベースのFold2Seqの独特な利点は、構造ベースのディープモデルやRosettaDesignと比較して、3つの現実世界の課題においてより明確になる。
論文 参考訳（メタデータ） (2021-06-24T14:34:24Z) - 3D Correspondence Grouping with Compatibility Features [51.869670613445685]
本稿では,3次元対応グルーピングのための簡易かつ効果的な手法を提案する。
目的は、局所幾何学的記述子を不整合と外接点にマッチングすることによって得られる初期対応を正確に分類することである。
本稿では,不整合と不整合を表わすために,互換性特徴(CF)と呼ばれる3次元対応の表現を提案する。
論文 参考訳（メタデータ） (2020-07-21T02:39:48Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。