ReasonSTL: A Learned Formal Compiler for Natural Language to Signal Temporal Logic

Compiling natural-language requirements into Signal Temporal Logic (STL) requires exact recovery of temporal scope, predicate selection, logical structure, and numerical constraints. Errors in any of these decisions alter the executable semantics. We formulate this problem as direct compilation from a clear requirement and a declared predicate interface, evaluating both translation accuracy and end-to-end latency. We introduce ReasonSTL, a locally deployed learned formal compiler that integrates semantic structure prediction, deterministic numerical tools, typed AST construction, and staged validation. Outcome-bounded process rewards tie stage-level credit to final-formula correctness, and prefix masking suppresses downstream credit after the first invalid step. The resulting trajectories expose tool execution, value placement, and reward assignment for inspection. We further introduce STL-Bench, a bilingual, computation-aware benchmark with scenario-held-out evaluation and 500 independently authored expert requirements. ReasonSTL-8B achieves 0.700/0.680 canonical accuracy on held-out English/Chinese scenarios and 0.780/0.752 expert semantic accuracy on Manual-500. On one H20, it attains 0.724 aggregate Manual-500 canonical accuracy with 3.88 s mean latency, compared with 0.524 and 3.87 s for Claude-Opus-4.7 under the reported serving configurations. These results establish a strong local accuracy–latency trade-off for open-loop NL-to-STL compilation.