Paper recorded by Signals 4 on 2026-11-02 in cs.CL. Abstract reproduced from arXiv; link to the original below.
Published 2026-11-02 on arXiv · recorded by Signals 4 on 2026-11-03
Category: cs.CL · 自然语言处理 · first seen 2026-11-03
In the LLM-as-formalizer paradigm, a large language model translates a problem into a formal program and leaves the search to a solver, gaining the solver's guarantees. Formalizers are now often reasoning models that write a long reasoning trace before the program, yet they are judged only by the program's output. We find that the trace routinely does the solver's job, assigning, testing and rulin