Alphabeta Math
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 · 1 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; all 1 also cleared it.

Multimodal contrastive alignment and transfer — Examples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Prompt and distribution-sensitive transfer

Example

Use R2 with e1=(1,0), e2=(0,1), ⟨(a,b),(c,d)⟩=ac+bd, and scale s>0. For one image x with normalized image embedding u=e1, consider classes A,B and two prompt templates. Under the first wording, their normalized text embeddings are vA1=e1, vA2=e2, and vB1=vB2=qB=(4/5,3/5). Embedding-space prompt averaging gives qA=(1/2,1/2) and qB=(4/5,3/5). The class-prototype classifier scores s/2 for A and 4s/5 for B. Define individual-text retrieval here to rank the four prompt embeddings by their dot product with u; it selects the first A prompt, while the class-prototype classifier selects B. If a second prompt wording gives both A prompts embedding e1 and leaves the B prompts unchanged, then the classifier selects A. These are possible encoder outputs, demonstrating that prompt wording and the candidate construction can change the result.

For a second fixed zero-shot classifier, let the normalized class prototypes be qA=e1 and qB=e2, and let two distinct images x0≠x1 both have normalized image embedding e1. Give them the fixed true labels A and B, respectively, so the classifier predicts A for both. Let dA,dB be class-specific descriptions: dA is true of A and false of B, while dB is true of B and false of A; their normalized text embeddings are qA,qB. The B image x1 paired with the incorrect A description dA is semantically mismatched but has cosine similarity 1; paired with its correct B description dB, it has cosine similarity 0. Thus this construction shows that the embeddings need not preserve semantic compatibility. Define the finite source evaluation law by assigning mass 3/4 to (x0,A) and 1/4 to (x1,B), and the target evaluation law by assigning mass 1/4 to (x0,A) and 3/4 to (x1,B). The label assigned to each image is the same under both laws, while the input frequencies differ. Define 0–1 error under either law as the total mass of its misclassified labelled inputs. The errors are 1/4 on the source law and 3/4 on the target law, illustrating input-distribution sensitivity for this fixed classifier.

The vector geometry in the first construction is shown schematically below: the horizontal component is the similarity with the image embedding e1. The exact coordinates above determine the rankings; no proof relies on the drawing.

diagram failed to render:
\begin{tikzpicture}[x=2.3cm,y=2.3cm,>=stealth]
  \draw[->] (-0.08,0) -- (1.18,0) node[right] {$e_1$};
  \draw[->] (0,-0.08) -- (0,1.16) node[above] {$e_2$};
  \draw[->,thick] (0,0) -- (1,0) node[below right] {$u=v_{A1}$};
  \draw[->,dashed] (0,0) -- (0,1) node[left] {$v_{A2}$};
  \draw[->,thick] (0,0) -- (0.707,0.707) node[above left] {$q_A$};
  \draw[->,thick] (0,0) -- (0.8,0.6) node[above right] {$q_B$};
\end{tikzpicture}

As separate empirical context, Radford et al. trained CLIP on 400 million WebImageText image/text pairs. Unless otherwise specified, their reported “CLIP” results use ViT-L/14@336px, trained for 32 epochs with one additional high-resolution epoch. On their 27-dataset suite, zero-shot CLIP outperformed a regularized logistic-regression classifier on ResNet-50 features on 16 datasets. Their default “A photo of a {label}” prompt improved ImageNet accuracy by 1.3%, and ensembling 80 prompts added a further 3.5 percentage points over that default. These are measured outcomes under the paper's data, models, training, evaluation suite, and prompt choices.

In §3.3, the authors report that zero-shot CLIP improved effective robustness relative to ImageNet models across seven natural distribution shifts, reducing the robustness gap by up to 75%. Their dataset-specific class prompts increased average effective robustness by 5%, with gains concentrated on a few datasets. They caution that these results do not isolate the cause of the robustness gap and that pretraining and evaluation distributions may share spurious correlations.

