VeryTrace: Verifying Reasoning Traces through Compilable Formalism and Structured Verification

Multi-step reasoning in Large Language Models (LLMs) is often fragile, as logical errors or hallucinations in early steps propagate to produce incorrect final conclusions. Existing methods like end-to-end verification or majority voting often fail to diagnose the specific source of these errors. The authors introduce VeryTrace, a zero-shot framework that treats reasoning traces as compilable programs. By formalizing natural language reasoning into a Domain-Specific Language (DSL), the framework makes step dependencies explicit and mechanizes quantitative content as executable expressions.

VeryTrace operates through a generate-verify-repair loop. First, a context-extraction module identifies initial facts, assumptions, and constraints from the prompt. Second, a translation module converts the LLM's reasoning trace into a structured DSL trace. The verification pipeline then uses a hybrid approach:

• Deterministic Checks: Validates computational correctness, dependency resolution, and constraint satisfaction using executable code.
• Structured LLM Audits: Uses targeted LLM queries to evaluate non-mechanizable semantic inferences, such as commonsense reasoning or natural language constraints.

If a step fails verification, the system generates a specific error report (e.g., identifying a constraint violation or a faulty calculation), allowing the LLM to perform targeted repairs on the problematic segment rather than regenerating the entire trace.

VeryTrace addresses the trade-off between the lack of granularity in end-to-end verification and the high manual effort required by formal theorem provers. By providing a domain-agnostic way to verify reasoning processes, it improves performance across diverse tasks—including competition mathematics, robotics planning, and kinship reasoning—without requiring domain-specific training or in-context examples. This demonstrates that formalizing the structure of reasoning is a scalable path toward more reliable and interpretable LLM outputs.