Source-linked AI summary
Implementing Computational Law in Wolfram Language for the Governance of Artificial Intelligence
James K. Wiles
TL;DR
Bridging English legal rules and fully formal computational logic is difficult because complete formality is impractical for ordinary legal drafting. The paper implements Reified Input/Output Logic, tests GPT-4 translations, and demonstrates contract rules operating in an AI guard dog; three of four accepted translations contained silent semantic errors.
Problem
Bridging English legal rules and fully formal computational logic is difficult because complete formality is impractical for ordinary legal drafting.
Method
The paper implements Reified Input/Output Logic in Wolfram Language, evaluates GPT-4 translations, and connects contractual rules to an embodied agent’s operational code.
Results
Three of four accepted GPT-4 translations carried silent semantic errors, while the formalism handled disjunction, reified negation, temporal scope, and nested obligations.
Takeaways & Limitations
A workable governance pipeline has LLMs draft translations, formal systems verify them, and humans adjudicate the results.
Takeaways & Limitations
This exploratory study covers four statements, one January 2024 model, one session, no repeated trials, and author judgment, yielding an existence proof rather than a benchmark score.
Abstract
from arXiv · showhide
How do we govern AI systems whose reasoning we cannot fully inspect? Governance does not require understanding a system's reasoning. It requires stating what the system is obliged, permitted, and forbidden to do, and checking whether it complied. I present an implementation of Reified Input/Output Logic, the formalism behind the DAPRECO knowledge base, in Wolfram Language: the core I/O axioms, obligations, permissions, constitutive norms, reified eventualities, and temporal operators. I then test whether GPT-4 can translate English legal statements into the formalism, and report the failures: hallucinated functions, omitted temporal scope, deviation from the formalism, and (in the worst cases) code that runs, reads plausibly, but silently encodes the wrong norm. A case study, an AI guard dog operating under a computational contract, shows how formalized rules can extend from a contract directly into the operational code of an embodied agent, producing symbolic, auditable justifications for its behaviour. I argue that computational law can be used as a governance tool and that a desirable goal would be to formalize the law that can and ought to be programmatically executable.
1 Introduction
Governance of black-box AI can proceed by specifying and checking obligations, permissions, and prohibitions without inspecting internal reasoning. The paper explores executable computational law through a Wolfram Language implementation, GPT-4 translation tests, and an AI-agent case study.
- Motivation: Governance need not await interpretability: it can state what an AI system is obliged, permitted, or forbidden to do and check compliance.The introduction contrasts understanding internal reasoning with specifying externally checkable requirements.
- Problem and contribution: Computational law addresses ambiguity in human-language statutes, contracts, and judgments by encoding legal reasoning as executable code.The paper proposes writing laws that AI systems can directly execute rather than relying on their interpretation of written law.
- Contributions: The paper implements the core of Reified Input/Output Logic, the formalism behind the DAPRECO knowledge base, in Wolfram Language.This is presented as an exploratory implementation study rather than a systematic evaluation.
- Contributions: Three of four GPT-4 translations ran and looked correct while silently encoding the wrong norm.Two imposed obligations on the wrong people, one despite correct comments, and one measured legal compliance with the wrong geometry.
- Contributions: A case study extends a computational contract into the operational code of an AI agent, specifically a robotic guard dog.The introduction identifies this case study as a contribution alongside the implementation and GPT-4 translation test.
2 Background
Computational law automates legal reasoning and compliance management, but translating ambiguous human legal language into reliable formal rules remains difficult. Reified I/O Logic, together with related standards and distinctions among norm types, provides a formal foundation for representing executable legal norms.
- Computational law and compliance: Computational law primarily focuses on compliance management, with tax software succeeding because its inputs, outputs, facts, and reasoning are largely digitised and arithmetic.The field develops systems that assess, facilitate, or enforce compliance with rules and regulations.
- Motivation: AI may become a forcing function for computational law, following regulatory pressures such as the GDPR and post-2008 financial regulation that stimulated tools, research, and knowledge bases.The DAPRECO knowledge base is identified as a direct product of GDPR-driven investment.
- Language and input: Ambiguous human language and unsafe user input make computational law difficult because legal evidence arrives as quotes, testimonies, and descriptions rather than clean machine-readable data.Legal language can encode vagueness, context dependence, and potentially consequential imprecision, while user-supplied text may deliberately or accidentally break software assumptions.
- Related standards: Machine-processable legal standards include Akoma Ntoso for legal documents, LegalRuleML for logical rule content, and OWL 2 for precise domain ontologies.LegalRuleML is the encoding format used by the DAPRECO knowledge base.
- Formal foundations: Reified I/O Logic represents conditions and normative conclusions as input/output pairs while reification turns events, states, and processes into recursively referable objects.The formalism supports obligations, permissions, and definitions, and underlies DAPRECO’s formalization of GDPR provisions over the PrOnto ontology.
- Norm types: Regulative norms direct behaviour, whereas constitutive norms create the institutional facts on which regulative norms operate; separating them is practically important.The paper notes that GPT-4 later hard-coded a classification where a constitutive norm was required.
3 Reified I/O Logic in Wolfram Language
The implementation represents legal reasoning as Wolfram Language rewrite rules, extending them with I/O axioms, norm types, reified eventualities, temporal operators, and ABox/TBox distinctions. Its formal transparency supports symbolic, inspectable reasoning, but the resulting expressions are difficult for lawyers to write and motivate an English-to-formalism bridge.
- I/O pairs and axioms: Wolfram Language rewrite rules directly represent Input/Output pairs, with legal bodies as rule lists and scenarios transformed by rule replacement.The basic unit of the formalism coincides with a language primitive.
- I/O pairs and axioms: The implemented axioms strengthen inputs, weaken outputs, combine shared inputs, preserve provenance through identity, and repair cumulative-transitivity paradoxes by combining outputs.Disjunction is implemented but avoided because it discards which condition produced the output; Output Equivalence remains unimplemented.
- Norm types: Legal reasoning uses obligation, permission, and constitutive norm sets, with constitutive rules chaining raw facts into institutional facts and then deontic conclusions.For example, signedContract can imply isEmployee, which can imply canAccessOffice through the same rewrite mechanism.
- Reification and time: Reified eventualities are inert symbolic expressions that can be inspected structurally, while temporal operators represent existence, disjunction, and negation at specified times.RexistAtTime keeps outputs symbolic implications rather than truth values, supporting reasoning about hypothetical norms.
- ABox/TBox and formalization limits: ABox/TBox typing separates factual statements from logically structured, temporally scoped rules, but full formal expressions remain difficult for lawyers to write despite direct Wolfram Language rendering.This difficulty motivates using a machine that reads English fluently to bridge English and formal expressions.
4 Bridging the gap with LLMs
The exploratory GPT-4 study shows that LLMs can generate readable Reified I/O candidates, but they also produce temporal omissions, formalism drift, hallucinated APIs, and silent semantic errors. The resulting division of labour is candidate generation by the model and executable human verification, not autonomous formalization.
- Study design: The study used four statements, one ChatGPT-4 version, one unrepeated session, and author judgment, yielding an existence proof and failure catalogue rather than a benchmark.Three failures were discovered only while preparing the paper.
- Failure modes: GPT-4 correctly represented Statement A’s conditions, obligation, disjunction, and I/O pair, but its checker returned True for every input because the conditions never evaluated.A follow-up appeared correct only by coincidence, and neither the model nor author noticed the bug at the time.
- Failure modes: The translations omitted temporal scope, conflated constitutive classification with regulative obligation, and sometimes encoded meta-level conditions incorrectly.For Statement C, the code ignored the manager argument and triggered obligations for anyone whenever the action appeared in a global list.
- Failure modes: Four recurring failures were hallucinated functions, temporal omission, formalism drift, and silent semantic errors, with the last category surviving plausible code and motivated review three times.Hallucinated functions fail loudly, whereas silent errors require discriminating tests and comparison against expected outputs.
- Assessment: The model responded well to correction within two or three rounds and produced readable candidate formalizations, making it useful as a productivity tool.The proposed workflow is for humans to verify generated candidates against executable test cases, including verifying the tests themselves.
5 Case study: Fluffy
Fluffy demonstrates a computational contract whose executable rules connect sensor-derived facts to autonomous decisions and auditable normative outputs. The case also exposes verification failures and limits, including silent misformalization, unresolved conflicts, actuator enforcement, and interpretation at the English-to-formal boundary.
- Code as contract: Fluffy’s contract extends into its operational code, making the formalization both the legal document and the robot’s operational constraint.This removes developer approximation as an intermediate layer, while leaving gaps between English intent, formalization, symbolic conclusions, and actuators.
- Real-world grounding: Sensor data becomes symbolic facts that legal rules consume directly, linking camera detections, geographic distances, and named entities to normative evaluation.The demonstration uses FindFaces on a camera image and a Wolfram Language entity for the home.
- Auditable behaviour: The rules distinguish obligations, violations, permissions, and their negations, producing auditable deontic positions that control actions and expose symbolic justifications to human auditors.Taser use is affirmatively permitted rather than merely unforbidden, while the boundary rule changes from a standing obligation to a violation outside 200 meters.
- Verification: Five scenarios matched the contract’s intent, but the original harness falsely reported failures because its assertions demanded one conclusion instead of each scenario’s full expected output list.The corrected harness asserted complete expected outputs, and all five scenarios passed.
- Verification: The case contrasts noisy false alarms from the Fluffy harness with GPT-4’s silent wrong norms, showing why executable compliance rules require independent checking.The harness’s failure pointed to itself despite correct behaviour, whereas GPT-4’s Statements A, C, and D encoded wrong behaviour without an alarm.
- Limitations: The demonstration uses static snapshots and resolves neither conflicting obligations nor enforcement, while actions such as “stop” still require interpretation.A deployed system would need continuous fact updates and re-evaluation; the formalization determines what Fluffy should do but not how actuators enforce it.
6 Governance, enforcement, and the limits of law
Computational law governs deployed AI by specifying and verifying machine behaviour, but enforcement depends on controlling energy, information, and compute rather than merely formalizing rules. Its practical scope is selective: executable rules are valuable for safety-critical systems, while much law remains too vague, contradictory, or context-dependent to encode.
- Governance and enforcement: Computational law governs deployed machines by specifying and verifying behaviour without depending on how they work internally or who built them.It is distinct from governance of the AI field, which concerns training data, compute, research directions, and the humans building systems.
- Governance and enforcement: Formalization establishes what rules require and whether they were followed, whereas enforcement controls machines’ electricity, compute, data, networks, and actuator access.Machine enforcement can be graduated, from softer operational incentives and human approvals to cutting power off.
- Ethics and programmable law: Ethics and governance are intertwined but distinct: ethics concerns what should be done, while governance concerns enforceable rules, verification, and consequences.Attempts to encode Asimov’s First Law exposed ambiguities around harm, universal harmfulness, and immediate versus long-term consequences.
- Ethics and programmable law: Making law programmable may be a first step toward communicating ethics to AI, but deciding which rules to encode remains a human question.The paper treats law as the most developed human system for governing through explicit rules, without addressing the substantive choice of rules.
- Translation and verification: A workable bridge from English law to machine logic combines LLM translation, formal verification, and human adjudication because English-first parsing is unsafe without verification.Code-first methods are rigorous but require people fluent in law and logic, while English-first methods are more accessible and flexible.
- Limits and scope: Much law may resist coding because of loopholes, contradictions, deliberate vagueness, and context dependence, so computational law should target rules that are formalizable and executable.Safety-critical autonomous systems warrant computational guardrails, while tax, financial regulation, data protection, and machine-operation rules are more tractable than constitutional interpretation.
7 Conclusion
The paper concludes that executable, auditable obligations can govern AI without inspecting its reasoning, but deployment requires unchecked human and institutional safeguards. It identifies technical, legal, institutional, and philosophical work needed to make computational law deployable.
- Conclusion: Reified I/O Logic makes explicit, executable, auditable AI obligations technically possible in a human-readable symbolic language.LLMs can draft English-to-formal translations, and contracts can extend into agents’ operational code while producing audit trails.
- Conclusion: 3 of 4 accepted translations carried silent semantic errors, showing that formalization, LLM drafting, and tests all require checking.The formalism handled disjunction, reified negation, temporal scope, and nested obligations, while one mild sentence required an impractical quantified formula and Fluffy’s tests were wrong.
- Conclusion: Deployable computational law requires conflict resolution, runtime integration, verified rule libraries, computationally fluent practitioners, coding standards, executable-contract practices, and regulatory recognition.The paper also calls for clarity about the limits of formalization and acknowledges that much of law belongs beyond it.
- Conclusion: The decisive governance question is whether law can transform quickly enough to govern AI through advance executable specifications of when decisions are lawful.The conclusion frames this urgency against AI’s already ongoing transformation of law and the need to know why consequential decisions occur.
A Complete Wolfram Language Implementation
The complete Wolfram Language implementation is presented with corrections to earlier notebook code and was independently executed and verified. Verification covered 31 assertions, while camera-dependent perception snippets and Statement D’s live SatelliteData call were excluded.
- Implementation corrections: The implementation corrects the conjoinOutput guard and rewrites disjoinInput in an equivalent, clearer form.The conjoinOutput condition was moved to apply properly to the whole pattern.
- Verification: 31 assertions passed under Wolfram Language 14.3 using the repository verification script.The script also verified the GPT-4 translations and failure reproductions from Sections 4 and 5.
- Verification: Camera-dependent perception lines and Statement D’s live SatelliteData call were excluded from execution.These exclusions reproduce outputs from the original notebook session rather than requiring live hardware or data access.
A.1 I/O pairs and axioms
The section represents input/output pairs as legal norms in Wolfram Language and implements core operations for transforming, combining, and relating those rules. It also distinguishes ordinary operations from paradox-prone cumulative transitivity and an aggregative alternative.
- I/O pairs and axioms: I/O pairs are represented as rules of the form a -> b, with legal norms stored as a set of such pairs.The implementation defines inputOutputPair = a -> b and exemplifies legalNorms as {a -> b, c -> d, e -> f}.
- I/O pairs and axioms: Strengthening the input replaces a rule’s antecedent with a broader condition while preserving its consequent.The implementation returns broaderCondition -> rule[[2]].
- I/O pairs and axioms: Weakening the output replaces a rule’s consequence with a weaker one while preserving its antecedent.The implementation returns rule[[1]] -> weakerConsequence.
- I/O pairs and axioms: Output conjunction combines rules only when their inputs match, while input disjunction adds a rule whose antecedent is the disjunction of listed inputs.Mismatched inputs return "Inputs do not match"; the disjunction uses Or @@ ruleList[[All, 1]] and the first rule’s output.
- I/O pairs and axioms: The implementation presents cumulative transitivity as paradox-prone for contrast and defines aggregative cumulative transitivity by conjoining the two outputs under the first input.The aggregative form returns r1[[1]] -> (r1[[2]] && r2[[2]]) and otherwise reports "No Transitivity".
A.2 Norm sets
The norm set encodes implications connecting attributes to obligations, permissions, and status conditions. Its rules include taxation, insurance, driving, office access, employment, and adulthood.
- A.2 Norm sets: The norm set maps being an adult to paying taxes and owning a car to having insurance.These implications are represented as "isAdult" -> "payTaxes" and "ownsCar" -> "hasInsurance".
- A.2 Norm sets: It maps having a license to being able to drive and being an employee to being able to access an office.The encoded rules are "hasLicense" -> "canDrive" and "isEmployee" -> "canAccessOffice".
- A.2 Norm sets: It derives employee status from a signed contract and adult status from being age 18.The corresponding implications are "signedContract" -> "isEmployee" and "age18" -> "isAdult".
A.3 Reification and temporal operators
The implementation reifies scenarios, Boolean relations, and temporal existence as structured Wolfram Language expressions. It also provides temporal axioms for reified disjunction and negation, with supporting ABox/TBox typing utilities.
- Reification: Reified scenarios represent a transfer, its voluntariness, and their conjunction as nested symbolic expressions.The notebook constructs Alice’s transfer to Bob with `Transfer`, wraps it in `Voluntary`, and combines both using `And`.
- Reification: Structural tests confirm that the reified transfer contains the book and Alice, while its second component has head `Voluntary`.Each reported test evaluates to `True`.
- Temporal operators: Reified Boolean and temporal operators encode disjunction, negation, and an eventuality’s existence at a specified time.The definitions use `orPrime`, `notPrime`, and `RexistAtTime` to preserve these relations symbolically.
- Temporal operators: Temporal axioms infer that an existing disjunctive eventuality implies existence of one disjunct, while an existing negated relation implies nonexistence of the related eventuality.Both rules apply at the same time variable `t`.
A.4 Fluffy
The Fluffy implementation combines perceptual inputs and named entities with formal obligations, prohibitions, permissions, and violations. Five scenarios are checked against expected deontic outputs in a corrected verification harness.
- Implementation: Fluffy is configured with a name, a 100-unit distance threshold, and a symbolic Night condition.The implementation defines Fluffy = "Fluffy", DistanceThreshold1 = 100, and TimeNight = "Night".
- Implementation: Perception captures the current image, detects faces, highlights detected persons, and identifies the CN Tower as Home.The notebook uses CurrentImage[], FindFaces, HighlightImage, and Entity["Building", "CNTower"].
- Implementation: The formalized contract represents stopping and geographic containment as obligations, while taser use is represented as a permission or its absence.The code includes Stop and StayWithin200Meters obligations, a StayWithin200Meters violation, and both Permission and NoPermission for UseTaser.
- Verification: Five scenarios vary person distance, time of day, and boolean conditions, and the corrected verification harness reports all tests passing against expected deontic results.The scenarios include distances 80, 150, and 250, Night and Day conditions, and True or False values; expected outputs include obligations, permissions, and violations.