論文の概要: 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.18445v1
- Date: Wed, 19 Aug 2026 02:20:59 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-20 20:13:55.249538
- 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要約: ロマノフのトリプルト論理(TLS)の最初の機械的形式化をRocq証明アシスタントに提示する。
我々は、コンパクトトリプレット式(CTF)、CTS、ハイパー構造、クリアリング、SVIを含むTLSのコアをRocqで定式化する。
良好な形状のスライディングウインドウフラグメントに対しては,節ごとのCNF-チェーン変換,クリア処理,整列交点の検証を行う。
また,グループウィンドウ翻訳の音質を形式化し,その完全性に対して形式的な反例を示す。
- 参考スコア（独自算出の注目度）: 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 triplet-based combinatorial framework for reasoning about compatible paths through layered triplet structures, called Compact Triplets Structures (CTS), and their intersection via Romanov's Effective Procedure, which we refer to as Simple Vertex Intersection (SVI). Originally motivated by Boolean satisfiability, TLS constitutes a self-contained mathematical theory whose formal properties had not been previously established. We formalise the core of TLS in Rocq, including Compact Triplets Formulas (CTF), CTS, hyperstructures, clearing, and SVI. For the well-formed sliding-window fragment we verify a clause-by-clause CNF-to-CTF translation, the clearing procedure, and aligned intersection, and we prove explicit polynomial-time bounds for the filter stages. Our main contribution is a precise correctness boundary: the existence of a joint satisfying set implies non-emptiness of SVI, but the converse does not hold in general; for aligned structures we recover a complete bi-implication, extended to systems of structures. We also formalise soundness of grouped-window translation and exhibit a formal counterexample to its completeness. We introduce VFR, an extracted OCaml prototype that provides a verified decision procedure for the sliding-window fragment and a sound one-sided filter for general 3-CNF, with a Python runtime and reproducible Docker packaging. Benchmarks on random and structured instances confirm the predicted behaviour, and the complete toolchain is available as a curated Zenodo artifact. The Rocq development comprises more than 23,000 lines of code across seventeen files, with 427 proved lemmas and theorems and zero admitted goals.
- Abstract（参考訳）: ロマノフのトリプルト論理(TLS)の最初の機械的形式化をRocq証明アシスタントに提示する。
TLSは、三重項構造(CTS)と呼ばれる層状三重項構造と、ロマノフのエフェクト・プロシージャ(英語版)(SVI)によるそれらの交叉による相似経路の推論のための三重項ベースの組合せフレームワークである。
元々はブール充足性(Boolean satisfiability)に動機づけられたTLSは、形式的性質が以前に確立されていなかった自己完結型数学的理論を構成する。
我々は、コンパクトトリプレット式(CTF)、CTS、ハイパー構造、クリアリング、SVIを含むTLSのコアをRocqで定式化する。
良好な形状のスライディングウインドウフラグメントに対しては,節単位のCNF-to-CTF変換,クリーニング手順,アライメント交叉を検証し,フィルタ段の多項式時間境界を明示する。
結合満足集合の存在は SVI の空でないことを意味するが、逆は一般には成り立たない。
また,グループウィンドウ翻訳の音質を形式化し,その完全性に対して形式的な反例を示す。
我々は,Pythonランタイムと再現可能なDockerパッケージを備えた,スライドウインドウフラグメントの確定決定手順と,一般的な3CNFのためのサウンドワンサイドフィルタを提供する,抽出されたOCamlプロトタイプであるVFRを紹介する。
ランダムで構造化されたインスタンスのベンチマークは予測された振る舞いを確認し、完全なツールチェーンはZenodoアーティファクトとして利用できる。
Rocqの開発には17のファイルに23,000行以上のコードが含まれ、427の証明された補題と定理と0のゴールがある。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。