Opening · Scientific engineering deck

Adaptive Visual Context

From CARES Research to a Verified Agent Workflow

A rigorous bridge from query-conditioned resolution research to deterministic tooling, executable scientific checks, and narrowly scoped Lean proofs.

Daniel Liezrowice

Presenter · Engineering Software Lab
ESL — AI SDLC Consultants

Research attribution

CARES — Kimhi, Shabtay, Giryes, Baskin & Schwartz (2025)
arXiv:2510.19496v3

Independent Apache-2.0 implementation · not affiliated with or endorsed by CARES authors.

← Swipe to navigate →

Research

Executive scientific thesis

r* = π(x, q) — not π(x) alone

Conditioning changes allocation

The same pixels can require different evidence. “Summarize layout” may tolerate a proxy; “read CVE-2026-…” may require an exact crop. Resolution is conditioned jointly on image x and query q.

Policy π(x,q)

Image x + query q → allocate the least visual context sufficient for the objective: resolution, crop, and token budget.

Foundations

VLM pipeline — where visual cost enters

pixels
H×W

→

vision encoder
patch tokens

→

projector
bridge

→

LLM decoder
self-attention

→

answer
G tokens

T = Q + V + G

Ω_decoder ≈ 2s²h + 12sh²

Increasing V raises attention-like s²h and projection/MLP-like sh² work. Pixel count is only a proxy; tokenization and latency are target-model specific.

Foundations · Project-generated figure

Why visual tokens dominate

Chart of visual-token dominance by model and resolution

At 4096 px

Qwen: 21,609 visual tokens (99.54% with 100 text)
InternVL: 10,496 (99.06%)
AnyRes analytic cap: 2,880 (96.64%)

share_visual = V / (V + Q)

Analytic Table 7 formula reproduction—not measured target latency and not benchmark-accuracy reproduction.

Research

Capability versus allocation

AnyRes / LLaVA-NeXT

Tiling preserves local detail and aspect ratios. It expands feasible budget; it does not decide whether this query needs it.

Native dynamic resolution

Qwen2-VL maps varying image sizes to varying token counts. Dynamic capability is not objective-conditioned allocation.

CARES selector

A query-aware selector predicts the smallest sufficient input range before invoking an untouched target VLM.

more available tokens ≠ more useful evidence

CARES method

CARES problem definition

x: image q: query F: target VLM x^(r): resized image

T(r): target utility at input range r

r_s = min {r ∈ R : sufficient(T,r)}

Finite support

R={r₁,…,r_K}; choose among supported ranges.

Target untouched

Selection is upstream; F is not retrained or modified.

Minimal sufficient

First supported range satisfying a metric-derived criterion—not globally minimal pixels.

CARES method

Label generation — utility and sufficiency

u_i = ANLS(F(x^(rᵢ),q), y)

u_i ≥ τ ∧ max_j>i(u_j−u_i) ≤ δ

Thresholds

Paper setup: τ=.85 utility floor; δ=.10 tolerance. Both encode metric/teacher assumptions.

Non-monotonic utility

Use all higher classes. u={.86,.80,.99}: r₁ fails because later gain .13>δ.

Terminal fallback

If no lower range qualifies, select the highest supported class.

ANLS = average normalized Levenshtein similarity; labels inherit metric sensitivity.

CARES method

CARES architecture

low-res proxy

→

truncated SmolVLM
≈350M

→

image + query feature

→

K-class classifier

→

untouched target VLM

Key separation

Selector inference is paid once; routed target inference dominates remaining cost.

Information ceiling

A low-resolution selector cannot infer evidence absent from its proxy.

Compatibility

No target fine-tuning; prediction maps to supported target input.

CARES method

Training protocol and variant

Reported setting	Value
Training samples	80,000
Datasets	4
Label smoothing	0.05

L = −Σ_k ỹ_k log p_k

Base selector

Low-res proxy + truncated SmolVLM representation + classification head; labels from target-VLM utility sweeps.

AR Granite-Docling variant

Paper also reports an autoregressive variant; architecture remains task/model dependent.

80K / four datasets / 0.05 are reported facts—not reproduced here.

CARES method

Continuous inference and upward rounding

p=softmax(z), r̃=Σ_kp_kr_k

336×.10 + 672×.25 + 1024×.45 + 2048×.20 = 1,072 → round upward to 2048

Why upward?

Avoid selecting a supported range below the continuous expectation.

