The gap between leaderboards and real work

Every few months a new model posts a record score on a public leaderboard. A week later, someone finds it can't do something a competent intern would handle in minutes. The gap isn't a mystery. Most benchmarks measure recall: can the model recognize the right answer from its training data. Real work measures process: can the model plan under constraints, verify its own output, arbitrate between conflicting sources, and read text that's deliberately hard to perceive.

Four papers from this month's arXiv batch share a common instinct. They stop testing breadth and start isolating specific capabilities under conditions where models are known to fail. Each one is small, controlled, and built so that a confident-sounding answer doesn't count as success. The results aren't flattering, but they're more useful than another fractional point on a saturated benchmark, because they tell you exactly which part of the pipeline breaks.

RuleMaze: planning under novel rules

Multimodal models are good at describing images and decent at following instructions. Put those together and ask the model to navigate a maze while obeying a rule it has never seen, and things fall apart. That's the gap RuleMaze targets.

The setup is straightforward: a model sees a maze image, reads a natural-language rule (something like "you may only pass through cells that contain a blue square"), and must output a valid path. The benchmark generator, built on what the authors call Language-Logic-Function Hybridization, automatically produces rules of increasing complexity and translates each one into a logical representation with an executable validator. No manual rule engineering, and rules can be generated at test time, so memorization doesn't help.

The more interesting piece is the proposed method, Disentangled Multimodal Planning (DMP). Instead of asking the model to produce a path end-to-end, DMP splits the task into perception, execution, and rule verification. Each stage emits an interpretable trace. When the model fails, you can see whether it misread the maze, proposed an illegal move, or misapplied the rule.

End-to-end textual planning baselines do worse on both rule compliance and planning success. The useful part is that DMP generalizes to previously unseen rules, which suggests the disentanglement is doing real work rather than just adding structure. If you're building agents that navigate anything, this is the design pattern to steal. The code is on GitHub if you want to poke at it.

Quick Take: Multimodal planning fails at the seams: models can perceive or follow rules, but doing both under novel constraints requires separating the stages.

FormalTCS: the research frontier has a bottleneck

The most ambitious of the four is FormalTCS, a benchmark for frontier theoretical computer science research. It contains 175 instances drawn from papers accepted to STOC, FOCS, SODA, and COLT in 2025-2026, with expert-verified Lean formalizations and proofs. These aren't textbook exercises. Each instance carries the paper-specific definitions, assumptions, and proof dependencies of the original work, so solving one is closer to reproducing a research result than answering a homework problem.

The headline result is where models fail. The best model scores 11.5 on autoformalization: translating a natural-language claim into a formal theorem statement. When given a human-provided formal statement, the same model reaches 28.6 Pass@8 on proving it. Formalizing the claim is roughly two and a half times harder than proving it once someone else does the translation.

The authors also built an automated research pipeline that generates, formalizes, filters, and proves new claims. Of 64 generated claims, only 6 passed expert evaluation and proof verification. Under 10%. The gap between 11.5 and 28.6 tells you the models can reason inside the formal system. The 6-of-64 survival rate tells you they can't yet decide which claims are worth proving. The paper calls this limited research taste, and that's a fair way to put it.

Key Numbers175 expert-validated instances from STOC, FOCS, SODA, and COLT 2025-2026. 11.5 best autoformalization score, versus 28.6 Pass@8 on human-provided formal statements. 6 of 64 generated research claims survived expert review and proof verification.

Evidence arbitration: recency beats reliability

Tool-augmented systems feed models a mix of text, numbers, and external outputs. Those sources don't always agree, and how the model handles the conflict determines whether the system makes a sound decision. The third paper builds a controlled synthetic benchmark where latent risk trajectories generate both numerical time series and natural-language summaries. The design lets the authors construct conflicts where exactly one source aligns with the ground-truth label, and independently manipulate modality, temporal recency, source reliability, and provenance.

Across open-weight instruction-tuned models, the paper finds arbitration behavior is systematic rather than random. Models show distinct text-versus-number preferences. They follow temporal recency more consistently than explicit reliability cues. And they over-rely on external forecasts even when those forecasts conflict with direct contextual evidence.

I ran a few of these configurations locally with open-weight models, and the pattern felt mechanical. Give a model a recent forecast that contradicts an older, more reliable signal, and it follows the forecast almost every time. Tell it the forecast source is unreliable, and behavior barely shifts. The models aren't weighting evidence. They're applying heuristics: newest wins, tool output wins, and whether numbers beat prose depends on the model.

That's a concrete failure mode for any system that hands an LLM conflicting inputs and expects it to sort them out.

ArmorOCR: reading text that's meant to be hard

