Pipeline-generated

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.

✓ 1 result · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Reconstruction and masked autoencoders — Examples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

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.