Terminal-style Mathematical Modeling Bench: The First Agentic and Verifiable Benchmark for Mathematical Modeling

Terminal-style Mathematical Modeling Bench. The First Agentic and Verifiable Benchmark for Mathematical Modeling. By Xiaojun Wu and five others, from IDEA Research, the Hong Kong University of Science and Technology, Guangzhou, and one other institution. Published on the fifth of November.

Mathematical modeling starts from an open-ended real-world problem and ends with assumptions, a model, a solution, and a recommendation someone has to defend. Its answers only matter if two things hold: they are close to a credible reference, and they are physically feasible. Existing benchmarks miss that. Some score fragments of a solver. Others hand a written report to an LLM judge for a grade. Either way, the numbers the modeling produced are never checked.

TB-MathModel, the Terminal-style Mathematical Modeling Bench, aims at the numbers themselves. It is described as the first benchmark to make complete contest-style modeling problems agentic, verifiable and terminal all at once. Agentic means a model acts as an agent working through the task. Verifiable means its answer can be checked rather than judged. Terminal means the work happens at a command line. The material is eighteen real problems from the CUMCM and MCM contests, from the years two thousand twenty-three to two thousand twenty-five. What gets scored is not the whole write-up but the numeric core of each problem's final question.

Each task arrives as it would for a contestant: the verbatim statement, the official attachments and the figures, all inside a containerized terminal. The agent works there and returns a single JSON artifact. That answer is compared against a reproduction of the paper that won an Outstanding award, and in fact against a panel of human outstanding papers rather than just one. A model has to land near many accepted answers, not one lucky one.

Two further choices set it apart. Scoring is direction-aware and one-sided, so an answer that beats the reference anchor is never penalised for it. And feasibility is verified in two layers. A programmatic gate checks six decidable forms of invariant, and on top of that sit six hundred and twenty-four obligations in Lean four. The gate is hard: an infeasible answer scores zero, however close its number looks.

Seven multimodal entries were evaluated, each over three seeds. The strongest reach a multi-reference O-Eval of sixty-four point five eight percent. An open model holds fifty-nine point eight one percent at roughly a hundredth of the cost. Under this scoring, the distance between the strongest entries and a far cheaper open model comes to under five points. Because the feasibility gate zeroes infeasible answers, an answer that fails it contributes nothing to those percentages, however close its number was.

Where earlier benchmarks scored solver fragments or let a judge grade a report, this one asks two plainer questions of the final numbers. Are they near what strong human teams found? And could they physically be true? Both are answered by machine, so a score can be reproduced rather than re-argued. The authors offer it as a reproducible, machine-checkable signal for measuring long-horizon modeling competence, and as a way of collecting agent trajectories.