稅務系統高度依賴法規規則與數值計算，涉及法定公式、申報年度常數、使用者事實資料，以及可能影響實際財務決策的計算目標。因此，實用的稅務規劃系統不能只提供自然語言解釋，還必須能重現官方計算器行為、搜尋符合法規限制的可行解空間，並保留可稽核的計算紀錄。本文提出一個用於稅務規劃的代理式神經符號框架，結合大型語言模型、官方入口網站驗證，以及形式化約束求解與最佳化方法。系統中的神經層負責法條生成、欄位對齊與自然語言互動；符號層則由經驗證的求解器組成，用以執行法定規則、最佳化規劃目標，並提供可驗證的計算結果。
本系統根據財政部電子申報服務入口網站的欄位結構與檢索到的法規條文，建構與官方計算器對齊的稅務求解器，並透過自動化差異測試與官方入口網站進行比對驗證。當求解器通過官方行為一致性驗證後，系統會將使用者目標轉換為受欄位結構限制的最佳化任務。本文也加入最佳化後診斷層，在求解器算出最佳解後，檢查是否仍存在更佳解，並分析哪些官方預設假設可能阻擋進一步改善，同時避免放寬使用者原始限制與事實輸入。
實驗結果顯示，本文產生的稅務求解器能在多種台灣稅制上達到與官方計算器一致的計算行為，並能處理自然語言形式的稅務規劃任務。相較於僅依賴大型語言模型的方式，本文方法能提供更穩定且可驗證的最佳化結果。整體而言，本文展示了一個適用於稅法計算與稅務規劃的神經符號模式：大型語言模型提供介面理解與合成輔助，官方驗證與符號求解器則提供可執行的正確性、最佳化能力與可解釋的計算結果。

Tax systems are legal-critical software artifacts: they encode statutory formulas, filing-year constants, user-provided facts, and objective functions whose outputs may affect real financial decisions. A useful tax-planning system must therefore do more than produce plausible natural-language explanations; it must reproduce official calculator behavior, search the compliant solution space, expose auditable artifacts, and explain why an optimized result cannot be improved under the user's assumptions. This thesis presents an agentic neuro-symbolic framework for taxation planning that combines large language models (LLMs), official-portal oracle validation, and Satisfiability Modulo Theories/Optimization Modulo Theories (SMT/OMT) solving. The neural layer assists with statute-conditioned drafting, schema grounding, natural-language intent translation, and report generation, while the symbolic layer consists of validated Python+Z3 solver artifacts that execute statutory rules, optimize planning objectives, and provide replayable diagnostic evidence. The system first constructs portal-aligned Python+Z3 tax solvers from Ministry of Finance (MoF) eTax schemas and retrieved statutes, then validates each candidate against the official portal through Selenium-based differential testing and a developer-guided draft--check--patch loop. After oracle parity is reached, the validated solver backbone is exposed through a guarded planning agent that translates user goals into schema-constrained optimization tasks. Beyond calculator parity and optimization, this thesis adds a traced post-optimality diagnostic layer: after Z3 computes an optimum, the system proves that no strictly better solution exists, extracts an unsat core, and tests which zero-valued portal-default assumptions block further improvement without relaxing user constraints, budget caps, free variables, or nonzero factual inputs. Across ten Taiwanese tax regimes, the resulting solvers achieve calculator-level fidelity and solve 20 natural-language planning tasks with 100\% exact optimality, while web-based LLM baselines reach 35--45\%. The diagnostic experiments further show that default-only unsat-core release analysis preserves scenario semantics, that core-guided candidate selection finds effective releases with fewer solver calls than exhaustive or random baselines, and that effective releases requiring realistic bounds can be converted into bounded what-if scenarios whose conservative median improvement is 97,500 NTD. These results demonstrate a practical neuro-symbolic pattern for legal-critical software: LLMs provide interface and synthesis assistance, while official oracles and symbolic solvers provide executable correctness, optimization, and auditable post-optimality explanations.

