DASS: A Framework for Accountable Smart Contract Wills

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

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.