In §5, the authors report median detected overlap of 2.2% and mean overlap of 3.2% across 35 evaluation datasets; only seven datasets had an overall accuracy change above 0.1%, and the largest detected increase was 0.6% on Birdsnap. They also state that detector recall could not be checked across all 400 million training pairs and that the Overlap and Clean subsets could differ in distribution or difficulty. Section 6 notes that the benchmark suite was partly co-adapted through repeated validation-set queries and reports weak results on fine-grained, systematic, novel, and truly out-of-distribution tasks. These results and limitations supply no general guarantee of transfer, out-of-distribution accuracy, reasoning, fairness, or semantic alignment.

Facts & Assumptions

Given: The two finite embedding setups, the class descriptions with their stated meanings, the source/target evaluation laws, a positive scale s, and the specified individual-text retrieval and finite 0–1 error rules. Verify the prompt-dependent classifier outputs, the retrieval/classification difference, the semantic-pair similarity contrast, and both finite error values.

[F1]

Zero-shot prompt classification: For each class, normalize each prompt embedding, average and renormalize those vectors to form a prototype, score it by the scaled inner product with the normalized image embedding, and return the least-index class maximizing the score.

[A1]

In the first setup, u=e1, vA1=e1, vA2=e2, and vB1=vB2=(4/5,3/5). Under the alternate wording, vA1=vA2=e1 and the B vectors remain unchanged. Retrieval ranks the four individual prompt embeddings by inner product with u.

[A2]

In the second setup, x0≠x1, qA=e1, qB=e2, u(x0)=u(x1)=e1, and the fixed labels are y(x0)=A, y(x1)=B. The source law places masses 3/4,1/4 on (x0,A),(x1,B), and the target law places masses 1/4,3/4 on those same labeled inputs. Error is the total mass assigned to misclassified inputs.

[A3]

The class-specific descriptions dA,dB are true only of classes A,B, respectively, among these two classes, and their normalized text embeddings are qA=e1 and qB=e2.

Verification

Given: The two finite embedding setups, the class descriptions with their stated meanings, the source/target evaluation laws, a positive scale s, and the specified individual-text retrieval and finite 0–1 error rules. Verify the prompt-dependent classifier outputs, the retrieval/classification difference, the semantic-pair similarity contrast, and both finite error values.

1.1givenF1A1algebra

Under the first wording, the normalized mean of e1 and e2 is qA=(1/2,1/2), while the two B prompts average to qB=(4/5,3/5).

1.2givenF1A1algebra

Under the alternate wording, the A prototype is e1 and the B prototype remains (4/5,3/5), giving scores s and 4s/5. Thus the same image is classified as A after the prompt change.

1.3givenF1A2algebra

In the second setup both image embeddings equal e1, so their scores against (qA,qB)=(e1,e2) are (s,0) and the classifier predicts A on both images. It is correct on x0 and incorrect on x1.

2.1givenF1A1step 1.1algebra

Their scores are zA=s/2 and zB=4s/5. Since both sides are positive and (4/5)2=16/25>1/2=(1/2)2, zB>zA, so the class-prototype classifier returns B.

2.2givenA2step 1.3algebra

Since x0≠x1, the source law gives input mass 3/4 to x0 and the target law gives it 1/4, with the reverse masses at x1; the label assigned to each image is fixed. The only error atom has source mass 1/4 and target mass 3/4. Therefore the source and target errors are 1/4 and 3/4, respectively, with difference 1/2.

3.1givenA1step 2.1algebra

The individual retrieval dot products are 1,0,4/5,4/5. Since 1>4/5, retrieval returns the first A prompt, unlike the class-prototype classifier.

4.1givenA2A3algebra∎

By [A2] and [A3], x1 is a B image and dA is false of B, so (x1,dA) is semantically mismatched. The stated inner-product formula ⟨(a,b),(c,d)⟩=ac+bd gives similarity 1 for (x1,dA) and 0 for the matched pair (x1,dB).

Sources