FORGE: Measuring the Formalization Spectrum for Verifiable Legal Reasoning

Legal reasoning systems must combine natural-language understanding with reproducible rule application. Large language models (LLMs) are useful for parsing statutes and extracting facts, but their chain-of-thought traces are not reliable proof objects, their numeric reasoning is brittle under small perturbations, and their legal answers can hallucinate. Symbolic systems offer deterministic execution and auditability, but require costly legal formalization. We introduce FORGE, a framework for evaluating legal AI systems along a formalization spectrum: zero-shot prompting, chain-of-code, compiled rule interpretation with LLM fact extraction, and ontology-derived semantic extraction with deterministic rule application. FORGE exposes these levels through a unified runtime, allowing the legal decision boundary to be treated as an experimental variable rather than a fixed architecture. Across statutory tax reasoning, legal entailment, diversity jurisdiction, and Contract NLI, our results show that formalization is useful but not monotonically beneficial: tightly coupled numeric computation favors compiled interpreters with hand-curated schemas, while entailment and transfer tasks benefit more from ontology-grounded structured extraction combined with deterministic task interfaces. We explicitly report which components are hand-engineered, so the spectrum measures decision-boundary designs rather than fully automatic formalization. These findings support the choice of where the legal decision is made as a central design and evaluation dimension for verifiable legal AI.