LLM Agents Interview Questions #18 - The Benchmark Isolation Trap

Math benchmarks reward sealed reasoning problems, while production theorem proving is a retrieval problem across an evolving dependency graph.

You’re in a Senior AI Engineer interview at Google DeepMind. The interviewer sets a trap:

“Your reasoning model hits 80% on miniF2F math benchmarks using just the current proof state. You deploy it to help researchers formalize a real paper in Lean, and its accuracy flatlines to 0%. Why?”

90% of candidates walk right into it.

Most candidates say the model lacks domain-specific training data. They suggest setting up a DPO pipeline to fine-tune on the specific math subfield, or scaling up from an 8B to a 70B parameter model to handle the reasoning complexity. If they are feeling infrastructure-savvy, they blame the context window and suggest RoPE scaling to 128k to ingest the whole textbook.

But you aren’t optimizing for reasoning capability; you’re dealing with environmental blindness.

The reality is that math competition problems are hermetically sealed. An IMO problem can be stated in one line of code and relies entirely on standard library (Mathlib) theorems. Real-world research math doesn’t work like that.