Tuesday, June 2, 2026
An interpretability preprint says diffusion image models read only word meaning and order from prompts, a Lean4 framework brings formal verification to agent workflows, and attackers seized Instagram accounts by asking Meta's support bot.
What image models read from a prompt
A preprint on arXiv argues that diffusion-transformer text-to-image models barely use their text encoders, drawing on only two properties of the embeddings: subword tokens merged into whole-word representations, and word order carried by the encoder’s positional embeddings. Cross-prompt context, attribute binding, and compositional structure go unused, the authors say; the image model itself decodes the linguistic structure.
To test this, the authors built a “bag of position-tagged words” embedding that keeps each word’s meaning and position but discards all whole-prompt context. Generating from that stripped-down representation matched full embeddings on visual quality and text fidelity, they report. If the result holds, text encoders are over-specified for the task and lighter, cheaper ones could suffice. The paper stops at the ablation: it includes no encoder-swap cost study, does not state how many models or datasets it covers, and has drawn little attention so far.
Formal verification for agent workflows
A second preprint applies Lean4, a dependent-type formal language used to machine-check mathematics, to LLM agent workflows. The framework, Lean4Agent, models a workflow’s semantics, checks it for consistency under stated assumptions, and tries to localize where a failed run went wrong; a companion tool, LeanEvolve, revises workflows from the verification results. On a hard subset of SWE-Bench-Verified and a subset of ELAIP-Bench across five models, the authors report that workflows passing verification beat failing ones by 11.94% on average, with LeanEvolve adding 7.47% on the SWE tasks. The headline gap compares passing against failing workflows, a correlation selection effects could explain, and the abstract gives no subset sizes or baselines. The interest is the approach, machine-checkable specifications for agent behavior rather than natural-language evals, more than the reported margins.
Account takeover by request
Simon Willison’s link blog relays reports that attackers took over high-profile Instagram accounts by asking Meta’s AI support bot to do it. Per the accounts Willison cites, the attacker told the bot to link the target username to an attacker-controlled email, then supplied the verification code, completing Instagram’s account-recovery flow. Willison says it barely qualifies as prompt injection: the failure is a missing authorization check, not a clever jailbreak, since Meta gave the support bot authority over recovery with no independent check of who was asking. The report is secondhand; Willison says he doubted it until he saw it corroborated by multiple sources, including video, and the post quotes no Meta response. The recurring lesson, as companies connect chatbots to privileged backends, is to keep irreversible identity actions like email rebinding and account recovery behind a separate verification step.
What to watch today
- Replication of the text-encoder ablation, and any encoder-swap study that converts the claim into measured cost or quality deltas.
- A Meta statement or fix on the Instagram recovery flow; none appears in the reporting so far.
- Release of Lean4Agent’s FormalAgentLib library and an independent evaluation with disclosed baselines and subset sizes.