pith. machine review for the scientific record. sign in

arxiv: 2604.18882 · v1 · submitted 2026-04-20 · 💻 cs.AI · cs.LO· cs.PL

Recognition: unknown

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

George Koomullil
Authors on Pith no claims yet

Pith reviewed 2026-05-10 03:55 UTC · model grok-4.3

classification 💻 cs.AI cs.LOcs.PL
keywords patent analysisformal verificationLean 4dependent type theoryintellectual propertyDAG coveragemachine learningtheorem proving
0
0 comments X

The pith

A Lean 4 pipeline produces machine-checkable certificates for patent claim coverage once ML scores are fixed.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper builds a hybrid system that feeds machine learning match scores into formally verified algorithms written in Lean 4. Patent claims are represented as directed acyclic graphs, match strengths live in a complete lattice, and coverage is computed by monotone functions whose properties are kernel-checked. The central DAG-coverage algorithm, its structural lemmas, and the identity that coverage equals weighted coverage are fully machine-verified. Five standard intellectual-property tasks are given specification-level formalizations, with the core coverage step carrying machine-checked certificates. Higher-level proofs remain sketches, and all guarantees stop at the boundary of the supplied ML scores.

Core claim

The DAG-coverage core algorithm is fully machine-verified in Lean 4 once bounded match scores are supplied. Claims are encoded as DAGs, match strengths as elements of a verified complete lattice, and scores propagate through dependencies via proven-correct monotone functions. Structural lemmas, the coverage-core generator, and the closed-path identity coverage = W_cov are kernel-checked; the five IP use cases are formalized at the specification level with candidate certificates.

What carries the argument

The coverage-core generator and monotone score-propagation functions over claim DAGs in Lean 4's dependent type theory.

If this is right

  • Freedom-to-operate and claim-construction sensitivity analyses receive kernel-checked certificates.
  • Cross-claim consistency and doctrine-of-equivalents mappings become certifiable downstream of the scores.
  • Patent-to-product mapping inherits proven-correct weighted coverage calculations.
  • All five formalized use cases share the same machine-verified coverage core.
  • Untrusted proof generators for higher-level theorems are architecturally isolated by kernel checking and axiom auditing.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same verified lattice and monotone propagation pattern could be reused for other claim-interpretation tasks outside patents.
  • Any future integration with actual ML models must include explicit bounds on score outputs to keep the certificates valid.
  • Completing the informal proof sketches for the remaining use cases would turn the current specification-level formalizations into fully machine-checked theorems.
  • The approach suggests a general route for making AI-assisted legal reasoning auditable without requiring the ML component itself to be verified.

Load-bearing premise

The machine learning match scores are treated as fixed and bounded inputs, so verification applies only to the computations that follow them.

What would settle it

A concrete Lean 4 counterexample in which the verified coverage computation on a known claim DAG produces a result that violates the closed-path identity coverage equals W_cov.

Figures

Figures reproduced from arXiv: 2604.18882 by George Koomullil.

