Haz Lab is a research group led by Prof. Li "Harry" Zhang at Drexel University. We address the lack of verifiability and the danger of hallucination of large language models (LLMs) with the LLM-as-Formalizer paradigm: shifting their role from an unreliable problem solver to a precise translator. The LLM converts natural language input into rigorous formal languages (like PDDL), which are then solved by symbolic solvers, providing verifiability and deterministicity. Such a neuro-symbolic method promises performant and reliable AI systems for high-stakes domains.

I. Auto-Formalization and Tool-Based Problem Solving

Our primary line of work uses LLMs to map specifications of complex reasoning tasks—such as MDP/POMDP planning, constraint satisfaction, or theorem proving—to formal representations like PDDL, SMT, and Lean. These are not only verifiable but also deterministically executable via external solvers. Efforts include benchmarking, test-time and training-time improvements, multimodal and multi-agent formalization, etc.

II. Mechanistic Interpretability

Our secondary line focuses on optimizing the efficiency and fidelity of the LLMs themselves in the abovementioned process. We emply mechanistic interpretability methods such as steering, circuit analysis, etc., to dissect and alter LLMs' behavior in auto-formalization tasks.