Proposition 3.7 - Perfect-feature LP-FT separation
ProvedFeatureDistortion.PerfectFeatureLPFTSeparationNotation: , is the input dimension, the feature dimension, the data map, the labels, the features, and the head. Adjoint means Euclidean transpose. The loss is , with no normalization. The probability model, when present, is explicitly specified below; deterministic flow statements involve no random data assumption.
For every triple of natural numbers , every choice of continuous real-linear maps and , real-linear isometric bijection , and , and every probability measure on with integrable squared norm and for every nonzero , where and , let , , , , , and . Assume , , , , , and injectivity on of both and , with denoting orthogonal projection. For every real , four assertions hold together. Here a fine-tuning pair from means functions and with , , and, at every real , derivatives within equal to and , the latter being a derivative in the space of continuous linear maps. A probing curve from means with and derivative within equal to at every real . The four assertions are: (1) for every there exists a fine-tuning pair from ; (2) for every there exists a probing curve from , and every probing curve from that tends to in the Euclidean topology as ; (3) for every fine-tuning pair from and every real , ; and (4) for almost every under the pushforward of standard Gaussian measure on by , every fine-tuning pair from that satisfies for every real . All adjoints are Euclidean. The exceptional null set in (4) is chosen before the universal quantifiers over pairs and times; this includes time zero and asserts positivity at each nonnegative real time, without a uniform positive lower bound or a statement about a limiting loss. The admissibility hypotheses exclude zero dimensions and require and . No conclusion is required for , and the curves have no conditions at negative times.
Formalization note: Source-derived Proposition 3.7 in the explicit nonzero-signal, identifiable perfect-feature regime, including flow existence and LP convergence. No uniform time-infimum, quantitative Theorem 3.3 constant, or imperfect-feature guarantee is claimed. Source: Kumar, Raghunathan, Jones, Ma, and Liang, Fine-Tuning can Distort Pretrained Features and Underperform Out-of-Distribution, ICLR 2022, https://arxiv.org/pdf/2202.10054v1. Section 3.4, PDF p. 10, Proposition 3.7, equations (3.10)--(3.11); Appendix A.7, PDF pp. 45--47, equations (A.208)--(A.218). Source-backed parent: Section 3.4, PDF p. 10, Proposition 3.7, equations (3.10)--(3.11); Appendix A.7, PDF pp. 45--47.
import Definitions.Def_FeatureDistortion_Model open MeasureTheory Filter open scoped Topology
namespace FeatureDistortion
theorem PerfectFeatureLPFTSeparation :
∀ (n d k : ℕ) (P : Problem n d k) (D : OODLaw d), Admissible P →
∀ σ : ℝ, 0 < σ →
(∀ v₀ : Vec k, ∃ γ : Trajectory d k,
IsFineTuningFlow P.data (labels P) v₀ (initialFeatures P) γ) ∧
(∀ v₀ : Vec k,
(∃ v : ℝ → Vec k, IsLinearProbingFlow P.data (labels P) v₀ (initialFeatures P) v) ∧
∀ v : ℝ → Vec k,
IsLinearProbingFlow P.data (labels P) v₀ (initialFeatures P) v →
Tendsto v atTop (𝓝 (alignedHead P))) ∧
(∀ γ : Trajectory d k,
IsFineTuningFlow P.data (labels P) (alignedHead P) (initialFeatures P) γ →
∀ t : ℝ, 0 ≤ t →
oodLoss D (targetWeights P) (γ.head t) (γ.features t) = 0) ∧
(∀ᵐ v₀ ∂gaussianHead k σ, ∀ γ : Trajectory d k,
IsFineTuningFlow P.data (labels P) v₀ (initialFeatures P) γ →
∀ t : ℝ, 0 ≤ t →
0 < oodLoss D (targetWeights P) (γ.head t) (γ.features t)) := by sorry
end FeatureDistortion
Read-back
What the Lean code literally says, in plain math · gpt-6
For every triple of natural numbers , every choice of continuous real-linear maps and , real-linear isometric bijection , and , and every probability measure on with integrable squared norm and for every nonzero , where and , let , , , , , and . Assume , , , , , and injectivity on of both and , with denoting orthogonal projection. For every real , four assertions hold together. Here a fine-tuning pair from means functions and with , , and, at every real , derivatives within equal to and , the latter being a derivative in the space of continuous linear maps. A probing curve from means with and derivative within equal to at every real . The four assertions are: (1) for every there exists a fine-tuning pair from ; (2) for every there exists a probing curve from , and every probing curve from that tends to in the Euclidean topology as ; (3) for every fine-tuning pair from and every real , ; and (4) for almost every under the pushforward of standard Gaussian measure on by , every fine-tuning pair from that satisfies for every real . All adjoints are Euclidean. The exceptional null set in (4) is chosen before the universal quantifiers over pairs and times; this includes time zero and asserts positivity at each nonnegative real time, without a uniform positive lower bound or a statement about a limiting loss. The admissibility hypotheses exclude zero dimensions and require and . No conclusion is required for , and the curves have no conditions at negative times.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.