This paper presents a hybrid framework that combines Large Language Models (LLMs) with Satisfiability Modulo Theories (SMT) solvers to advance automated legal analysis in the financial regulatory domain. Designed for Taiwan's legal context, the system integrates a Retrieval-Augmented Generation (RAG) pipeline to access statutory references, historical enforcement cases, and corporate violation records from the Financial Supervisory Commission (FSC). Leveraging Python-based tools including Z3 and OpenAI API, the framework supports case similarity assessment, regulatory constraint checking, and scenario simulation through constraint-based formal reasoning.
The agent emulates legal expert analysis using a chain-of-thought prompting approach tailored for financial compliance. It identifies potential violations, interprets applicable legal provisions, and generates corrective recommendations aligned with statutory requirements. By distinguishing hard constraints (laws) from soft constraints (case-specific facts), the system enables minimal legal corrections and iterative validation using a cone-of-influence analysis. A Gradio-based interactive interface allows users to explore compliance evaluations in real-time.
Experimental evaluation on 87 FSC-issued penalty cases shows that the proposed LLM+SMT hybrid system significantly outperforms LLM-only baselines in identifying illegal terms, generating accurate corrections, and delivering interpretable reasoning outputsโachieving over 300ร speed-up and perfect accuracy in constraint satisfaction tasks. This work lays the groundwork for future applications of AI-enhanced legal reasoning in financial governance, offering a transparent, customizable, and regulation-aligned tool for automated compliance diagnostics.