ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A normalized-pixel objective with a constant representation

Example

Let $M = 2$ , $q = 2$ , $p_{0} = (0, 1 / 2)$ , and $p_{1} = (1 / 2, 1)$ . Consider two equally weighted images $X^{(0)} = (p_{0}, p_{0})$ and $X^{(1)} = (p_{1}, p_{1})$ with downstream labels $0$ and $1$ , respectively. Use one visible patch ( $k = 1$ ), the patchwise normalized-pixel target, an encoder returning the fixed token $z_{*} = 0 \in Z = R$ at every visible position, and a decoder that predicts $(- 1, 1)$ at each patch position for every input and mask. This model has masked reconstruction objective zero, although its representation cannot distinguish the two labels.

As a separate empirical example, He et al. report an ImageNet-1K ViT-L/16 run with random 75% masking, an eight-block decoder of width 512, an unnormalized-pixel target, random resized crops, and 800 pretraining epochs. Their Table 1 reports 84.9% top-1 validation accuracy (the fraction of validation images whose highest-scoring predicted class is correct) after 50-epoch supervised fine-tuning, measured on a single $224 \times 224$ crop; their Appendix A.1 gives the pretraining optimizer settings (AdamW, base learning rate $1.5 \times 10^{- 4}$ with the rule $l r = b a s e_l r \cdot b a t c h s i z e / 256$ , weight decay $0.05$ , momentum $(0.9, 0.95)$ , batch size $4096$ , cosine-decay schedule, and 40 warmup epochs). These are measurements for the reported data, architecture, and training protocol, not a theorem about other tasks or a semantic-sufficiency guarantee.

Example references

He et al., §3.3: normalized masked-patch target

He et al., §4/Table 1: ViT-L/16 ImageNet-1K ablation, masking ratio, pretraining length, and reported validation accuracy

He et al., Appendix A.1/Tables 8–9: pretraining and fine-tuning settings

Goodfellow et al., §14.5: general corruption-conditioned denoising objective

Vincent et al., §§2.2–2.3: finite reconstruction objective and corruption-conditioned clean target

Facts & Assumptions

Given: The training law assigns weight $1 / 2$ to each of $X^{(0)}$ and $X^{(1)}$ ; independently choose the visible set uniformly from ${{1}, {2}}$ . The target is $T_{n o r m}$ , the encoder is $E (V, (x_{j})_{j \in V}) = (z_{*})_{j \in V} \in Z^{V}$ with $z_{*} = 0$ and $Z = R$ , and the decoder returns $(- 1, 1)$ at both positions for every encoded sequence.

[F1]

Reconstruction autoencoder and denoising risk: for a patch with positive standard deviation, $T_{n o r m} (u) = (u - \overset{ˉ}{u} 1) / s (u)$ , and the masked-patch loss averages squared errors over positions in $[M] ∖ V$ .

[F2]

Masked autoencoder pretraining: the visible set is uniform among all size- $k$ subsets; the encoder sees only visible patches, while the decoder predicts every patch after mask tokens are inserted at missing positions.

[F3]

Expectation of a real random variable on a finite probability space: expectation on a finite probability space is the weighted sum of the values over its outcomes.

[F4]

Finite feedforward computation graphs and layered MLPs: each non-input vertex has a real bias, weights on its incoming edges, and an activation; in a layered MLP the output vertices use the identity activation.

Verification

1.1givenF1algebra

For $p_{0}$ , the mean is $1 / 4$ and the standard deviation is $1 / 4$ ; for $p_{1}$ , they are $3 / 4$ and $1 / 4$ . Hence [F1] gives $T_{n o r m} (p_{0}) = (- 1, 1) = T_{n o r m} (p_{1})$ .

1.2givenF1F2F3algebra

Both patches of either image have this same normalized target. By [F2], each mask leaves exactly one masked patch, and the decoder predicts $(- 1, 1)$ there. Its squared error is zero, so the per-example loss [F1] is zero for every image-mask outcome. The finite expectation [F3] is therefore zero.

2.1givenF4algebra∎

For each fixed visible set $V$ , the encoder returns the identical indexed token family $(z_{*})_{j \in V}$ for both differently labelled images. Any deterministic classifier applied only to this representation has the same output on both images at that $V$ , so it cannot classify both labels correctly. Allowing the classifier to use $V$ does not change this conclusion, since $V$ is independent of the equally weighted label. The constant token map and decoder are permitted finite feedforward maps by [F4], taking zero incoming weights, identity output activations, and fixed biases.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Kaiming He, Xinlei Chen, Saining Xie, Yanghao Li, Piotr Dollár, and Ross Girshick, Masked Autoencoders Are Scalable Vision Learners, §3.3, §4/Table 1, and Appendix A.1/Tables 8–9 (standard reference, not scraped)
Ian Goodfellow, Yoshua Bengio, and Aaron Courville, Deep Learning, §14.5 (standard reference, not scraped)
Pascal Vincent, Hugo Larochelle, Yoshua Bengio, and Pierre-Antoine Manzagol, Extracting and Composing Robust Features with Denoising Autoencoders, §§2.2–2.3 (standard reference, not scraped)