将欧盟人工智能法案的逻辑模态形式化，为法律智能推理打基础
Logical Modalities within the European AI Act: An Analysis
- 用高阶逻辑统一建模法案中的各种规范性语义
- 在Isabelle/HOL中实现多个逻辑系统的嵌入并编码法案条文
- 为法律自动化推理提供可计算框架，适合法律科技研究者
本文对欧盟人工智能法案中的逻辑模态进行了系统分析，旨在为其构建形式化表示，例如在逻辑多元的知识工程框架与方法（LogiKEy）中。LogiKEy基于形式化方法开发规范性推理工具，采用高阶逻辑（HOL）作为统一元逻辑，通过浅层语义嵌入整合多种逻辑体系。该集成借助Isabelle/HOL这一支持自动定理证明的证明辅助工具实现。论文讨论了人工智能法案中各类模态及其适用逻辑，并为部分逻辑创建了在HOL中的嵌入表示，进而用于编码法案样本段落。初步实验评估了这些嵌入在自动化推理中的适用性，揭示了迈向更强推理能力所面临的关键挑战。
原文摘要 · Abstract (English)
The paper presents a comprehensive analysis of the European AI Act in terms of its logical modalities, with the aim of preparing its formal representation, for example, within the logic-pluralistic Knowledge Engineering Framework and Methodology (LogiKEy). LogiKEy develops computational tools for normative reasoning based on formal methods, employing Higher-Order Logic (HOL) as a unifying meta-logic to integrate diverse logics through shallow semantic embeddings. This integration is facilitated by Isabelle/HOL, a proof assistant tool equipped with several automated theorem provers. The modalities within the AI Act and the logics suitable for their representation are discussed. For a selection of these logics, embeddings in HOL are created, which are then used to encode sample paragraphs. Initial experiments evaluate the suitability of these embeddings for automated reasoning, and highlight key challenges on the way to more robust reasoning capabilities.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。