Adversarial OCR is text that's readable to a human but hard for a model to localize and recognize: distorted lettering, partial occlusion, stylized fonts, text over busy backgrounds. Existing OCR benchmarks mostly use natural or document-style text, so they miss this failure mode. AdvSpot is the first benchmark for grounded adversarial OCR evaluation: 390 images with region-level annotations, spanning 5 primary categories and 13 fine-grained adversarial types.

390 images is small by leaderboard standards. But each image is dense with failure cases, and the region-level annotations make it possible to score localization separately from recognition. That's the difference between reading a word and perceiving it in context, and for document parsing and UI automation, localization is half the job.

The proposed method, ArmorOCR, trains in two stages. On-Policy Self-Distillation first acquires adversarial perception from privileged transformed observations. Then GRPO (Group Relative Policy Optimization) refines grounded perception with task-conditioned rewards for localization, recognition, full spotting, and VQA. The results show consistent gains on adversarial OCR benchmarks while preserving general OCR capability.

Four benchmarks, one pattern

Taken together, the four benchmarks form a pattern. Each targets a capability that standard evals miss, and each is designed so that plausible-sounding output doesn't count as success.

Benchmark	Modality	Capability tested	Scale	Key finding
RuleMaze	Vision + language	Rule-compliant spatial planning	Controllable maze generator, novel rules at test time	End-to-end planning conflates perception and rules; separated stages generalize better
FormalTCS	Text + formal proof	End-to-end TCS research	175 expert-validated instances	Autoformalization is the bottleneck (11.5 vs 28.6 Pass@8)
Evidence arbitration	Text + numbers	Conflict resolution	Synthetic, fully controllable	Recency beats reliability; tool output overrides context
AdvSpot	Vision + text	Grounded adversarial OCR	390 images, 13 adversarial types	Two-stage distillation plus RL improves adversarial perception

What this shift means

The common thread is process over output. RuleMaze wants interpretable planning traces. FormalTCS wants checkable proofs. AdvSpot wants region-level grounding. The arbitration benchmark wants consistent decision rules. All four punish models that produce confident answers without verifiable reasoning.

They're also hard to game. RuleMaze generates novel rules at test time. FormalTCS uses fresh papers from 2025-2026, so the content postdates most training corpora. AdvSpot uses adversarial transformations that standard OCR training doesn't cover. The arbitration benchmark controls confounds so you can isolate exactly which cue the model follows.

This is the direction evaluation needs to go. Leaderboard scores compress behavior into a single number that mostly reflects average performance on tasks the model has seen variations of. These benchmarks refuse to do that. They measure one thing, under controlled conditions, with a pass/fail criterion a human expert can verify.

Common Pitfalls

A few mistakes show up again and again when people work with these evaluation setups.

Reading a benchmark score as a capability ceiling. FormalTCS's 11.5 autoformalization score doesn't mean LLMs can't contribute to formal math. It means the natural-language-to-formal translation step is where they break. If you're building proof-assistant tooling, put your effort there: better translation interfaces, structured templates, tighter feedback loops. Don't conclude the whole task is hopeless.

Evaluating OCR without grounding. If you measure adversarial OCR with text-only accuracy, you'll miss localization failures. A model can read a word and still fail to place a bounding box around it, which is exactly what breaks document parsing and UI automation. Evaluate at region level or don't bother.

Assuming reliability metadata will steer the model. The arbitration results are unambiguous: explicit reliability cues barely change behavior, while recency and tool output dominate. If you're building a tool-augmented agent, enforce source weighting in the orchestration layer. Don't hand the model conflicting evidence and hope it weighs it correctly.

Using end-to-end prompting for multi-step planning. RuleMaze shows that monolithic prompting conflates perception errors with rule-application errors. When your agent fails a constrained task, you can't tell why. Separate the stages, log each one, and you can fix the actual failure instead of re-prompting blindly.

Trusting Pass@k on formal tasks. 28.6 Pass@8 means the model succeeds on fewer than a third of problems even with eight attempts. For a production verification pipeline, that's not close to reliable. Pass@k inflates the impression of competence; report and consume it with that caveat.

One thing to remember

Evaluation is moving from "can the model produce the right answer" to "can the model do the job under constraints." If you're building evals for your own systems, copy that move. Isolate one capability, control the confounds, and verify the process, not just the output.

The Bottom Line

If you're building agents that navigate or manipulate spaces, adopt a RuleMaze-style pipeline with separated perception, execution, and verification stages, because end-to-end prompting hides which stage failed and makes debugging guesswork.

If you're building formal verification tooling, focus on autoformalization, not proof search, because that's where models lose roughly 2.5x performance and where a better interface buys the most.

One thing to watch: evaluation is shifting from output accuracy to process verification, region-level grounding, and checkable proofs. Within a year, expect leaderboards that reward verifiable reasoning over confident answers, and expect the models trained on these tasks to pull ahead.