| dc.contributor | 資管系 | - |
| dc.creator (作者) | 郁方 | - |
| dc.creator (作者) | Hwang, Ting Chien;Yu, Fang;Jiang, Jie-Hong Roland | - |
| dc.date (日期) | 2026-04 | - |
| dc.date.accessioned | 11-Feb-2026 09:26:49 (UTC+8) | - |
| dc.date.available | 11-Feb-2026 09:26:49 (UTC+8) | - |
| dc.date.issued (上傳時間) | 11-Feb-2026 09:26:49 (UTC+8) | - |
| dc.identifier.uri (URI) | https://ah.lib.nccu.edu.tw/item?item_id=181260 | - |
| dc.description.abstract (摘要) | Tax systems are inherently complex, governed by many numerical parameters and frequently updated statutory rules. For taxpayers, correctly computing and optimizing liability is difficult and error-prone from text alone. We propose a two-layer framework that integrates large language models (LLMs) with Satisfiability Modulo Theories (SMT) solving to support tax computation and planning. In the first layer, a law-first Retrieval-Augmented Generation (RAG) pipeline retrieves relevant clauses and portal rules, which guide LLM-assisted drafting of Python+Z3 calculators that mirror the Ministry of Finance (MoF) eTax input/output schema and encode brackets, thresholds, deductions, and caps. Drafts are not assumed correct: we employ oracle-gated differential testing against the official MoF calculator and refine the constraint code through an iterative draft–check–patch workflow that is developer-guided (with optional LLM assistance) until portal parity is reached. In the second layer, the verified constraint backbone is connected to Z3 Optimize to explore the compliant solution space under user goals and constraints, and is exposed via a guarded agentic service that translates natural-language requests into schema-constrained solver calls and produces auditable optimization reports. Across ten Taiwanese tax regimes, the resulting solvers achieve calculator-level fidelity and enable reliable tax minimization and budget-bounded planning. | - |
| dc.format.extent | 91082 bytes | - |
| dc.format.mimetype | application/pdf | - |
| dc.relation (關聯) | ICSE-SEIP '26: Proceedings of the IEEE/ACM 48th International Conference on Software Engineering: Software Engineering in Practice, IEEE/ACM SIGSOFT, pp.797-807 | - |
| dc.subject (關鍵詞) | tax computation; SMT solving; optimization modulo theories; Z3;
large language models; agentic systems; oracle-gated validation | - |
| dc.title (題名) | Agentic Taxation Optimization via LLM SMT-Constraint Reasoning | - |
| dc.type (資料類型) | conference | - |
| dc.identifier.doi (DOI) | 10.1145/3786583.3786917 | - |
| dc.doi.uri (DOI) | https://doi.org/10.1145/3786583.3786917 | - |
