Decomposed Online Learning for Adaptive LLM Inference in Formal Mathematics

Recent advances in agentic mathematical reasoning show that frontier Large Language Models (LLMs) can solve highly challenging mathematical problems. However, these successes often require substantial inference-time compute, making them prohibitively expensive for routine theorem proving. Crucially, subgoals within a proof vary significantly in difficulty, and many can be solved by smaller, more efficient models. We present _METIS_, a budget-aware agentic framework that uses online learning to reduce inference cost while preserving overall capability. Rather than relying on a fixed model, we use feedback from the Lean compiler to (1) decompose the problem into sub-lemmas, (2) adaptively assign budget-efficient, capable models to individual sub-lemmas using a non-stationary online algorithm, and (3) reassemble the complete proof. The decomposition improves sample complexity by generating more tasks for the online learner, and improves predictive power since sub-lemmas are simpler than the original problem. Comprehensive evaluation across four benchmarks demonstrates that _METIS_ improves the trade-off between inference cost and proof resolution rate. Specifically, _METIS_ achieves an accuracy comparable to the base Claude-Opus-4.8 model while requiring 68.3% less budget on average. Furthermore, _METIS_ matches the strongest model selection baseline accuracy while reducing total budget expenditure by an absolute 13.6%. Furthermore, under unstable inference environments, our framework maintains robust performance, with up to twofold lower standard deviation in both inference accuracy and budget than static methods.