論文の概要: Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline

• arxiv url: http://arxiv.org/abs/2604.18882v1
• Date: Mon, 20 Apr 2026 22:02:57 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-22 22:41:49.521034
• Title: Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline
• Title（参考訳）: 依存型理論による形式的検証された特許分析: ハイブリッドAI+リーン4パイプラインによるマシン管理可能な証明書
• Authors: George Koomullil,
• Abstract要約: 我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。 DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。 クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a formally verified framework for patent analysis as a hybrid AI + Lean 4 pipeline. The DAG-coverage core (Algorithm 1b) is fully machine-verified once bounded match scores are fixed. Freedom-to-operate, claim-construction sensitivity, cross-claim consistency, and doctrine-of-equivalents analyses are formalized at the specification level with kernel-checked candidate certificates. Existing patent-analysis approaches rely on manual expert analysis (slow, non-scalable) or ML/NLP methods (probabilistic, opaque, non-compositional). To our knowledge, this is the first framework that applies interactive theorem proving based on dependent type theory to intellectual property analysis. Claims are encoded as DAGs in Lean 4, match strengths as elements of a verified complete lattice, and confidence scores propagate through dependencies via proven-correct monotone functions. We formalize five IP use cases (patent-to-product mapping, freedom-to-operate, claim construction sensitivity, cross-claim consistency, doctrine of equivalents) via six algorithms. Structural lemmas, the coverage-core generator, and the closed-path identity coverage = W_cov are machine-verified in Lean 4. Higher-level theorems for the other use cases remain informal proof sketches, and their proof-generation functions are architecturally mitigated (untrusted generators whose outputs are kernel-checked and sorry-free axiom-audited). Guarantees are conditional on the ML layer: they certify mathematical correctness of computations downstream of ML scores, not the accuracy of the scores themselves. A case study on a synthetic memory-module claim demonstrates weighted coverage and construction-sensitivity analysis. Validation against adjudicated cases is future work.
• Abstract（参考訳）: 我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。 DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。 カーネルチェックされた候補証明書を用いて、フリーダム・トゥ・オペレーティング、クレーム・コンストラクションの感度、クロスステート・一貫性、ドクトリン・オブ・等価分析を仕様レベルで定式化する。 既存の特許分析手法は、手動の専門家分析(ゆっくりと、非スケーリング可能)やML/NLP法(確率的、不透明、非構成的)に依存している。 我々の知る限り、これは、依存型理論に基づく対話的定理証明を知的財産分析に適用する最初のフレームワークである。 クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。 我々は6つのアルゴリズムを用いて5つのIPユースケースを定式化する(Patent-to-product mapping,free-to-operate, claim construction sensitivity, cross-claim consistency, doctrine of equivalents)。 構造的な補題、カバレッジコアジェネレータ、クローズドパスのアイデンティティカバレッジ = W_covはLean 4.0でマシン検証されています。 他のユースケースの高次定理は非公式な証明スケッチのままであり、その証明生成関数はアーキテクチャ的に緩和されている(出力がカーネルチェックされ、無条件の公理が監査される信頼できない生成元)。 保証はML層上で条件付きであり、スコア自体の正確さではなく、MLスコアの下流で計算の数学的正しさを証明している。 合成メモリモジュールクレームのケーススタディでは、重み付きカバレッジと構成感度解析が示されている。 判決を受けた事件に対する検証は今後の作業である。

関連論文リスト

• Compliance-by-Construction Argument Graphs: Using Generative AI to Produce Evidence-Linked Formal Arguments for Certification-Grade Accountability [0.0]
  本稿では、生成AI(GenAI)と構造化された形式的引数表現を統合したコンプライアンス・バイ・コンストラクションアーキテクチャを提案する。 アーキテクチャは、各AI支援ステップを、検証済みの証拠によって支持され、明示的な推論制約に対して検証されなければならないクレームとして扱う。 この分析は、GenAIが議論構築を加速させながら、疑わしい主張が決定記録に入るのを防ぐことができることを示唆している。
  論文  参考訳（メタデータ） (2026-04-05T12:55:16Z)
• Decidable By Construction: Design-Time Verification for Trustworthy AI [0.0]
  機械学習における一般的な仮定は、モデル正しさは事実の後に強制されなければならないというものである。 我々は,AIモデルが数値的に安定しているか,計算的に正しいか,あるいは物理領域と整合しているかを決定する特性が,必ずしもポストホック強制を要求するとは限らないことを観察する。
  論文  参考訳（メタデータ） (2026-03-26T13:09:36Z)
• 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)
• Measuring Uncertainty in Transformer Circuits with Effective Information Consistency [0.0]
  本研究では,トランスフォーマー回路のシャーフ/コホモロジーと因果出現の視点を開発する。 EICSは(i)局所ジャコビアンとアクティベーションから計算された正規化棚の不整合と(ii)回路レベルの因果発生のためのガウスEIプロキシを組み合わせる。 本稿では,スコアの解釈,計算オーバーヘッド(高速かつ高精度なモード),およびおもちゃの健全性チェック分析に関する実践的ガイダンスを提供する。
  論文  参考訳（メタデータ） (2025-09-08T18:54:56Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  大規模言語モデル(LLM)は、コード解析と合成に成功している。 我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。 プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
  論文  参考訳（メタデータ） (2023-11-07T05:47:47Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。 しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。 本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-09-29T09:41:19Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。