WEEK OF APR 26 – MAY 2, 2025

Qwen3 opened eight models under Apache 2.0 the same week the leaderboard itself got audited

A 235B mixture-of-experts activating 22B parameters landed under a license with no acceptable-use clause, beside a 671B open-weight Lean prover. Simultaneously, researchers documented how the arena rankings favored closed labs — and named 27 private Llama-4 variants.

Alibaba's Qwen team released Qwen3 on April 29: eight open-weight models under Apache 2.0, two of them mixture-of-experts — 235B total with 22B active, and 30B total with 3B active — plus dense checkpoints at 32B, 14B, 8B, 4B, 1.7B and 0.6B, each runnable in a thinking or non-thinking mode toggled per request. Activating 22B parameters per token carries roughly the memory and FLOP profile of a 20-30B dense model, so frontier-adjacent quality now deploys on hardware teams already own — and Apache 2.0 removes the acceptable-use and reporting clauses that turned some earlier open weights into a legal review.

The same week produced the correction that makes such claims checkable. The Leaderboard Illusion, a 68-page audit from Cohere Labs and academic collaborators, documented that a small group of preferred providers could test many variants privately and publish only the best-scoring one, identified 27 private Llama-4 variants Meta tested ahead of release, and simulated that ten private variants were worth roughly 100 Arena points. DeepSeek meanwhile published a 671B open-weight theorem prover for Lean 4, and Meta and Microsoft priced the compute build-out in opposite directions on the same day.

WED · Apr 30, 2025open-weightsdeepseekformal-methodstheorem-proving

DeepSeek publishes a 671B open-weight theorem prover for Lean 4

DeepSeek uploaded DeepSeek-Prover-V2 to Hugging Face on April 30: a 671B-parameter open-weight model built on DeepSeek-V3-Base that writes Lean 4 proofs, plus a 7B sibling with a 32K context window. The pipeline bootstraps itself — DeepSeek-V3 decomposes a theorem into Lean subgoals, a smaller prover searches each subgoal, and the resolved steps are stitched back into chain-of-thought data used to cold-start reinforcement learning. DeepSeek reports an 88.9% pass ratio on MiniF2F-test and 49 of 658 PutnamBench problems solved, which it calls state of the art for neural theorem proving.

Formal verification is the one part of the stack where generated code can be checked instead of trusted, and the missing piece was always a prover good enough to automate it. With 671B weights downloadable and a 7B variant that fits on a single GPU, a team can wire proof search into CI and let Lean reject bad proofs rather than asking a second model for an opinion. The marginal cost of that loop is the hardware you already own, not an API invoice.

DeepSeek publishes a 671B open-weight theorem prover for Lean 4
Hugging Face

WHY IT MATTERS

If machine-checked proofs become a cheap local primitive, verified code moves from research demo to CI gate: an agent proposes a patch, Lean decides whether the reasoning holds, and reviewers stop being the last line of defense on correctness claims. That is a materially different reliability story from asking a second model to agree with the first.

WED · Apr 30, 2025infrastructurecapexearningsmetamicrosoft

Meta raises 2025 AI capex to $64-72B while Microsoft says its capex growth slows

Meta's Q1 2025 results on April 30 lifted full-year capital expenditure guidance to $64-72 billion from $60-65 billion, citing additional data-center investment for AI and a higher expected cost of infrastructure hardware; the same release puts Meta AI at almost 1 billion monthly actives. Microsoft reported the same day: revenue of $70.1 billion, Azure growth of 33%, and $21.4 billion of capex in the March quarter, up 53% year on year. CFO Amy Hood told the call that capex keeps growing in FY26 but at a lower rate than FY25, weighted toward short-lived assets correlated with revenue — from a company that had spent recent months slowing or pausing some data-center projects.

The two numbers price capability in opposite directions on the same day. A raised Meta budget says capacity is scarce enough to justify paying more for servers; Microsoft's decelerating curve and shift to revenue-linked hardware says the build-out is being sized to demand rather than ambition.

Meta raises 2025 AI capex to $64-72B while Microsoft says its capex growth slows
s21.q4cdn.com

WHY IT MATTERS

Hyperscaler capex guidance is the twelve-month leading indicator for GPU availability and inference pricing. A budget being raised on hardware costs while a competitor's growth rate falls tells you to model per-token costs as flat-to-uneven rather than falling, and to keep a self-hosted path priced alongside any API contract.

TUE · Apr 29, 2025open-weightsqwenmoepricingdistillation

Qwen3 opens eight models under Apache 2.0, including a 235B MoE that activates 22B