Boundary

Rounding guarantees support membership and order—not empirical sufficiency.

Evidence

Reported evidence across target models

Target	Reported score	Reported cost
Granite	.59→.60	−63%
InternVL	.77→.77	−64%
Qwen2.5-VL-72B	.79→.80	−70%
GPT-4o	.69→.68	−55%

Scope

Nine benchmarks · four target models (paper report).

Evidence status

REPORTED, NOT INDEPENDENTLY REPRODUCED. Score aggregation, hardware, routing overhead, and exact cost definition require empirical replication.

Evidence

Scientific interpretation and limitations

Selector overhead

Break-even requires C_s+E[C_r]<C_h.

Proxy blindness

Low resolution can hide OCR and tiny-object evidence.

Metric dependence

ANLS labels inherit teacher, answer, threshold, and benchmark choices.

Interaction scope

Single-image/single-turn focus; video, multi-page, conversation need new policies.

Safety gap

No independent adversarial, calibration, OOD, or safety study supplied here.

Cost proxy

Pixel/token reduction does not guarantee latency, memory, energy, or quality.

Literature

Literature map by intervention stage

Input

DRNet · AnyRes · Qwen2-VL

Encoder

DynamicViT · EViT · ToMe

VLM sparsity

HiRED · SparseVLM

Depth

PyramidDrop · VTW

Elastic

TokenFLEX · M3 · LLaVA-Mini

Cascade

SGL · compute-optimal scaling

allocation → pruning → merging → withdrawal → elastic training → collaboration

Literature

Input-resolution lineage

DRNet (2021)

Per-input dynamic resolution for efficient recognition; training changes the model; query awareness is not the central VLM objective.

AnyRes / LLaVA-NeXT

Grid/tiles preserve detail and aspect ratio. Mechanism exposes capacity, but does not choose by question.

Qwen2-VL

Arbitrary image size to variable visual tokens: capability, not necessarily allocation.

query-aware? CARES: yes | DRNet / AnyRes / Qwen2-VL: not the same controller objective

Literature

ViT token reduction mechanisms

ρ=|S_keep|/N

DynamicViT

Predicts retained tokens; attention masking supports differentiable training.

x̄=Σa_ix_i/Σa_i

EViT

Keeps attentive tokens and fuses the rest into a summary.

m(a,b)=(s_aa+s_bb)/(s_a+s_b)

ToMe

Merges similar tokens while preserving aggregate “size” weights.

Composition warning: reducers can remove evidence selected upstream. Joint calibration is required.

Literature

VLM inference sparsification

HiRED

Allocates visual-token budget using high-resolution encoder signals, retaining spatially informative tokens.

b_i=B·w_i/Σ_jw_j

SparseVLM

Uses text-to-vision relevance and visual-token ranking for task-aware retention.

rel(v_i,q)=max_jsim(v_i,t_j)

rank(v_i)=rel(v_i,q)+λ·centrality(v_i)

Schematic controller equations; consult papers for exact definitions.

Literature

Depth-wise visual-token reduction

s₀→s₁→…→s_L, s_ℓ+1≤s_ℓ

Ω≈2s²h+12sh²

PyramidDrop

Drops visual tokens progressively across LLM depth; savings compound through quadratic and linear sequence terms.

Visual Tokens Withdrawal

Withdraws tokens after their information influences text states. Timing is a fidelity/control variable.

Resolution controls input evidence; depth controls retention.

Literature

Elastic trained models and controller gap

TokenFLEX

Trains over flexible visual-token budgets; runtime budget choice still needs a controller.

Matryoshka Multimodal Models

Nested representations remain useful at multiple granularities; deployment still chooses budget.

LLaVA-Mini

Learned modality interaction compresses visual burden; architecture is not a query policy.

elastic capability + controller objective + calibrated gate = adaptive system

Literature

Small–large collaboration and compute optimality

F_inf=O(NT), T=Q+V+G

SGL

Small model can route/draft/handle easy work and escalate. Overhead and error correlation determine value.

Y(N,T)=(A/N^α)·(B/T^β)+D

Compute-optimal VLMs

Model size N and token budget T form a joint design space; more image tokens are not universally optimal.

OCR caveat: below readability threshold, capacity cannot recover missing characters.

Synthesis

Composition thesis — a generalized controller

a=[r, crop, B_enc, merge, withdrawal layer, model, escalate]

