TL;DR for operators The strongest result in this case study is not that an AI system wrote working Prolog. Across 33 targeted exercises, Claude generated 508 runtime tests alongside 257 lemmas and roughly 11,800 lines of proof, with the authors manually inspecting the generated files and an independent theorem prover checking the proofs. ...
TL;DR for operators Tax AI should not be judged by whether the model can produce a confident answer in fluent prose. That is how one builds a very polite liability machine. The useful pattern in this paper is architectural: let the language model translate statutory text and taxpayer facts into executable Prolog; let a symbolic solver compute the result; reject outputs that fail execution or disagree across independent attempts; then evaluate the system using an error-cost ledger, not just accuracy.1 The paper’s strongest practical message is therefore not “LLMs can do tax”. It is: high-stakes rule automation becomes more credible when the model is demoted from final authority to structured translator. ...