A Lean 4 system models patent claims as DAGs with match scores in a verified complete lattice and supplies kernel-checked certificates for coverage calculations and five IP use cases, conditional on unverified ML inputs.
Systematic design of program analysis frameworks
5 Pith papers cite this work. Polarity classification is still indexing.
5
Pith papers citing it
verdicts
UNVERDICTED 5representative citing papers
Agentic interpretation uses lattices to track LLM judgments on decomposed program claims during analysis.
A new abstract interpretation algorithm enables sound optimistic analysis of e-graphs during equality saturation, unifying it with non-destructive rewriting and improving precision on cyclic SSA programs.
SAQR-QC is a new logic for scalable approximate quantitative reasoning about quantum circuits via local qubit operations and controlled precision loss, demonstrated on GHZ circuits and quantum phase estimation.
Presents sound abstract interpretation plus controlled unsoundness techniques to produce tighter, efficient, terminating approximations of fixed points for non-monotone processes.
citing papers explorer
-
Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline
A Lean 4 system models patent claims as DAGs with match scores in a verified complete lattice and supplies kernel-checked certificates for coverage calculations and five IP use cases, conditional on unverified ML inputs.
-
Agentic Interpretation: Lattice-Structured Evidence for LLM-Based Program Analysis
Agentic interpretation uses lattices to track LLM judgments on decomposed program claims during analysis.
-
Optimism in Equality Saturation
A new abstract interpretation algorithm enables sound optimistic analysis of e-graphs during equality saturation, unifying it with non-destructive rewriting and improving precision on cyclic SSA programs.
-
SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
SAQR-QC is a new logic for scalable approximate quantitative reasoning about quantum circuits via local qubit operations and controlled precision loss, demonstrated on GHZ circuits and quantum phase estimation.
-
Bounding Fixed Points of Non-Monotone Processes: Theory to Practice
Presents sound abstract interpretation plus controlled unsoundness techniques to produce tighter, efficient, terminating approximations of fixed points for non-monotone processes.