J. Ahlgren, M. E. Berezin, K. Bojarczuk, et al., “Testing web enabled sim- ulation at scale using metamorphic testing,” in 2021 IEEE/ACM 43rd In- ternational Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), IEEE, 2021, pp. 140–149 (cit. p. 12).
J. Austin, A. Odena, M. Nye, et al., Program synthesis with large language models, 2021. arXiv: 2108.07732 [cs.PL] (cit. p. 2).
J. Aslett, “Understanding Artificial Intelligence in Tax and Customs Ad- ministration,” Technical Notes and Manuals, vol. 2024, no. 006, p. 1, Nov. 2024 (cit. p. 1).
R. Brummayer and A. Biere, “Boolector: An efficient smt solver for bit- vectors and arrays,” in Tools and Algorithms for the Construction and Anal- ysis of Systems, S. Kowalewski and A. Philippou, Eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2009, pp. 174–177 (cit. p. 11).
H. Barbosa, C. Barrett, M. Brain, et al., “Cvc5: A versatile and industrial- strength smt solver,” in Tools and Algorithms for the Construction and Analysis of Systems, D. Fisman and G. Rosu, Eds., Cham: Springer Inter- national Publishing, 2022, pp. 415–442 (cit. p. 11).
S. Badreddine, A. d’Avila Garcez, L. Serafini, and M. Spranger, “Logic tensor networks,” Artificial Intelligence, vol. 303, p. 103 649, 2022 (cit. p. 7).
E. T. Barr, M. Harman, P. McMinn, M. Shahbaz, and S. Yoo, “The oracle problem in software testing: A survey,” IEEE Transactions on Software Engineering, vol. 41, no. 5, pp. 507–525, 2015 (cit. p. 12).
N. Bjørner, A.-D. Phan, and L. Fleckenstein, “νZ - an optimizing smt solver,” in Tools and Algorithms for the Construction and Analysis of Sys- tems, C. Baier and C. Tinelli, Eds., Berlin, Heidelberg: Springer Berlin Hei- delberg, 2015, pp. 194–199 (cit. pp. 3, 11).
R. Bairi, A. Sonwane, A. Kanade, et al., “Codeplan: Repository-level cod- ing using llms and planning,” Proceedings of the ACM on Software Engi- neering, vol. 1, no. FSE, 2024 (cit. p. 13).
A. Cimatti, A. Griggio, B. J. Schaafsma, and R. Sebastiani, “The mathsat5 smt solver,” in Tools and Algorithms for the Construction and Analysis of Systems, N. Piterman and S. A. Smolka, Eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 93–107 (cit. p. 11).
M. Chen, G. Li, L.-I. Wu, et al., Can language models pretend solvers? logic code simulation with llms, 2024. arXiv: 2403.16097 [cs.AI] (cit. pp. 2, 10).
J. Chen, H. Li, J. Yang, Y. Liu, and Q. Ai, Enhancing LLM-based agents via global planning and hierarchical execution, 2025. arXiv: 2504.16563 [cs.AI] (cit. p. 8).
L. de Moura and N. Bjørner, “Z3: An efficient smt solver,” in Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakr- ishnan and J. Rehof, Eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 337–340 (cit. p. 11).
C. Deng, K. Mao, Y. Zhang, and Z. Dou, “Enabling discrimina- tive reasoning in llms for legal judgment prediction,” arXiv preprint arXiv:2407.01964, 2024 (cit. p. 6).
X. Du, M. Wen, J. Zhu, et al., “Generalization-enhanced code vulnerability detection via multi-task instruction fine-tuning,” in Findings of the Asso- ciation for Computational Linguistics: ACL 2024, L.-W. Ku, A. Martins, and V. Srikumar, Eds., Bangkok, Thailand: Association for Computational Linguistics, Aug. 2024, pp. 10 507–10 521 (cit. p. 10).
R. Ehsani, E. Parra, S. Haiduc, and P. Chatterjee, Hierarchical knowledge injection for improving llm-based program repair, 2025. arXiv: 2506.24 015 [cs.SE] (cit. p. 10).
Ł. Górski, B. Kuzniacki, M. Almada, et al., “Exploring explainable ai in the tax domain,” Artificial Intelligence and Law, pp. 1–29, May 2024 (cit. p. 1).
N. Guha, J. Nyarko, D. Ho, et al., “LegalBench: A Collaboratively Built Benchmark for Measuring Legal Reasoning in Large Language Models,” in Advances in Neural Information Processing Systems, A. Oh, T. Nau- mann, A. Globerson, et al., Eds., vol. 36, Curran Associates, Inc., 2023, pp. 44 123–44 279 (cit. p. 6).
S. Gogani-Khiabani, A. Trivedi, D. Saha, and S. Tizpaz-Niari, “An llm agentic approach for legal-critical software: A case study for tax prep soft- ware,” in Proceedings of the 48th International Conference on Software Engineering (ICSE 2026), 2026. arXiv: 2509.13471 [cs.SE] (cit. pp. 3, 12, 19).
S. B. Hakim, M. Adil, A. Velasquez, and H. H. Song, “Neuro-symbolic agentic ai: Architectures, integration patterns, applications, open chal- lenges and future research directions,” Computer Science Review, vol. 60, p. 100 902, 2026 (cit. pp. 2, 7–9).
Y. Hao, Y. Chen, Y. Zhang, and C. Fan, Large language models can solve real-world planning rigorously with formal verification tools, 2025. arXiv: 2404.11891 [cs.AI] (cit. p. 2).
S. Hong, M. Zhuge, J. Chen, et al., “MetaGPT: Meta programming for a multi-agent collaborative framework,” in International Conference on Learning Representations, 2024 (cit. p. 8).
D. Huang, J. M. Zhang, M. Luck, et al., Agentcoder: Multi-agent-based code generation with iterative testing and optimisation, 2023. arXiv: 2312 .13010 [cs.SE] (cit. p. 13).
S. Judson, M. Elacqua, F. Cano, et al., “Soid: A tool for legal accountabil- ity for automated decision making,” in Computer Aided Verification, A. Gurfinkel and V. Ganesh, Eds., Cham: Springer Nature Switzerland, 2024, pp. 233–246 (cit. p. 25).
Kognitos, What is neurosymbolic ai? the technology behind hallucination- free automation, https://www.kognitos.com/blog/what-is-neuros ymbolic-ai/, Accessed: 2026-07-06, 2026 (cit. pp. 2, 9).
S. Kapoor, B. Stroebl, Z. S. Siegel, N. Nadgir, and A. Narayanan, AI agents that matter, 2024. arXiv: 2407.01502 [cs.AI] (cit. p. 8).
Y. Li, A. Albarghouthi, Z. Kincaid, A. Gurfinkel, and M. Chechik, “Sym- bolic optimization with smt solvers,” in Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’14, San Diego, California, USA: Association for Computing Machinery, 2014, pp. 607–618 (cit. pp. 3, 11).
J. Lai, W. Gan, J. Wu, Z. Qi, and P. S. Yu, Large language models in law: A survey, 2023. arXiv: 2312.03718 [cs.CL] (cit. p. 6).
A. Louis, G. van Dijck, and G. Spanakis, “Interpretable long-form legal question answering with retrieval-augmented large language models,” Pro- ceedings of the AAAI Conference on Artificial Intelligence, vol. 38, no. 20, pp. 22 266–22 275, Mar. 2024 (cit. p. 6).
X. Liang, H. Wang, Y. Wang, et al., Controllable text generation for large language models: A survey, 2024. arXiv: 2408.12599 [cs.CL] (cit. p. 10).
T. Masterman, S. Besen, M. Sawtell, and A. Chao, The landscape of emerg- ing AI agent architectures for reasoning, planning, and tool calling: A sur- vey, 2024. arXiv: 2404.11584 [cs.AI] (cit. p. 8).
N. Panickssery, N. Gabrieli, J. Schulz, et al., Steering llama 2 via con- trastive activation addition, 2024. arXiv: 2312.06681 [cs.CL] (cit. p. 10).
P. Putta, E. Mills, N. Garg, et al., Agent Q: Advanced reasoning and learn- ing for autonomous AI agents, 2024. arXiv: 2408.07199 [cs.AI] (cit. p. 8).
R. Riegel, A. Gray, F. Luus, et al., Logical neural networks, 2020. arXiv: 2006.13155 [cs.AI] (cit. p. 7).
N. Shinn, F. Cassano, A. Gopinath, K. Narasimhan, and S. Yao, “Reflex- ion: Language agents with verbal reinforcement learning,” in Advances in Neural Information Processing Systems, vol. 36, 2023, pp. 8634–8652 (cit. pp. 8, 13).
D. Srinivas, R. Das, S. Tizpaz-Niari, A. Trivedi, and M. L. Pacheco, “On the potential and limitations of few-shot in-context learning to generate metamorphic specifications for tax preparation software,” in Proceedings of the Natural Legal Language Processing Workshop 2023, Association for Computational Linguistics, 2023, pp. 231–245. arXiv: 2311.11979 [cs.SE] (cit. pp. 3, 12, 29).
R. Sebastiani and P. Trentin, “Optimathsat: A tool for optimization mod- ulo theories,” in International conference on computer aided verification, Springer, 2015, pp. 447–454 (cit. p. 11).
Z. Sun, K. Zhang, W. Yu, H. Wang, and J. Xu, “Logic rules as explanations for legal case retrieval,” in Proceedings of the 2024 Joint International Conference on Computational Linguistics, Language Resources and Eval- uation (LREC-COLING 2024), N. Calzolari, M.-Y. Kan, V. Hoste, et al., Eds., Torino, Italia: ELRA and ICCL, May 2024, pp. 10 747–10 759 (cit. p. 6).
N. Tsiskaridze, C. Barrett, and C. Tinelli, Generalized optimization modulo theories, 2024. arXiv: 2404.16122 [cs.LO] (cit. p. 11).
S. Tizpaz-Niari, S. Darian, and A. Trivedi, Metamorphic debugging for accountable software, 2024. arXiv: 2409.16140 [cs.SE] (cit. pp. 12, 29).
S. Tizpaz-Niari, V. Monjezi, M. Wagner, et al., “Metamorphic testing and debugging of tax preparation software,” in 2023 IEEE/ACM 45th Interna- tional Conference on Software Engineering: Software Engineering in Soci- ety (ICSE-SEIS), IEEE, 2023, pp. 138–149. arXiv: 2205.04998 [cs.SE] (cit. pp. 3, 12, 19).
T. H. Trinh, Y. Wu, Q. V. Le, H. He, and T. Luong, “Solving olympiad geometry without human demonstrations,” Nature, vol. 625, pp. 476–482, 2024 (cit. p. 8).
M. van Bekkum, M. de Boer, F. van Harmelen, A. Meyer-Vitali, and A. ten Teije, “Modular design patterns for hybrid learning and reasoning sys- tems: A taxonomy, patterns and use cases,” Applied Intelligence, vol. 51, pp. 6528–6546, 2021 (cit. p. 7).
W. Wang, K. Liu, A. R. Chen, et al., Python symbolic execution with llm- powered code generation, 2024. arXiv: 2409.09271 [cs.SE] (cit. p. 2).
J. Wang, X. Xie, Q. Hu, et al., Defects4c: Benchmarking large language model repair capability with c/c++ bugs, 2025. arXiv: 2510 . 11059 [cs.SE] (cit. pp. 3, 10).
X. Wang, X. Zhang, V. Hoo, Z. Shao, and X. Zhang, “Legalreasoner: A multi-stage framework for legal judgment prediction via large language models and knowledge integration,” IEEE Access, vol. 12, pp. 166 843– 166 854, 2024 (cit. p. 3).
C. S. Xia, Y. Deng, S. Dunn, and L. Zhang, Agentless: Demystifying llm- based software engineering agents, 2024. arXiv: 2407.01489 [cs.SE] (cit. p. 3).
B. Xu, X. Liu, H. Shen, et al., “Gentopia.ai: A collaborative platform for tool-augmented llms,” in Proceedings of the 2023 Conference on Empir- ical Methods in Natural Language Processing: System Demonstrations, Association for Computational Linguistics, 2023, pp. 237–245 (cit. p. 13).
W. Yuan, J. Cao, Z. Jiang, et al., Can large language models grasp legal theories? enhance legal reasoning with insights from multi-agent collabo- ration, 2024. arXiv: 2410.02507 [cs.AI] (cit. p. 6).
W. Yu, R. Mangal, T. Zhuo, M. Fredrikson, and C. S. Pasareanu, A mix- ture of linear corrections generates secure code, 2025. arXiv: 2507.0950 8 [cs.CR] (cit. p. 9).
F. Yu, L. Quartey, and F. Schilder, “Exploring the effectiveness of prompt engineering for legal reasoning tasks,” in Findings of the Association for Computational Linguistics: ACL 2023, A. Rogers, J. Boyd-Graber, and N. Okazaki, Eds., Toronto, Canada: Association for Computational Linguis- tics, Jul. 2023, pp. 13 582–13 596 (cit. p. 2).
B. Yang, H. Tian, J. Ren, et al., “Morepair: Teaching llms to repair code via multi-objective fine-tuning,” ACM Transactions on Software Engineering and Methodology, May 2025 (cit. pp. 3, 10).
A. Z. H. Yang, H. Tian, H. Ye, R. Martins, and C. L. Goues, Security vul- nerability detection with multitask self-instructed fine-tuning of large lan- guage models, 2024. arXiv: 2406.05892 [cs.CR] (cit. p. 10).
S. Yao, J. Zhao, D. Yu, et al., “React: Synergizing reasoning and acting in language models,” in International Conference on Learning Representa- tions, 2023 (cit. pp. 8, 13).
A. Zou, L. Phan, S. Chen, et al., Representation engineering: A top-down approach to ai transparency, 2025. arXiv: 2310 . 01405 [cs.LG] (cit. p. 10).
K. Zhang, W. Yu, Z. Sun, and J. Xu, An explicit syllogistic legal reasoning framework for large language models, 2025. arXiv: 2504.04042 [cs.CL] (cit. p. 6).