CARES upstream
select evidence scale

→

encoder/projector
prune or merge

→

decoder depth
withdraw

→

cascade
model/escalate

Objective: minimize expected cost subject to fidelity, safety, support, and evidence-retention constraints.

Project

OSS project goals and evidence philosophy

Practical runtime

Portable Agent Skill + deterministic Pillow CLI. Explicit keyword policy—not trained CARES ≈350M selector.

Executable science

Wolfram reproduces Algorithm 1, Equation 3, Table 7 accounting, sensitivity, and break-even economics.

Narrow formalization

Lean proves selected exact statements under assumptions. It does not prove the paper or empirical accuracy.

trace every claim to an evidence class

Project

End-to-end project workflow

Runtime

Agent Skill runtime behavior

1
TEXT FIRST

2
INSPECT

3
OBJECTIVE

4
CROP FIRST

5
SAFE RESIZE

6
ESCALATE

Text-first gate

If text, DOM, OCR, or structured data answers the question, avoid image inference.

Fidelity policy

Overview 1280/JPEG88; detail 2048/PNG; exact/critical preserve dimensions.

Escalation

Warnings and consequential evidence trigger source verification or higher fidelity.

Runtime

Python implementation — deterministic by design

CLI / API

inspect PATH
prepare PATH --objective …
auto | overview | detail | exact | critical
crop X,Y,W,H · max-edge N

Safeguards

EXIF transpose; crop before resize; no upscale/overwrite; frame-count and color-mode checks.

Deterministic JSON

Policy/reason, dimensions, crop, format, pixel reduction, provenance, warning.

classifier = ordered keyword boundary matching

19 focused tests reported. Pixel reduction is only a proxy for target token and latency reduction.

Runtime

Worked path — exact evidence in a report

report.png
2200×1400

→

objective
exact CVE + version

→

policy
exact

→

crop
840,120,620,400

→

evidence.png
lossless

Crop first

Isolate the CVE table region before inference; preserve source unchanged.

Verification

No downsampling; deterministic JSON audit trail; verify consequential evidence against source.

Scientific lane

Wolfram architecture and generated artifacts

CARESModel.wl
validated functions

CARESReproduction.nb
narrative

build_project.wls
build

proof_audit.wls
checks

exports/
CSV · PNG · JSON

Package boundary

Validation, selector semantics, token formulas, break-even predicate.

Build boundary

Deterministic generation; required-artifact and audit reports.

Evidence boundary

10/10 analytic checks passed. Empirical benchmarks remain out of scope.

Scientific lane

Wolfram scientific checks

Selector overhead break-even analysis chart

C_s + E[C_r] < C_h

Algorithm 1

First passing class using τ and all-higher-gain δ; non-monotonic case included.

Equation 3

Weighted expectation, one-hot recovery, deterministic bounds.

Table 7

Published token-count targets and percentages checked analytically.

Formal lane

Lean formalization — trust boundary

Definitions

Finite three-class expected resolution; upward rounding; positional sufficiency selector.

Theorem families

Bounds, one-hot identities, upward mass transfer, supported rounding, first-pass/fallback behavior.

Pinned build

Lean 4.19.0; Mathlib v4.19 revision c44e0c8…; lake build exit 0; proofs complete.

Critical boundary: Lean proves these statements under assumptions. It does NOT prove CARES empirical accuracy, datasets, implementation fidelity, compute savings, or the paper as a whole.

Formal lane

Lean proof sketches and assumptions

r₁≤Σp_ir_i≤r₃

Assumptions

pᵢ≥0; Σpᵢ=1; ordered support. Upward transfer preserves mass and nonnegativity.

oneHot(k) ⇒ E[r]=r_k

Round-up

Supported, no lower than estimate, no higher than largest support—within defined cases.

mass ↑ ⇒ E[r] nondecreasing

Selector semantics

Positional first-pass / second-pass / highest fallback—not numeric minimality over ℝ.

No “Lean proves the paper” claim.

Evidence

Evidence matrix — do not collapse categories

Claim	Formally proved	Numerically validated	Reported / not reproduced
Expectation bounds / one-hot	✓	✓	—
Algorithm 1 examples	—	✓	paper mechanism
Table 7 token accounting	—	✓	published values
Benchmark accuracy / savings	—	—	✓ unreproduced
Python safeguards	—	19 tests	project behavior
CARES trained-selector accuracy	—	—	✓ unreproduced