On the Potential and Limitations of Few-Shot In-Context Learning to Generate Metamorphic Specifications for Tax Preparation Software (2023)

Abstract: Due to the ever-increasing complexity of income tax laws in the United States, the number of US taxpayers filing their taxes using tax preparation software henceforth, tax software) continues to increase. According to the U.S. Internal Revenue Service (IRS), in FY22, nearly 50% of taxpayers filed their individual income taxes using tax software. Given the legal consequences of incorrectly filing taxes for the taxpayer, ensuring the correctness of tax software is of paramount importance. Metamorphic testing has emerged as a leading solution to test and debug legal-critical tax software due to the absence of correctness requirements and trustworthy datasets. The key idea behind metamorphic testing is to express the properties of a system in terms of the relationship between one input and its slightly metamorphosed twinned input. Extracting metamorphic properties from IRS tax publications is a tedious and time-consuming process. As a response, this paper formulates the task of generating metamorphic specifications as a translation task between properties extracted from tax documents - expressed in natural language - to a contrastive first-order logic form. We perform a systematic analysis on the potential and limitations of in-context learning with Large Language Models (LLMs) for this task, and outline a research agenda towards automating the generation of metamorphic specifications for tax preparation software.

## introduction recent surveys estimate that between 40 to 50% of taxpayers in the united states use tax preparation software to file their taxes @xcite . given the pervasive use of these systems and the penalties associated with filing taxes incorrectly @xcite , making sure that tax preparation software is free of bugs is of paramount importance. however, there are considerable challenges * equal contribution that make the application of standard software testing approaches infeasible in this domain. among these, the absence of correctness requirements and the lack of publicly available benchmarks (due to obvious privacy concerns) are primary obstacles to automatic testing and debugging of such systems. to address these challenges, tizpaz-niari et al. (2023) introduced a testing framework for u.s. tax preparation software guided by metamorphic relations. the authors define metamorphic relations as relations between two similar individuals who differ in key characteristics that put them in different tax income buckets. this way, they are able to evaluate the outcome of an individual taxpayer in comparison with individuals who are deemed similar to them. with the help of tax preparation experts, they were able to manually derive a comprehensive set of critical correctness properties of tax preparation outcomes expressed in first-order logic, and develop a search strategy to automatically generate test cases for an open-source tax preparation software. while their approach was successful, deriving formal metamorphic specifications is a time-consuming process that requires significant domain expertise. moreover, any changes to the tax code would require continuous efforts to make sure that specifications remain up to date. in this paper, we set out to explore whether recent advances in large language models (llms) @xcite @xcite can help reduce the manual effort required to derive metamorphic specifications for this domain. while supervised learning without sizeable training datasets is infeasible, recent findings show that llms can perform surprisingly well in few-shot scenarios for a wide variety of language tasks, including traditional nlp tasks like translation and question-answering @xcite , vision-language tasks @xcite , and socio-linguistic tasks like morality framing @xcite . to perform our study, we first define the extraction of metamorphic specifications for tax preparation software as a language to first-order logic translation task. to do this, we curate a dataset of 33 high-quality natural language properties derived from tax documents * and their corresponding formal logic representation @xcite . as curating these high-quality examples is expensive, we formulate the problem as a fewshot learning task and experiment with various incontext learning strategies to obtain a formal representation for each property. in-context learning is a task-adaptation technique that does not update the parameters of the llm, but rather primes the model response by providing a sequence of demonstrations @xcite . recent work has shown that in-context learning can lead to better out-of-domain performance than few-shot finetuning @xcite . we perform a comprehensive analysis of our results and show that using few-shot in-context learning, the model makes between 1-2 mistakes per property on average when generating predicates, variables and operators. while this is encouraging for a model that has barely seen any in-domain, tasks-specific data, there is a lot of room for improvement before these specifications are usable for automated testing. this work represents a first step towards the automated generation of metamorphic specifications for tax preparation software. in sec. 5 we outline a research agenda for this purpose. ## related work converting natural language utterances to logic forms has a long history in the natural language processing community. semantic parsing is a long-standing nlp task that looks at this problem @xcite . most of the work in this space has been either tailored to going from natural language to linguistically-motivated meaning representations @xcite , or to executable programs like sql queries @xcite and robotic commands @xcite . the solutions employed for these domains are not readily applicable to our case. on the one hand, datasets for linguistically motivated meaning representations usually deal with simple general utterances, and their struc-tured forms are very distinct from the structured forms needed for automated software verification. on the other hand, executable domains like sql have the advantage that there are large-scale, readily available repositories of in-domain data, which is not the case for low-resource, closed domains like tax preparation software. more recently, there has been increased interest in exploring nlp techniques to derive formal specifications from technical documentation ## task description metamorphic testing is a well-studied strategy in the systems community @xcite . it was developed to circumvent the absence of oracles (i.e., black box modules that decide whether the output of the system is correct for a given input). the main idea behind metamorphic testing is that correctness can be established by contrasting multiple input-output behaviors @xcite . the running example is search-engine validation; while it might be impossible to know the expected items that should be returned for any search query q, if we have a more restrictive query q 0 , we know that the number of retrieved items for q should be greater than the number of retrieved items for q 0 . this allows for developing strategies to test whether systems satisfy the metamorphic relations. to formulate our task, we build on the definition of metamorphic specifications for tax-preparation software proposed by @xcite . we have a fixed set p of metamorphic properties written in natural language, expressing aspects of the u.s. individual income tax returns that relate to disability, credits, and deductions. for each property p 2 p , we want to synthesize a specification s in first-order logic that captures the metamorphic property. fig. 1 shows an example of the input and expected output. in appendix a, we detail the syntax and semantics of metamorphic specifications used for the tax preparation software, as well as the input: property output: specification an individual with the married filing jointly (mf j) status with a disabled spouse must receive similar or higher tax benefits compared to a similar individual but without the disabled spouse. 8x(x.@xmath0.s_blind ¬y.s_blind)) =) f(x) f(y) ## experimental evaluation in this section, we evaluate the performance of llms on the natural language to metamorphic specifications translations. we first outline the evaluation dimensions that we consider, then we describe our experimental setup and results.