Posts tagged #lean
-
Verified Security Gates: Safe ML Deserialization
Using Lean 4 soundness proofs to gate Python type-stub deserialization in the Falcon-secure project.
-
The Impossibility of Key-Only Routing: An Architectural Boundary
Formalizing why MoE routers must depend on residual-stream state rather than key-only summaries.
-
Formalizing the Softmax and Hessian: Lean 4 Soundness Proofs
A deep dive into the Lean 4 proofs for Softmax soundness and the BetaLocalHessian skeleton in the lean-mining project.
-
Multi-Head Foldability: Scaling Verified Compilation
Lifting single-head RoPE proofs to multi-head bundles and residual wrappers in the Verified Neural Compilation project.
-
The β-lift and FFN Transfer: MoE Compression Part E
Why β transfer in FFNs matters for quantization and the formal 'structure bonus' theorems in MoE compression.
-
Classifying the RoPE Commutant: Symmetry in Verified Neural Compilation
The algebra of which orthogonal transformations survive RoPE at zero cost, derived from the Symmetry.lean formalization.