A Multimodal AI System: Comparing LLMs and Theorem Proving Systems

This paper discusses a bi-modal AI system applied to legal reasoning for tax law. The results given here are very general and they apply to similar systems besides tax law. A central goal of this work is to gain better understanding of the relationships between LLMs (Large Language Models) and automated theorem proving. To do this, we suppose LLMs have an uncountable set of words in their domain and range. With this in mind, the results given in this paper use the downward and upward L\"owenheim–Skolem theorems to contrast the two modalities of AI that we use. One modality focuses on the syntax of proofs and the other focuses on logical semantics based on LLMs. Particularly, one modality uses a rule-based theorem-proving system to perform legal reasoning. The objective of this theorem-proving system is to provide proofs as evidence of valid legal reasoning. These proofs are syntactic structures that can be presented in court. The second modality uses large language models. An objective of our application of LLMs is to enhance and simplify user input and output for the theorem-proving system. In addition, the LLMs may help in the translation of the natural language tax law into rules for a theorem proving system. The combination of these two modalities empowers our vision. The LLMs provide notions of semantics for tax law inputs and they may help translate tax law statutes. While the theorem proving system gives syntactic proof-trees for legal arguments for potential justifications of tax claims.