DASS: A Framework for Accountable Smart Contract Wills

日常生活的许多方面都受到法律文件的影响，包括遗嘱和合同。与此同时，近几十年来的技术进步导致了生活的许多方面，无论是个人还是职业，从现实到虚拟的稳步迁移。正因为如此，由遗嘱和合同管理的活动将越来越多地由软件执行。为了确保将依赖这些系统的公众的完全访问和信任，重要的是要确保这些软件是负责任的，这意味着软件应该(1)可验证地遵循所有适用的规则和法律，(2)适当地适应法律的变化，以及(3)可解释，以便非程序员可以理解代码是做什么的，以及它如何与他们的意图相关。该项目旨在开发一个框架，用于设计和实施可问责的软件系统，以实现作为智能合约的遗嘱。该项目将通过将法律专业知识与自然语言处理技术以及可验证软件生成和执行的形式化方法相结合，开发负责任的软件。该框架将包括一个两阶段的翻译过程。在第一阶段，自然语言法律文件（这里是遗嘱）将被翻译成中间语义表示（答案集编程），可以从模板构建块中生成目标智能合约语言（Solidity）源代码。在第二阶段，将智能合约语言编译成可执行代码，并对其进行分析，以确保可执行代码忠实地表示预期的行为。翻译将是可解释的，这意味着每一个正式的指令都可以追溯到原始的人类可理解的法律文件文本。该项目将开发一个带注释的数据集，将自然语言的法律语句映射到中间表示，并使用它来适应深度学习技术，这种技术已经彻底改变了自然语言从意志到代码的机器翻译。该框架将通过两种互补的方式保证遗嘱的翻译和执行忠实于遗嘱和法律：(1)它将使用自然语言推理模块根据自然语言编写的法律检查翻译的形式表示，该模块能够评估在创建和执行的上下文中遗嘱中表达的原始文本是否与相关法律文本一致；(2)将使用编译器技术分析可执行代码，以推理验证的合同源代码与其反编译的可执行文件之间的语义相似性。该项目将在计算技术和法律方面对社会产生重大的积极影响：它将开发新的技术和工具，以一种定义良好且可解释的方式将人类可理解的合同转换为机器可理解的智能合同，并将根据原始合同验证生成的可执行代码。在项目期间，研究人员还将确定能够成功实现自动化并改善问责制的法律制度。研究过程中产生的所有软件和数据将免费提供给研究界。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Many aspects of everyday life are affected by legal documents, including wills and contracts. At the same time, the technological advances of recent decades have resulted in a steady migration of many aspects of life, both personal and professional, from the physical to the virtual. Because of this, activities governed by wills and contracts will increasingly be performed by software. To ensure the full access and trust of the public that will be relying on these systems, it is important to ensure that such software is accountable, meaning that the software should (1) verifiably follow all applicable rules and laws, (2) adapt appropriately to changes in laws, and (3) be explainable, so that non-programmers can understand what the code does and how it relates to what they intend. This project aims to develop a framework for the design and implementation of accountable software systems for wills implemented as smart contracts.The project will develop accountable software by combining expertise in the law with techniques from natural-language processing and formal methods for verifiable software generation and execution. The framework will include a two-stage translation process. In the first stage, natural-language legal documents (here, wills) will be translated into an intermediate semantic representation (Answer Set Programming) that can generate target smart-contract-language (Solidity) source code out of templated building blocks. In the second stage, the smart-contract language is then compiled into executable code that will be analyzed to ensure that the executable code faithfully represents the intended behavior. The translation will be explainable, meaning that each formal instruction can be traced back to the original human-understandable legal document text. The project will develop an annotated dataset that maps legal statements in natural language into the intermediate representation and use this to adapt deep-learning techniques that have revolutionized the machine translation of natural languages from wills to code. The framework will guarantee that the translation and execution of a will is faithful to the will and the law using two complementary methods: (1) It will check the translated formal representation against laws written in natural language using a natural-language inference module that is able to assess whether the original text expressed in the will in the context of creation and execution is consistent with relevant legal text, and (2) the executable code will be analyzed using compiler technology to reason about the semantic similarity between the validated source code of the contract and its decompiled executable. The project will have significant positive impacts on society, in terms of both computing technology and law: it will develop novel techniques and tools to translate human-understandable contracts to machine-understandable smart contracts in a well-defined and explainable way, and it will validate the resulting executable code against the original contracts. During the project, the researchers will also identify legal regimes that can be successfully automated and improve accountability. All of the software and data produced during this research will be made freely available to the research community.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.