发表机构
Wolfram Institute for Computational Foundations of Science（沃尔夫勒姆计算基础科学研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文在Wolfram语言中实现Reified Input/Output Logic，测试GPT-4转换英文法律陈述的情况，通过AI看门狗案例展示计算法可作为AI治理工具，理想目标是形式化可编程执行的法律。
AI 中文摘要
如何治理那些我们无法完全检查其推理过程的AI系统？治理并不需要理解系统的推理过程，而是需要明确规定系统有义务执行、被允许执行和被禁止执行的行为，并检查其是否合规。本文介绍了在Wolfram语言中对Reified Input/Output Logic（具体化输入/输出逻辑，即DAPRECO知识库背后的形式体系）的实现，涵盖核心I/O公理、义务、许可、构成性规范、具体化事项以及时间算子。随后测试了GPT-4能否将英文法律陈述转换为该形式体系，并报告了其失败情况：存在幻觉函数、省略时间范围、偏离形式体系，以及在最糟糕的情况下生成的代码可运行、看似合理，但暗中编码了错误的规范。一个案例研究展示了在计算合同下运行的AI看门狗，说明形式化规则如何能直接从合同扩展到具身智能体的操作代码，为其行为生成可审计的符号化理由。本文认为计算法可作为一种治理工具，且理想目标是将能够且应当可编程执行的法律形式化。
英文摘要
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.
Comments25 pages, 1 figure, 2 tables, 12 code listings. Wolfram Language implementation and verification script (31 assertions) available at https://github.com/Zaffer/research-computational-law