Figure 1
Figure 1. Figure 1: Hybrid ML + Formal Verification Pipeline Architecture. The trust boundary [PITH_FULL_IMAGE:figures/full_fig_p021_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Claim dependency DAG for a memory module patent. Node colors represent [PITH_FULL_IMAGE:figures/full_fig_p025_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: (a) The complete lattice [0, 1] with meet and join. (b) Weakest-link sensitivity analysis using the meet-based claimStrength model (Definition 5.2): a schematic DAG in which a node’s low score of 0.45 propagates through the dependency chain, bounding nodes that transitively depend on it. The “C12” label in panel (b) is a schematic node name that happens to reuse the same letter/number pattern as the memory… view at source ↗
Figure 4
Figure 4. Figure 4: Proof certificate generation and independent verification. The analysis system [PITH_FULL_IMAGE:figures/full_fig_p031_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: FTO proof construction flow. Strategy 1 (current implementation): if any element’s best match score falls below threshold, the algorithm returns Clear with a non￾infringement certificate; otherwise it returns Risk with a gap analysis. Strategy 2 (the dependency-chain branch shown in the figure) is a planned future extension, not current behavior; it would handle the case where per-element scores all clear … view at source ↗
Figure 6
Figure 6. Figure 6: Claim construction sensitivity analysis for the memory module patent (C1–C15). [PITH_FULL_IMAGE:figures/full_fig_p050_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Five IP analysis use cases enabled by formal verification. For UC1 (Algorithm [PITH_FULL_IMAGE:figures/full_fig_p063_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: illustrates the asymptotic scaling shapes implied by the complexity classes in [PITH_FULL_IMAGE:figures/full_fig_p069_8.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper claims to present the first formally verified framework for patent analysis using a hybrid AI + Lean 4 pipeline based on dependent type theory. Claims are encoded as DAGs, match strengths as elements of a verified complete lattice, and confidence scores propagate via proven-correct monotone functions. The DAG-coverage core (Algorithm 1b), structural lemmas, coverage-core generator, and closed-path identity (coverage = W_cov) are machine-verified in Lean 4; five IP use cases (patent-to-product mapping, freedom-to-operate, claim-construction sensitivity, cross-claim consistency, doctrine of equivalents) are formalized at the specification level with kernel-checked candidate certificates. Higher-level theorems remain informal proof sketches, guarantees are conditional on bounded ML scores, and a synthetic memory-module case study is provided, with real-data validation noted as future work.

Significance. If the verified components hold, this is the first application of interactive theorem proving in dependent type theory to intellectual property analysis, supplying machine-checkable certificates where existing methods are manual or probabilistic. The kernel-checked proofs for the DAG-coverage core and closed-path identity are clear strengths that demonstrate the feasibility of compositional formal verification in this domain. Practical significance is tempered by the explicit conditioning on ML accuracy and the use of synthetic rather than adjudicated data.

major comments (1)
  1. Abstract: The claim that five IP use cases are formalized via six algorithms is immediately qualified by the statement that higher-level theorems remain informal proof sketches. Because the title and abstract position the work as a 'formally verified framework,' this distinction between the machine-verified DAG-coverage core and the sketched use-case theorems should be stated more prominently to accurately delimit the verified scope.
minor comments (2)
  1. The propagation of confidence scores through monotone functions on the complete lattice is described at a high level; an explicit reference to the Lean 4 definition or a small illustrative derivation would improve readability without altering the technical content.
  2. Case study section: The synthetic memory-module claim is used to demonstrate weighted coverage and construction-sensitivity analysis, but the DAG structure, node labels, and numerical coverage values are not shown; including these would allow readers to verify the claimed outputs directly.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for this constructive observation on the abstract. We agree that the distinction between the machine-verified core and the informal sketches for higher-level theorems merits more prominent placement to avoid any risk of overstating the verified scope.

read point-by-point responses

  1. Referee: Abstract: The claim that five IP use cases are formalized via six algorithms is immediately qualified by the statement that higher-level theorems remain informal proof sketches. Because the title and abstract position the work as a 'formally verified framework,' this distinction between the machine-verified DAG-coverage core and the sketched use-case theorems should be stated more prominently to accurately delimit the verified scope.

    Authors: We accept the referee's point. Although the current abstract already notes that 'Higher-level theorems for the other use cases remain informal proof sketches,' we will revise the abstract to state this distinction more explicitly and earlier in the text. The revised wording will clearly separate the fully kernel-checked DAG-coverage core (Algorithm 1b, structural lemmas, coverage-core generator, and closed-path identity) from the specification-level formalization and kernel-checked candidate certificates provided for the five IP use cases, while retaining the accurate description of the overall hybrid pipeline. This change will better align the abstract with the paper's actual verified content without altering any technical claims. revision: yes

Circularity Check

0 steps flagged

No significant circularity; verification is externally grounded

full rationale

The paper's derivation chain centers on machine-checked Lean 4 proofs for the DAG-coverage core (Algorithm 1b), structural lemmas, the coverage-core generator, and the closed-path identity (coverage = W_cov). These are presented as kernel-verified under the explicit precondition that match scores are bounded elements of a verified complete lattice, with ML scores treated as fixed external inputs rather than fitted parameters. Higher-level theorems are explicitly scoped as informal sketches with architecturally mitigated generators. No equations reduce outputs to inputs by construction, no self-citations are load-bearing, and no ansatzes or uniqueness claims are smuggled in. The argument is self-contained against the external Lean 4 kernel and stated boundaries.

Axiom & Free-Parameter Ledger

1 free parameters · 2 axioms · 1 invented entities

The framework rests on modeling patent claims as DAGs and match strengths as a complete lattice whose operations are proven monotone. The ML-derived scores are treated as fixed external inputs. Dependent type theory soundness is assumed from the Lean 4 kernel.

free parameters (1)
  • bounded match scores
    The verification holds only once these scores (produced by the untrusted ML layer) are supplied as fixed inputs; their values are not derived inside the formal system.
axioms (2)
  • standard math Soundness of the Lean 4 kernel for dependent type theory
    All machine-checked certificates rely on the correctness of Lean's type checker.
  • domain assumption Patent claims can be faithfully encoded as directed acyclic graphs
    The DAG representation is introduced as the basis for coverage calculations.
invented entities (1)
  • DAG-coverage core (Algorithm 1b) no independent evidence
    purpose: To compute weighted coverage with kernel-checked structural lemmas
    New modeling artifact that turns claim matching into a verified lattice computation.

pith-pipeline@v0.9.0 · 5594 in / 1672 out tokens · 62353 ms · 2026-05-10T03:55:53.619068+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

32 extracted references · 18 canonical work pages

  1. [1]

    DAPFAM: A Domain-Aware Family-level Dataset to Benchmark Cross-Domain Patent Retrieval,

    Iliass Ayaou et al. DAPFAM: A domain-aware family-level dataset to benchmark cross-domain patent retrieval.arXiv preprint arXiv:2506.22141, 2025. URLhttps: //arxiv.org/abs/2506.22141

    work page arXiv 2025

  2. [2]

    The challenge of computer mathematics.Philo- sophical Transactions of the Royal Society A, 363(1835):2351–2375, 2005

    Henk Barendregt and Freek Wiedijk. The challenge of computer mathematics.Philo- sophical Transactions of the Royal Society A, 363(1835):2351–2375, 2005. doi: 10.1098/rsta.2005.1650

    work page doi:10.1098/rsta.2005.1650 2005

  3. [3]

    LogiKEyworkbench: Deontic logics, logic combinations and expressive ethical and legal reasoning.Science of Computer Programming, 196:102499, 2020

    ChristophBenzmüller,XavierParent,andLeendertvanderTorre. LogiKEyworkbench: Deontic logics, logic combinations and expressive ethical and legal reasoning.Science of Computer Programming, 196:102499, 2020. doi: 10.1016/j.scico.2020.102499

    work page doi:10.1016/j.scico.2020.102499 2020

  4. [4]

    Lean4Lean: VerifyingatypecheckerforLean, inLean.arXivpreprint arXiv:2403.14064, 2024

    MarioCarneiro. Lean4Lean: VerifyingatypecheckerforLean, inLean.arXivpreprint arXiv:2403.14064, 2024. URLhttps://arxiv.org/abs/2403.14064

    work page arXiv 2024

  5. [5]

    NLP verification: Towards a general methodology for certifying robustness.arXivpreprintarXiv:2403.10144,2024

    Marco Casadio et al. NLP verification: Towards a general methodology for certifying robustness.arXivpreprintarXiv:2403.10144,2024. URL https://arxiv.org/abs/ 2403.10144

    work page arXiv 2024

  6. [6]

    Towards trustworthy legal AI through LLM agents and formal reasoning.arXiv preprint arXiv:2511.21033, 2025

    Linze Chen et al. Towards trustworthy legal AI through LLM agents and formal reasoning.arXiv preprint arXiv:2511.21033, 2025. URLhttps://arxiv.org/abs/ 2511.21033

    work page arXiv 2025

  7. [7]

    In: Aho, A.V., Zilles, S.N., Rosen, B.K

    Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. InProceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 269–282, 1979. doi: 10.1145/567752.567778

    work page doi:10.1145/567752.567778 1979

  8. [8]

    Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, and Andrew Wells. Cedar: A new language for expressive, fast, safe, and analyzable authorization. Proceedings of the ACM on Programm...

    work page doi:10.1145/3649835 2024

  9. [9]

    Daubert v

    Daubert. Daubert v. Merrell Dow Pharmaceuticals, Inc. 509 U.S. 579 (1993), 1993. URLhttps://supreme.justia.com/cases/federal/us/509/579/

    1993

  10. [10]

    In: Automated Deduction – CADE 28: 28th International Conference on Auto- mated Deduction, Virtual Event, July 12–15, 2021, Proceedings, pp

    LeonardodeMouraandSebastianUllrich. TheLean4theoremproverandprogramming language. InAutomated Deduction – CADE 28, volume 12699 ofLecture Notes in Computer Science, pages 625–635. Springer, 2021. doi: 10.1007/978-3-030-79876-5_ 37

    work page doi:10.1007/978-3-030-79876-5_ 2021

  11. [11]

    A faster algorithm for finding Tarski fixed points.arXiv preprint arXiv:2010.02618, 2020

    John Fearnley, Dömötör Pałvolölgyi, and Rahul Savani. A faster algorithm for finding Tarski fixed points.arXiv preprint arXiv:2010.02618, 2020. URLhttps: //arxiv.org/abs/2010.02618. 88

    work page arXiv 2010

  12. [12]

    Festo Corp

    Festo. Festo Corp. v. Shoketsu Kinzoku Kogyo Kabushiki Co. 535 U.S. 722 (2002),

    2002

  13. [13]

    URLhttps://supreme.justia.com/cases/federal/us/535/722/

  14. [14]

    Beyond scaling: Predicting patent approval with domain-specific fine-grained claim dependency graph.arXiv preprint arXiv:2404.14372, 2024

    Xiaochen Gao et al. Beyond scaling: Predicting patent approval with domain-specific fine-grained claim dependency graph.arXiv preprint arXiv:2404.14372, 2024. URL https://arxiv.org/abs/2404.14372

    work page arXiv 2024

  15. [15]

    Graver Tank & Mfg

    Graver Tank. Graver Tank & Mfg. Co. v. Linde Air Prods. Co. 339 U.S. 605 (1950),

    1950

  16. [16]

    URLhttps://supreme.justia.com/cases/federal/us/339/605/

  17. [17]

    Programming languages and law: A research agenda.arXiv preprint arXiv:2206.14879, 2022

    James Grimmelmann. Programming languages and law: A research agenda.arXiv preprint arXiv:2206.14879, 2022. URLhttps://arxiv.org/abs/2206.14879

    work page arXiv 2022

  18. [18]

    Verified AI reasoning with Lean 4.https://harmonic.fun, 2025

    Harmonic AI. Verified AI reasoning with Lean 4.https://harmonic.fun, 2025. Accessed 2026-04-19

    2025

  19. [19]

    Johnson & Johnston Assocs

    Johnson & Johnston. Johnson & Johnston Assocs. Inc. v. R.E. Serv. Co. 285 F.3d 1046 (Fed. Cir. 2002), 2002. URLhttps://law.justia.com/cases/federal/ appellate-courts/F3/285/1046/570109/

    2002

  20. [20]

    Sarah B. Lawsky. A logic for statutes.Florida Tax Review, 21(1):60–116, 2018. URL https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3088206

    2018

  21. [21]

    Jeffrey A. Lefstin. The formal structure of patent law and the limits of enablement. BerkeleyTechnologyLawJournal,23(4):1141–1226,2008.URL https://btlj.org/ data/articles2015/vol23/23_4/23-berkeley-tech-l-j-1141-1226.pdf

    2008

  22. [22]

    Catala: A programming language for the law.Proceedings of the ACM on Programming Languages, 5(ICFP): 77:1–77:29, 2021

    Denis Merigoux, Nicolas Chataing, and Jonathan Protzenko. Catala: A programming language for the law.Proceedings of the ACM on Programming Languages, 5(ICFP): 77:1–77:29, 2021. doi: 10.1145/3473582. URLhttps://arxiv.org/abs/2103. 03198

    work page doi:10.1145/3473582 2021

  23. [23]

    Phillips v

    Phillips. Phillips v. AWH Corp. 415 F.3d 1303 (Fed. Cir. 2005), 2005. URL https://www.law.berkeley.edu/files/Phillips_v_AWH.pdf

    2005

  24. [24]

    Pitney Bowes, Inc

    Pitney Bowes. Pitney Bowes, Inc. v. Hewlett-Packard Co. 182 F.3d 1298 (Fed. Cir. 1999), 1999

    1999

  25. [25]

    Contributions to modeling patent claims when drafting patent applications

    Simone Reis, Andre Reis, Jordi Carrabina, and Pompeu Casanovas. Contributions to modeling patent claims when drafting patent applications. InAI Approaches to the Complexity of Legal Systems (AICOL-VI), volume 10791 ofLecture Notes in Computer Science, pages 135–149. Springer, 2018. doi: 10.1007/978-3-030-00178-0_9

    work page doi:10.1007/978-3-030-00178-0_9 2018

  26. [26]

    PatentMatch: A Dataset for Matching Patent Claims & Prior Art,

    JulianRisch,NicolasAlder,ChristophHewel,andRalfKrestel. PatentMatch: Adataset for matching patent claims and prior art.arXiv preprint arXiv:2012.13919, 2020. URL https://arxiv.org/abs/2012.13919. 89

    work page arXiv 2012

  27. [27]

    DSLean: A framework for type-correct interoperability between Lean 4 and external DSLs.arXiv preprint arXiv:2602.18657, 2026

    Tate Rowney et al. DSLean: A framework for type-correct interoperability between Lean 4 and external DSLs.arXiv preprint arXiv:2602.18657, 2026. URLhttps: //arxiv.org/abs/2602.18657

    work page arXiv 2026

  28. [28]

    Chudziak

    Albert Sadowski and Jaroslaw A. Chudziak. On verifiable legal reasoning: A multi-agent framework with formalized knowledge representations.arXiv preprint arXiv:2509.00710, 2025. URLhttps://arxiv.org/abs/2509.00710

    work page arXiv 2025

  29. [29]

    The Mathlib4 mathematics library for Lean 4.https: //github.com/leanprover-community/mathlib4, 2025

    The Mathlib Community. The Mathlib4 mathematics library for Lean 4.https: //github.com/leanprover-community/mathlib4, 2025. Accessed 2026-04-19

    2025

  30. [30]

    Warner-JenkinsonCo.v.HiltonDavisChem.Co

    Warner-Jenkinson. Warner-JenkinsonCo.v.HiltonDavisChem.Co. 520U.S.17(1997),

    1997

  31. [31]

    URLhttps://supreme.justia.com/cases/federal/us/520/17/

  32. [32]

    first number of ranks

    Yongmin Yoo et al. PatentScore: Multi-dimensional evaluation of LLM-generated patent claims.arXiv preprint arXiv:2505.19345, 2025. URLhttps://arxiv.org/ abs/2505.19345. A Lean 4 Formalization Details A.1 Complete Lattice Instance The implementation represents match strengths using Lean 4’s rational arithmetic rather than hardware floating-point, because L...

    work page arXiv 2025