Alibaba's Qwen team released Qwen3 on April 29: eight open-weight models under Apache 2.0, two of them mixture-of-experts — Qwen3-235B-A22B (235B total, 22B active, 128K context) and Qwen3-30B-A3B (30B total, 3B active, 128K) — plus dense 32B, 14B, 8B, 4B, 1.7B and 0.6B checkpoints. Every model runs in two modes, a thinking mode that emits a reasoning trace and a non-thinking mode for latency-critical calls, toggled per request through the chat template's enable_thinking flag. Qwen reports the flagship as competitive with o1, DeepSeek-R1, o3-mini, Grok-3 and Gemini 2.5-Pro on coding, maths and general benchmarks, and says the 30B MoE beats QwQ-32B while activating a tenth of the parameters.

The cost consequence is arithmetic: activating 22B parameters per token carries roughly the memory and FLOP profile of a 20-30B dense model, so frontier-adjacent quality now deploys on hardware teams already own. Supported checkpoints landed in vLLM and Ollama on day one alongside OpenAI-compatible endpoints, so moving a workload off a closed API is a config change rather than a migration. Apache 2.0 also removes the acceptable-use and reporting clauses that turned some earlier open weights into a legal review, and the small dense models exist mainly as distillation targets for teams that want the behavior at a fraction of the footprint.

WHY IT MATTERS

A permissively licensed, frontier-adjacent MoE resets the build-versus-buy line: prompts, weights and fine-tunes stay inside your infrastructure, inference becomes a hardware amortization line you control, and every closed-model price has to justify itself against a downloadable substitute that scores within a few points. This is the release that made self-hosting a reasoning-class model a mainstream default rather than a compromise.

TUE · Apr 29, 2025evalsbenchmarkslmarenaopen-weightsmeta

The Leaderboard Illusion: 27 private Llama-4 variants, and an arena that favored closed labs

On April 29, researchers from Cohere Labs and academic collaborators posted The Leaderboard Illusion (arXiv:2504.20879, 68 pages), an audit of Chatbot Arena's ranking pipeline. They document an undisclosed practice that let a small group of preferred providers test many variants privately and publish only the best-scoring checkpoint, and at the extreme they identify 27 private LLM variants Meta tested in the lead-up to the Llama-4 release. On data, they estimate Google and OpenAI received 19.2% and 20.4% of all arena battles respectively, while 83 open-weight models combined received 29.7%. Simulations put the payoff of ten private variants at roughly 100 Arena points, and two identical checkpoints of the same model scored 17 points apart purely from sampling randomness.

This lands three weeks after Llama 4's own leaderboard problem, when Meta submitted a non-public experimental chat version of Maverick to LMArena and LMArena replied that Meta's reading of its policy did not match what it expects from model providers. The paper's contribution is that the anecdote generalizes: sampling rates, model deprecation and score retraction are all asymmetric, so single-digit rank gaps carry no signal.

WHY IT MATTERS

Model selection increasingly starts from a leaderboard number. A documented, provider-favoring distortion means that number is marketing input rather than evidence — and the same overfitting it rewards in labs is the failure mode you inherit if you route production traffic by rank instead of by eval on your own workload. The operational fix is cheap: evaluate on your own traffic and treat Arena rank as a sourcing hint.

TUE · Apr 29, 2025agent-infrastructureguardrailsprompt-injectionllamasecurity

LlamaCon: an Llama API preview, a standalone Meta AI app, and open guardrails for agents

At its first LlamaCon on April 29, Meta opened a limited free preview of the Llama API with Python and TypeScript SDKs, OpenAI-SDK compatibility, and hosted fine-tuning plus an evaluation suite starting with Llama 3.3 8B — with the explicit promise that models built there remain portable to self-hosting. The same day it shipped the standalone Meta AI app, pitched on the personalization it can draw from a user's Facebook and Instagram context, and said Meta AI now spans WhatsApp, Instagram, Messenger and Facebook at almost a billion monthly actives.

The developer-facing releases were the security tools, all open source: Llama Guard 4, Prompt Guard 2 and LlamaFirewall. LlamaFirewall is an agent guardrail framework with three parts — PromptGuard 2 as a universal jailbreak detector, Agent Alignment Checks as a chain-of-thought auditor that inspects agent reasoning for prompt injection and goal misalignment, and CodeShield, an online static analyzer that blocks coding agents from emitting insecure code. Meta says the framework runs in production internally.

WHY IT MATTERS

Prompt injection is still unsolved at the model layer, so agent builders need defense in depth at the harness. An open-source, in-production guardrail stack gives a concrete starting point for that layer — and auditing the reasoning trace rather than only inputs and outputs is the pattern worth copying. A hosted API with genuinely portable weights also removes the last argument for accidental lock-in when prototyping against a closed provider.