CUTECat: Concolic Execution for Computational Law

• URL: http://arxiv.org/abs/2410.18212v2
• Date: Thu, 23 Jan 2025 10:10:41 GMT
• Title: CUTECat: Concolic Execution for Computational Law
• Authors: Pierre Goutagny, Aymeric Fromherz, Raphaël Monat,
• Abstract summary: We show how to handle default logic inside a concolic execution tool, and implement our approach in the context of Catala.<n>We evaluate the Catala implementation of the French housing benefits and Section 132 of the US tax code.
• Score: 1.1077637528502942
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Many legal computations, including the amount of tax owed by a citizen, whether they are eligible to social benefits, or the wages due to civil state servants, are specified by computational laws. Their application, however, is performed by expert computer programs intended to faithfully transcribe the law into computer code. Bugs in these programs can lead to dramatic societal impact, e.g., paying employees incorrect amounts, or not awarding benefits to families in need. To address this issue, we consider concolic unit testing, a combination of concrete execution with SMT-based symbolic execution, and propose CUTECat, a concolic execution tool targeting implementations of computational laws. Such laws typically follow a pattern where a base case is later refined by many exceptions in following law articles, a pattern that can be formally modeled using default logic. We show how to handle default logic inside a concolic execution tool, and implement our approach in the context of Catala, a recent domain-specific language tailored to implement computational laws. We evaluate CUTECat on several programs, including the Catala implementation of the French housing benefits and Section 132 of the US tax code. We show that CUTECat can successfully generate hundreds of thousands of testcases covering all branches of these bodies of law. Through several heuristics, we improve CUTECat's scalability and usability, making the testcases understandable by lawyers and programmers alike. We believe CUTECat thus paves the way for the use of formal methods during legislative processes.

Related papers

• Specification languages for computational laws versus basic legal principles [0.0]
  We speak of a textitcomputational law when that law is intended to be enforced by software through an automated decision-making process. In this paper, we investigate how certain legal principles fare in both scenarios: computational law written in natural language or written in formal language.
  arXiv  Detail & Related papers  (2025-03-12T07:39:27Z)
• Bayesian scaling laws for in-context learning [72.17734205418502]
  In-context learning (ICL) is a powerful technique for getting language models to perform complex tasks with no training updates. We show that ICL approximates a Bayesian learner and develop a family of novel Bayesian scaling laws for ICL.
  arXiv  Detail & Related papers  (2024-10-21T21:45:22Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  Large language models (LLMs) of code are typically trained on the surface textual form of programs. We propose NExT, a method to teach LLMs to inspect the execution traces of programs and reason about their run-time behavior.
  arXiv  Detail & Related papers  (2024-04-23T01:46:32Z)
• Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
  We propose Chain of Code, a simple yet surprisingly effective extension that improves LM code-driven reasoning. The key idea is to encourage LMs to format semantic sub-tasks in a program as flexible pseudocode that the interpreter can explicitly catch.
  arXiv  Detail & Related papers  (2023-12-07T17:51:43Z)
• 'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions [4.170056099990699]
  We show that under minimal assumptions automated reasoning can rigorously interrogate algorithmic behaviors. We model accountability processes, such as trials or review boards, as Counterfactual-Guided Logic Exploration and Abstraction Refinement loops. We implement our framework and demonstrate its utility on an illustrative car crash scenario.
  arXiv  Detail & Related papers  (2023-05-09T19:23:47Z)
• LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
  We propose LEVER, a simple approach to improve language-to-code generation by learning to verify the generated programs with their execution results. Specifically, we train verifiers to determine whether a program sampled from the LLMs is correct or not based on the natural language input, the program itself and its execution results. LEVER consistently improves over the base code LLMs(4.6% to 10.9% with code-davinci) and achieves new state-of-the-art results on all of them.
  arXiv  Detail & Related papers  (2023-02-16T18:23:22Z)
• CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version) [12.790826917588575]
  cryptography has been an exception, where many performance-critical routines have been written directly in assembly. We present CryptOpt, the first compilation pipeline that specializes high-level cryptographic functional programs into assembly code significantly faster than what GCC or Clang produce. On the formal-verification side, we connect to the FiatOpt framework (which translates functional programs into C-like IR code) and extend it with a new formally verified program-equivalence checker.
  arXiv  Detail & Related papers  (2022-11-19T11:07:39Z)
• Law Informs Code: A Legal Informatics Approach to Aligning Artificial Intelligence with Humans [0.0]
  Law-making and legal interpretation form a computational engine that converts opaque human values into legible directives. "Law Informs Code" is the research agenda capturing complex computational legal processes, and embedding them in AI.
  arXiv  Detail & Related papers  (2022-09-14T00:49:09Z)
• The Dangers of Computational Law and Cybersecurity; Perspectives from Engineering and the AI Act [1.332091725929965]
  Computational Law has begun taking the role in society which has been predicted for some time. In this paper we go through known issues and discuss them in the various levels, from design to the physical realm. We present three recommendations which are necessary for computational law to function globally.
  arXiv  Detail & Related papers  (2022-07-01T09:42:11Z)
• Metamorphic Testing and Debugging of Tax Preparation Software [2.185694185279913]
  We focus on an open-source tax preparation software for our case study. We develop a randomized test-case generation strategy to systematically validate the correctness of tax preparation software.
  arXiv  Detail & Related papers  (2022-05-10T16:10:10Z)
• Natural Language to Code Translation with Execution [82.52142893010563]
  Execution result--minimum Bayes risk decoding for program selection. We show that it improves the few-shot performance of pretrained code models on natural-language-to-code tasks.
  arXiv  Detail & Related papers  (2022-04-25T06:06:08Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  We propose a retrieval-augmented code completion framework, leveraging both lexical copying and referring to code with similar semantics by retrieval. We evaluate our approach in the code completion task in Python and Java programming languages, achieving a state-of-the-art performance on CodeXGLUE benchmark.
  arXiv  Detail & Related papers  (2022-03-15T08:25:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.