Linear Logic and its developments

Girard (1998): Light Linear Logic (LLL)

What it does.
Girard introduces LLL, a subsystem of linear logic designed so that cut-elimination runs in polynomial time. The key move is to constrain duplication via boxes and a special “paragraph” modality (often written §\mathsf{§}§), which implements a stratification (depth discipline) over proofs. Promotion (the source of duplication) is permitted only in tightly controlled contexts, so the size and depth of proof nets cannot blow up during normalization. This yields an implicit characterization of PTIME via proofs-as-programs. ScienceDirect+1

Why it matters for SLLL.
LLL is the prototype for “light logics”: enforce structural restrictions (rather than explicit resource counters) to guarantee complexity bounds. Our SLLL uses a level modality ↑\uparrow↑ and uniform-level duplication to achieve the same goal with more explicit typing and agent-facing semantics.


Baillot & Mazza (2010): Linear Logic by Levels and Bounded Time Complexity

What it does.
This paper generalizes Girard’s depth-based stratification by assigning integer levels to proof-net edges. Levels induce a stratification stricter (or looser) than depth, recovering Girard’s systems when “level = depth,” but allowing more flexibility. They prove that with appropriate level constraints, cut-elimination stays within elementary time or PTIME, giving new characterizations of complexity classes. Notably, they show one can avoid paragraph boxes (or restrict them to atoms) while keeping the same complexity properties—useful for more efficient type assignment. arXivScienceDirectACM Digital Library+1

Why it matters for SLLL.
“Levels” are exactly the idea our ↑\uparrow↑-modality makes explicit at the type level. We adopt their insight that stratification can be decoupled from box depth, which makes typing and implementation cleaner for real agents (LLMs/GPUs).


Boudes, Mazza, Tortora de Falco (2015): An Abstract Approach to Stratification in Linear Logic

What it does.
This paper abstracts “stratification” into its own separate modality, defined by a general categorical construction that applies to any model of linear logic. They show that stratification need not be baked into the exponentials; however, when you connect it to exponentials, you recover the light-logic complexity bounds. They also give three reformulations of Baillot–Mazza’s “levels” (geometric, interactive, semantic), clarifying the landscape and unifying different presentations. arXivScienceDirectACM Digital LibraryDBLP

Why it matters for SLLL.
Exactly our philosophy: make stratification a first-class modality (our ↑\uparrow↑). Their categorical account justifies treating stratification independently and then coupling it to duplication to get provable PTIME bounds.


Murfet (2014/2017): Logic and Linear Algebra: an Introduction

What it does.
Murfet gives a friendly but deep tour of linear logic for algebraists, with concrete vector-space semantics of proofs as linear maps, emphasizing the cofree cocommutative coalgebra (Sweedler) for modeling the exponential !!!. It also connects to geometry of interaction intuitions. As a result, the semantics of promotion/duplication becomes linear-algebraic (coalgebraic) structure, which is great for building computable models and for seeing how resource sensitivity emerges algebraically. arXiv+1ResearchGate

Why it matters for SLLL.
A ready-made semantic playground for our system: the ↑\uparrow↑-modality and uniform-level !!

! can be interpreted over vector spaces/cofree coalgebras, helping to reason about soundness and potentially compile SLLL-typed agents to linear-algebraic runtimes (relevant for GPU/LLM backends).

技术人工智能安全研究方向的建议

Anthropic(Anthropic)的对齐科学团队正在进行技术研究,旨在减少未来高级人工智能系统可能导致的灾难性风险,例如大规模生命损失或人类对自身控制的永久丧失。我们面临的核心挑战是确定当下可以开展的具体技术工作,以预防这些风险。我们的研究将在未来的世界中发挥作用——也就是说,在那些因人工智能而存在重大灾难性风险的世界中——这些世界将被人工智能的发展彻底改变。我们的大部分工作在于为如何在这些变革的世界中驾驭人工智能发展绘制路径。

我们经常遇到对减少灾难性风险感兴趣的人工智能研究人员,但他们也面临同样的挑战:目前可以进行哪些技术研究,能够帮助人工智能开发者确保其未来系统的安全性?在这篇博文中,我们分享了我们对这个问题的一些思考。

为了撰写这篇文章,我们请对齐科学团队的成员撰写他们认为重要的开放性问题或研究方向的描述,然后将结果整理成几个广泛的类别。这个结果并非技术对齐研究方向的全面列表。可以将其视为一份品鉴菜单,旨在突出该领域一些有趣的开放性问题。

这也不是我们正在积极从事、协调或提供研究支持的方向列表。虽然我们确实在其中一些领域开展研究,但许多方向是我们希望看到取得进展但自己没有能力投入的。我们希望这篇博文能够激励更广泛的人工智能研究社区在这些领域开展更多工作。


评估能力

我们如何衡量人工智能系统的能力?

为了让社会成功地应对向强大人工智能的过渡,基于实证的专家共识对于当前和预期未来人工智能系统的影响至关重要。然而,目前专家们对人工智能发展的预期轨迹,甚至对当前人工智能系统的能力,都存在广泛的分歧。

许多人工智能能力评估基准(包括针对博士级知识的困难测试)很快就会饱和,因此未能提供人工智能进展的连续、可外推信号。另一方面,人工智能系统的现实影响往往落后于基于令人印象深刻的基准分数所预期的水平。因此,创建能够真正追踪其现实世界影响的高质量人工智能能力评估至关重要。

在某些对国家安全至关重要的领域——如化学、生物、辐射和核(CBRN)武器开发能力——此类评估应在与政府协调的安全实验室中进行。然而,还有许多其他能力——如进行新颖研究、与工具互操作以及自主完成开放性任务——对于理解人工智能系统的影响也很重要。我们期待看到对这些能力的高质量评估,以及相应的人类基准。

请参阅我们之前此处的公告,了解我们希望看到更多研究的能力评估的更多信息(但请注意,该倡议的截止日期已过)。


评估对齐

我们如何衡量人工智能系统的对齐程度?

我们目前对前沿模型对齐的测量主要集中在相对表面的属性上,如:

  • 模型是令人愉快的对话助手

  • 模型拒绝有害的查询

  • 模型避免产生有毒文本

虽然这些属性足以确保当前人工智能聊天机器人的安全性,但我们预计未来的人工智能系统将在我们无法预料的各种(有时是高风险的)环境中部署。因此,我们需要更好的方法来衡量人工智能系统倾向于未对齐行为的可能性。

例如,给定一个模型,我们可能想回答以下问题:

  • 模型是否具有驱动、目标、价值观或偏好?如果有,它们是什么?

    • 例如,我们发现我们的模型有阿谀奉承的倾向:它们通常倾向于讨好用户的回应。
  • 模型是否曾故意假装比实际更对齐?它是否曾隐藏其驱动、目标、价值观或偏好?它是否曾战略性地选择不透露自己拥有的能力?

  • 在什么情况下模型会故意误导人类?

尽管这些问题极其微妙——在许多情况下,模糊或定义不清——但它们可能对未来的部署决策至关重要。

考虑这样一种情况:一个模型(1)足够有能力成功执行极其有害的行动,但(2)在受控的实验室环境中,通常避免采取此类行动。我们能做些什么来放心地广泛部署这样的模型?

理解模型认知

当我们的模型生成输出时,它们在“想”什么?

许多人工智能研究涉及从输入/输出行为的角度理解人工智能系统。行为问题的例子包括:模型的答案中有多大比例是正确的?哪些输入会导致模型生成有毒文本?当被问到时,我们的模型是否声称优先考虑用户的利益?

在评估模型的对齐程度时,我们不仅想检查模型的输出是否看起来无害,还想了解模型是否出于“正确的原因”得出了其输出。因此,我们希望通过研究这些行为背后的认知来补充对模型行为的理解。理解模型认知涉及询问模型在想什么,导致其表现出某些感兴趣的行为。例如,我们可能会问:

  • 当我们的模型给出答案时,是因为它认为答案是正确的?还是因为它模拟了用户认为答案是正确的?或者因为它认为答案会以其他方式取悦用户?

  • 我们的模型是否形成计划?如果是,这些计划是什么?

  • 我们的模型对其处境了解多少?它们是否猜测自己是在训练中,或者它们是如何被监控的?这种知识如何影响它们的行为?

  • 我们的模型是否知道在被问到时不会报告的信息?

理解模型认知可能有助于加速对令人担忧的行为的搜索(例如在审计或红队测试期间),改进我们在训练期间的监督,或预测模型在分布外的行为。

在理解模型认知方面有大量研究,尤其是在机械可解释性领域,这是一个专注于直接解码训练好的人工智能系统学习的内部算法的方法的领域。与其尝试概述机械可解释性的轮廓,我们建议读者参考Anthropic的可解释性团队博客

另一方面,我们相信在理解模型认知的其他方法上有充足的空间。例如:

  • 外化认知:诱导模型“高声思考”(例如通过推理链(chain-of-thought)草稿)并研究产生的推理轨迹。这里的核心挑战是确保外化推理的可信度;见下文。

  • 内省:训练模型直接口头表达其隐藏状态的内容(Binder等人,2024;Chen等人,2024;Ghandeharioun等人,2024;Zhuang等人,2024;Pan等人,2024)。例如,我们能否训练一个模型准确报告其在棋盘游戏中的计划,通过判断模型的答案是否准确预测其后续行动?

理解模型的角色如何影响其行为

模型的“性格”对其行为有什么影响?

如今的领先模型通常以良性的方式表现,即使面对它们未经过训练的不寻常提示也是如此。对这种泛化的一个假设是,它们采用了某种角色,即乐于助人的助手,这暗示了一系列良好的默认行为。然而,不同的助手有略微不同的角色,角色的看似微小变化可能对它们在新情况下的行为产生重要影响。例如,在研究对齐伪装时,我们发现,在某些环境中,只有一些模型会伪装对齐。模型伪装对齐的倾向在多大程度上受其角色或价值观的影响?是否可能模型的写作风格和性格不仅仅是表面的,而是对模型的行为有广泛的间接影响,包括在安全关键的情况下?

我们期待看到更多工作来描述模型的角色如何影响其在各种环境中的行为。例如,可以创建(通过少样本提示或在合成数据上训练)一组能力相似但角色不同的模型,并研究这些性格差异如何影响它们在各种下游情况下的行为。

推理链的可靠性

我们何时可以直接相信模型的推理链?

语言模型并不总是说出它们的真实想法。事实上,它们可能系统性地歪曲其行为背后的推理。因此,我们对检测(Lanham等人,2023;Mills等人,2024)或确保(Radhakrishnan等人,2023;Chen等人,2024;Chua等人,2024)语言模型的推理链(CoT)可靠性的技术感兴趣。这是一个重要但尚未得到充分探索的研究领域,因此我们鼓励对此进行更多研究。例如,我们对以下问题的答案感兴趣:

  • 推理链的可靠性在不同类型的任务中如何变化?如果使用推理链能显著提升任务性能,这是否意味着推理链相对可信?推理链的可靠性在数学和社会推理之间是否有所不同?

  • 模型对其处境的认知是否会影响其推理链的可靠性?例如,在被告知其推理链正在被监控或评估可信度后,模型会产生更可信或更不可信的解释吗?

  • 我们如何使检测不可信推理链的自动方法(Lanham等人,2023;Mills等人,2024;Chen等人,2024)更高效并具有更高的召回率?


人工智能控制

我们能否通过在部署模型的同时配备足够的安全保障来确保安全?

目前,我们相信人工智能系统不会带来灾难性风险的主要原因是它们缺乏造成灾难性伤害所需的许多能力(如能够进行新颖的研究或有效地操纵大量人群)。在未来,我们可能会有人工智能系统足够有能力造成灾难性伤害,但由于它们足够对齐而不这样做;如果我们在评估对齐方面取得了足够的进展,我们可以基于对齐来提供安全保证。

我们可以做出的第三类保证——除了充分的对齐或缺乏危险能力之外——是我们已经在部署人工智能系统的同时配备了足够的安全保障,即使它们尝试也无法成功造成灾难性伤害。这种策略,被称为人工智能控制,适用于当人工智能系统在没有安全保障的情况下足够有能力造成灾难,但在受限环境中部署时,无法规避谨慎开发者施加的安全保障。在本节中,我们将讨论人工智能控制的可能策略,重点关注人工智能系统的运行时监控。

行为监控

我们能否通过让另一个人工智能监控我们的人工智能的输入和输出来确保安全?

一种人工智能控制策略是使用辅助人工智能系统(监控者)来筛查另一个不可信的人工智能系统(执行者)的输入和输出(Naihin等人,2023;Chen等人,2024;Greenblatt等人,2023)。Greenblatt等人(2023)研究了这个想法的不同变体,包括:

  • 可信监控:使用较弱但可信的人工智能系统来监控执行者的输入和输出,例如使用GPT-3.5来筛查潜在恶意的GPT-4编写的代码。

  • 不可信监控:使用另一个不可信的模型(例如,执行者模型的另一个实例)作为监控者。

这些监控设置的核心挑战是,监控器的失败可能系统性地集中在执行者表现出恶意行为的相同情节中。例如,这可能是因为执行者故意破坏监控器(例如通过越狱),或者——在不可信监控的情况下——因为监控器和执行者串通。

我们对提高行为监控的有效性的工作感到兴奋。有前景的方向包括:

  • 减少执行者-监控器之间的串通或越狱机会,例如在将执行者的输出展示给监控器之前编辑或改写输出。

  • 培训更好的监控器,例如通过生成真实反映复杂、恶意行为的合成数据。

  • 更好地估计极其罕见的灾难性结果的失败率。

  • 开发即使在执行者具有额外能力的情况下也能起作用的监控方案,例如拥有之前情节的记忆或能够在实例之间传递消息的能力。

激活监控

我们能否通过监控人工智能的隐藏状态来确保安全?

监控人工智能系统的输入/输出行为的替代方案是监控其潜在激活。例如,可以尝试训练简单的探测器,使用模型的潜在激活来分类它何时在编写安全与不安全的代码。这个方向可以被视为理解模型认知的一个不那么雄心勃勃的替代方案,我们在这里寻找可扩展、自动的方法来检测模型内部处理中预先指定的不期望的概念的存在。

这种监控方法很有前途,因为模型的激活(1)对应于被监控模型的推理,(2)难以被模型控制。例如,当使用弱模型来行为监控更强大的代码生成模型的是否存在不安全代码时,我们可能担心弱监控器会遗漏一些漏洞,或者代码生成模型会混淆其代码以使漏洞难以检测;监控代码生成模型自身的激活可能会避免这些失败。

另一方面,激活监控器可能对分布偏移不够鲁棒。一个特别重要的分布偏移是从固定的合成数据集到模型自身生成的数据。如果我们没有要检测的坏输出的模型生成示例,那么我们需要以某种其他方式合成输出来训练激活监控器。然后我们需要验证使用这些输出训练的监控器能够泛化到我们关心的实际危险模型生成上。

虽然激活监控已经显示出一些迹象活力,但需要更多研究使其在生产人工智能系统中部署时足够可靠。

异常检测

我们能否自动检测我们的模型何时表现“异常”?

许多监控方法都是有监督的:它们涉及在精选的正负样本数据集上训练分类器,以识别坏的模型行为。然而,我们可能事先不知道危险的失败是什么样的。因此,另一种无监督的监控方法是异常检测:尝试检测模型的计算何时在某些方面异常或偏离分布。

例如,假设我们已经部署了一个模型和某种有害行为的监控器。我们可能期望我们的监控器能够捕获有害行为的典型案例,但在罕见的输入(例如越狱)上失败。因此,我们可能还会在模型和监控器旁边部署一个异常检测器,旨在标记远离分布的输入(如罕见的越狱)。我们可以手动检查和标记这些输入,随后使用它们改进我们的监控器的覆盖范围。将现有的异常检测技术应用于模型的潜在激活可能已经适用于这样的任务;参见例如这里

更雄心勃勃的是,我们可能尝试将异常检测应用于检测两个模型之间存在巨大差异的情况。例如,考虑一个输入,强模型理解了弱模型不理解的东西,导致行为新颖,并且——从弱模型的角度来看——令人惊讶。可能可以自动检测此类输入。据我们所知,这是一个尚未探索的问题设置,我们期待在这方面取得进展。

https://alignment.anthropic.com/2025/recommended-directions/

Sabotage Modal Logic

HAL Id: hal-01194426 

https://inria.hal.science/hal-01194426v1

摘要(中文)

本文探讨了破坏模态逻辑(Sabotage Modal Logic,SML)的一些模型和证明论方面的问题。破坏模态逻辑是一种扩展了标准模态语言的新逻辑,增加了边删除模态操作符,表达了“在删除至少一条边后公式成立”的语义。研究的核心贡献包括:

  1. 特征定理的证明:将破坏模态逻辑刻画为一阶逻辑中对破坏双模仿(sabotage bisimulation)保持不变的片段。
  2. 表格方法的提出:开发了SML的一个可靠且完备的表格方法(tableau method)。
  3. 未解问题的讨论:提出了一系列关于破坏模态逻辑的研究方向,包括其与模型更新逻辑的整合、决策性问题的探讨,以及对SML逻辑形式的可能限制。

此外,文章还讨论了破坏模态逻辑与动态认知逻辑和理论计算机科学的联系,特别是在模型检查复杂性及其不可判定性方面的研究进展。


Abstract (English)

This paper explores certain model and proof-theoretic aspects of Sabotage Modal Logic (SML). SML extends the standard modal language by introducing an edge-deletion modality that expresses the semantics “after deleting at least one edge, the formula holds.” The main contributions of this study include:

  1. Proof of a Characterization Theorem: SML is characterized as the fragment of first-order logic invariant under a specific notion of bisimulation, called sabotage bisimulation.
  2. Development of a Tableau Method: A sound and complete tableau method for SML is proposed.
  3. Discussion of Open Problems: Several open research questions are raised, including the integration of SML within the current landscape of logics of model update, its decision problems, and potential semantic restrictions.

The paper also discusses the connections of SML with dynamic epistemic logic and theoretical computer science, particularly in terms of model-checking complexity and its undecidability.


A Classical Logic of Existence and Essence

Authors: S. Galvan and A. Giordani

Abstract.The purpose of this paper is to provide a new system of logic for existence and essence, in which the traditional distinctions between essential and accidental properties, abstract and concrete objects, and actuallyexistent and possibly existent objects are described and related in a suit-able way. In order to accomplish this task, a primitive relation of essentialidentity between different objects is introduced and connected to a firstorder existence property and a first order abstractness property. The basicidea is that possibly existent objects are completely determinate and thatessentially identical objects are just different individuations of the same in-dividual essence. Accordingly, essential properties are defined as propertiesthat are invariant with respect to this kind of identity, while abstract objectsare determined by being characterized by essential properties only. Oncesuch ideas are implemented, a number of classical intuitions about objects,their essence, and their way of existence can be consistently interpreted.

Keywords: essence; existence; qualitative identity; essential identity; abstract objects; possible worlds semantics; quantified modal logic

这篇论文提出了一种新的经典模态逻辑CML,旨在提供一个形式框架来描述存在、本质和必然性等经典概念之间的关系。该框架的主要特征有:

  1. 引入了一个一阶存在谓词E来表示实际存在的属性。
  2. 引入了一个本质同一关系≈来连接本质相同的不同对象。本质相同的对象是同一本质的不同个体化。
  3. 定义了不变性质(invariant property)和本质性质(essential property)。不变性质是对象的所有本质变体都必然共享的性质。本质性质是非普适的不变性质。
  4. 引入了抽象性谓词A来描述抽象对象。抽象对象存在且不可变。
  5. 区分了潜在存在(potential existence)和逻辑存在(logical existence)。前者表示对象可能实际存在,后者表示对象逻辑上可能存在。
  6. 定义了必然对象(necessary object)和偶然对象(contingent object)。必然对象必然存在,偶然对象只是可能存在。
  7. 证明了一些关于本质性质和对象的重要定理,体现了经典形而上学的一些基本洞见。
  8. 与 Meinong主义、莱布尼兹主义、Lewis模态实在论和最简单的模态逻辑进行了比较。
总的来说,该论文通过一系列概念和公理的明确定义,构建了一个表达经典存在论和本体论观点的模态逻辑系统。它区分了不同类型的物体、性质和存在方式,并证明了一些重要的经典命题。这为探讨存在、本质、必然性等议题提供了一个新的理论框架。

我对人格生物特征证明有何看法?

特别感谢 Worldcoin 团队、Proof of Humanity 社区和 Andrew Miller 的讨论。

以太坊社区的人们一直在尝试构建的更棘手但可能是最有价值的小工具之一是去中心化的人格证明解决方案。人格证明,又名“独特的人类问题”,是现实世界身份的一种有限形式,它断言给定的注册帐户由一个真实的人(以及与每个其他注册帐户不同的真实人)控制,理想情况下没有揭示它是哪个真人。

人们已经做出了一些努力来解决这个问题:Proof of HumanityBrightIDIdenaCircles就是例子。其中一些带有自己的应用程序(通常是 UBI 代币),还有一些在Gitcoin Passport中用于验证哪些账户对于二次投票有效。像Sismo这样的零知识技术为许多解决方案增加了隐私性。最近,我们看到了一个更大、更雄心勃勃的人格证明项目的崛起:世界币

世界币由山姆·奥尔特曼 (Sam Altman) 联合创立,他因担任 OpenAI 首席执行官而闻名。该项目背后的理念很简单:人工智能将为人类创造大量的丰富和财富,但它也可能会杀死很多人的工作,并且几乎无法区分谁是人类,谁是机器人,所以我们需要通过(i)创建一个非常好的人格证明系统来填补这个漏洞,以便人类可以证明他们实际上是人类,以及(ii)为每个人提供全民基本收入。世界币的独特之处在于它依赖于高度复杂的生物识别技术,使用名为“Orb”的专用硬件扫描每个用户的虹膜:



我们的目标是生产大量这些球体,并将它们广泛分发到世界各地,并将它们放在公共场所,以便任何人都可以轻松获得 ID。值得赞扬的是,世界币还致力于随着时间的推移去中心化。首先,这意味着技术上的去中心化:使用Optimism 堆栈成为以太坊上的 L2,并使用ZK-SNARK 和其他加密技术来保护用户的隐私。后来,它包括系统本身的去中心化治理。

世界币因 Orb 的隐私和安全问题、其“硬币”的设计问题以及该公司做出的一些选择的道德问题而受到批评。有些批评非常具体,集中在项目做出的决定上,而这些决定很容易以另一种方式做出——事实上,世界币项目本身可能愿意改变。然而,其他人则提出了更根本的担忧,即生物识别技术——不仅是世界币的眼睛扫描生物识别技术,还包括人类证明和 Idena 中使用的更简单的面部视频上传和验证游戏——是否是一个好主意。全部。还有一些人批评一般人格证明。风险包括不可避免的隐私泄露、人们匿名浏览互联网的能力进一步受到侵蚀、独裁政府的胁迫,以及在去中心化的同时保证安全的可能性。



这篇文章将讨论这些问题,并讨论一些论点,这些论点可以帮助您决定在我们的新球形霸主面前鞠躬并扫描您的眼睛(或脸部,或声音,或......)是否是一个好主意,并且自然的替代方案——使用基于社交图谱的人格证明或完全放弃人格证明——是否更好。

什么是人格证明以及为什么它很重要?

定义身份证明系统的最简单方法是:它创建一个公钥列表,其中系统保证每个密钥都由唯一的人控制。换句话说,如果你是人类,你可以在列表中放置一个键,但不能在列表中放置两个键,如果你是机器人,则不能在列表中放置任何键。

人格证明很有价值,因为它解决了许多人面临的许多反垃圾邮件和反权力集中问题,避免了对中央机构的依赖,并尽可能揭示最少的信息。如果人格证明没有得到解决,去中心化治理(包括社交媒体帖子上的投票等“微观治理”)将变得更容易非常富有的参与者(包括敌对政府)捕获。许多服务只能通过设置访问价格来防止拒绝服务攻击,有时,对于许多低收入合法用户来说,足以阻止攻击者的高价格也太高了。

当今世界上的许多主要应用程序通过使用政府支持的身份系统(例如信用卡和护照)来处理这个问题。这解决了问题,但它在隐私方面做出了巨大且可能不可接受的牺牲,并且可能会受到政府本身的轻微攻击。


有多少人格证明支持者看到了我们面临的双面风险。


在许多人格证明项目中——不仅是世界币,还包括人类证明、Circles 等——“旗舰应用程序”是内置的“N 人代币”(有时称为“UBI 代币”) 。每个在系统中注册的用户每天(或每小时或每周)都会收到一些固定数量的代币。但还有很多其他应用:

在许多这样的情况下,共同的主线是希望创建开放和民主的机制,避免项目运营商的集中控制和最富有的用户的统治。后者在去中心化治理中尤其重要。在许多这样的情况下,当今的现有解决方案依赖于以下因素的某种组合:(i) 高度不透明的人工智能算法,这些算法留下很大的空间来难以察觉地歧视运营商根本不喜欢的用户,以及 (ii) 集中式 ID,又名“KYC” 。有效的身份证明解决方案将是一个更好的替代方案,可以实现这些应用程序所需的安全属性,而不会遇到现有集中式方法的陷阱。

在人格证明方面有哪些早期尝试?

人格证明有两种主要形式:基于社交图谱和生物识别。基于社交图谱的人格证明依赖于某种形式的担保:如果爱丽丝、鲍勃、查理和大卫都是经过验证的人类,并且他们都说艾米丽是经过验证的人类,那么艾米丽也可能是经过验证的人类。凭证通常会通过激励措施得到增强:如果爱丽丝说艾米丽是人类,但事实证明她不是,那么爱丽丝和艾米丽都可能会受到惩罚。人格的生物识别证明涉及验证艾米丽的某些身体或行为特征,这将人类与机器人(以及人类个体之间)区分开来。大多数项目结合使用这两种技术。

我在文章开头提到的四个系统的工作原理大致如下:

  • 人性证明:您上传自己的视频,并提供押金。要获得批准,现有用户需要为您提供担保,并且需要经过一段时间才能对您提出质疑。如果存在质疑, Kleros 去中心化法院将判定您的视频是否真实;如果不是,您将失去存款,而挑战者将获得奖励。
  • BrightID:您与其他用户一起加入视频通话“验证方”,每个人都互相验证。通过Bitu可以进行更高级别的验证,在该系统中,如果有足够多的其他经过 Bitu 验证的用户为您提供担保,您就可以获得验证。
  • Idena:您在特定时间点玩验证码游戏(以防止人们多次参与);验证码游戏的一部分涉及创建和验证验证码,然后将其用于验证其他验证码。
  • Circles:现有 Circles 用户为您提供担保。Circles 的独特之处在于它不尝试创建“全球可验证的 ID”;相反,它创建了一个信任关系图,其中某人的可信度只能从您自己在该图中的位置的角度来验证。

世界币如何运作?

每个世界币用户在手机上安装一个应用程序,该应用程序会生成私钥和公钥,就像以太坊钱包一样。然后他们亲自去参观“Orb”。用户凝视 Orb 的摄像头,同时向 Orb 展示由其 Worldcoin 应用程序生成的二维码,其中包含其公钥。Orb 扫描用户的眼睛,并使用复杂的硬件扫描和机器学习分类器来验证:

  1. 用户是一个真实的人
  2. 用户的虹膜与之前使用过该系统的任何其他用户的虹膜不匹配

如果两次扫描都通过,Orb 会签署一条消息,批准用户虹膜扫描的专门哈希值。哈希值被上传到数据库 - 目前是一个集中式服务器,一旦确定哈希机制有效,就打算用去中心化的链上系统取代。系统不存储完整的虹膜扫描;它只存储哈希值,这些哈希值用于检查唯一性。从那时起,用户就有了一个“世界ID ”。

World ID 持有者能够通过生成 ZK-SNARK 来证明他们是唯一的人,证明他们持有与数据库中的公钥相对应的私钥,而无需透露他们持有哪个密钥。因此,即使有人重新扫描您的虹膜,他们也无法看到您采取的任何操作。

世界币建设的主要问题是什么?

人们立即想到四个主要风险:

  • 隐私。虹膜扫描的注册表可能会泄露信息。至少,如果其他人扫描您的虹膜,他们可以根据数据库进行检查,以确定您是否拥有世界 ID。虹膜扫描可能会揭示更多信息。
  • 无障碍。除非有足够多的球体,世界上任何人都可以轻松获得,否则世界 ID 将无法可靠地访问。
  • 集中化。Orb 是一个硬件设备,我们无法验证它的构造是否正确且没有后门。因此,即使软件层完美且完全去中心化,世界币基金会仍然有能力在系统中插入后门,让它创建任意多个虚假的人类身份。
  • 安全。用户的手机可能会被黑客入侵,用户可能会被迫扫描自己的虹膜,同时出示属于其他人的公钥,并且有可能 3D 打印“假人”,可以通过虹膜扫描并获得世界 ID。

重要的是要区分 (i) 世界币做出的选择所特有的问题,(ii)任何人格生物特征证明都不可避免地存在的问题,以及 (iii)任何一般人格证明都会存在的问题。例如,签署“人性证明”意味着在互联网上发布您的面孔。加入 BrightID 验证方并不能完全做到这一点,但仍然可以向很多人暴露您的身份。加入 Circles 会公开暴露您的社交图谱。世界币明显更好在保护隐私方面比这两者都强。另一方面,世界币依赖于专门的硬件,这带来了信任球体制造商是否正确构建球体的挑战 - 这一挑战在人类证明、BrightID 或 Circles 中都没有类似的挑战。甚至可以想象,在未来,世界币以外的其他人将创建具有不同权衡的不同专用硬件解决方案。

生物识别身份证明方案如何解决隐私问题?

任何身份证明系统最明显、最大的潜在隐私泄露是将一个人采取的每个行动与现实世界的身份联系起来。这次数据泄露的规模非常大,可以说大得令人无法接受,但幸运的是利用零知识证明技术很容易解决。用户可以制作一个 ZK-SNARK 来证明他们拥有对应的公钥位于数据库中某处的私钥,而不用直接使用其对应的公钥在数据库中的私钥进行签名,而无需透露他们使用的是哪个特定密钥。有。这通常可以使用Sismo等工具来完成(请参阅此处用于人类证明特定的实现),并且世界币有其自己的内置实现。在这里提供“加密原生”的人格信用证明非常重要:他们实际上关心采取这一基本步骤来提供匿名化,而基本上所有集中式身份解决方案都不会这样做。

一个更微妙但仍然重要的隐私泄露是生物识别扫描公共注册表的存在。就人性证明而言,这是大量数据:您可以获得每个人性证明参与者的视频,这使得世界上任何愿意调查所有人性证明参与者是谁的人都非常清楚。就世界币而言,泄漏的情况要有限得多:Orb 在本地计算并仅发布每个人虹膜扫描的“哈希值” 。这个哈希值不是像 SHA256 这样的常规哈希值;相反,它是一种基于机器学习的Gabor 滤波器的专门算法,用于处理不精确性任何生物识别扫描所固有的,并确保对同一个人的虹膜进行的连续哈希具有相似的输出。


蓝色:同一个人虹膜两次扫描之间差异的位数百分比。橙色:两个不同人虹膜的两次扫描之间差异的位数百分比。


这些虹膜散列仅泄漏少量数据。如果对手可以强行(或秘密)扫描您的虹膜,那么他们可以自己计算您的虹膜哈希,并根据虹膜哈希数据库进行检查,以了解您是否参与了该系统。这种检查某人是否注册的能力对于系统本身来说是必要的,以防止人们多次注册,但它总是有可能被滥用。此外,虹膜哈希值有可能泄露一定量的医疗数据(性别、种族,也许还有医疗状况),但这种泄露远远小于当今使用的几乎任何其他海量数据收集系统所能捕获的数据(例如,甚至街头摄像机)。总的来说,对我来说,存储虹膜哈希值的隐私性似乎就足够了。

如果其他人不同意这个判断并决定设计一个具有更多隐私的系统,有两种方法可以做到:

  1. 如果可以改进虹膜散列算法以使同一个人的两次扫描之间的差异低得多(例如,可靠地低于 10% 位翻转),那么系统可以存储较少数量的纠错,而不是存储完整的虹膜散列虹膜哈希值的位(参见:模糊提取器)。如果两次扫描之间的差异低于 10%,则需要发布的位数将至少减少 5 倍。
  2. 如果我们想更进一步,我们可以将 iris 哈希数据库存储在多方计算 (MPC)系统中,该系统只能由 Orbs 访问(有速率限制),从而使数据完全无法访问,但代价是显着管理 MPC 参与者集的协议复杂性和社会复杂性。这样做的好处是,即使用户愿意,也无法证明他们在不同时间拥有的两个不同世界 ID 之间的联系。

不幸的是,这些技术不适用于人性证明,因为人性证明要求公开每个参与者的完整视频,以便在有迹象表明它是假的(包括人工智能生成的假货)时可以对其提出质疑,并且在这种情况下进行更详细的调查。

总的来说,尽管盯着一个球体并让它深入扫描你的眼球有一种“反乌托邦的感觉”,但专业的硬件系统似乎确实可以在保护隐私方面做得相当不错。然而,另一方面是专用硬件系统带来了更大的集中化问题。因此,我们密码朋克似乎陷入了困境:我们必须用一种根深蒂固的密码朋克价值观与另一种价值观进行权衡。

生物识别身份证明系统中的可访问性问题是什么?

专用硬件会带来可访问性问题,因为专用硬件不太容易访问。目前,51%64%的撒哈拉以南非洲人拥有智能手机,预计到 2030 年这一比例将增至87%。但是,虽然智能手机有数十亿部,但 Orb 的数量却只有几百个。即使有了更大规模的分布式制造,也很难达到一个距离每个五公里之内都有一颗宝珠的世界。


但值得赞扬的是,他们一直在努力


还值得注意的是,许多其他形式的人格证明存在更糟糕的可访问性问题。除非您已经认识社交图中的某个人,否则加入基于社交图谱的人格证明系统非常困难。这使得此类系统很容易被限制在单个国家的单个社区内。

即使是集中式身份系统也吸取了这一教训:印度的Aadhaar ID 系统是基于生物识别的,因为这是快速加入其庞大人口的唯一方法,同时避免重复和虚假账户的大规模欺诈(从而节省大量成本)。整个 Aadhaar 系统在隐私方面比加密社区内大规模提议的任何系统都要弱得多。

从可访问性的角度来看,性能最好的系统实际上是像“人性证明”这样的系统,您只需使用智能手机即可注册 - 不过,正如我们已经看到的和我们将看到的,此类系统会带来各种其他权衡。

生物识别身份证明系统存在哪些中心化问题?

有三种:

  1. 系统顶层治理的中心化风险(尤其是当系统中不同参与者主观判断不一致时做出最终顶层决策的系统)。
  2. 使用专用硬件的系统所特有的集中化风险。
  3. 如果使用专有算法来确定谁是真正的参与者,则存在中心化风险。

任何身份证明系统都必须应对 (1),也许“接受的”ID 集完全是主观的系统除外。如果一个系统使用以外部资产(例如 ETH、USDC、DAI)计价的激励,那么它就不可能是完全主观的,因此治理风险就不可避免。

[2] 对于世界币来说,其风险比人类证明(或 BrightID)要大得多,因为世界币依赖于专门的硬件,而其他系统则不然。

[3] 是一种风险,特别是在“逻辑集中”系统中,只有一个系统进行验证,除非所有算法都是开源的,并且我们可以保证它们实际上正在运行它们声称的代码。对于纯粹依赖用户验证其他用户的系统(例如人性证明),这不是风险。

世界币如何解决硬件中心化问题?

目前,世界币附属实体“ Tools for Humanity”是唯一制作 Orbs 的组织。然而,Orb 的源代码大部分是公开的:您可以在这个 github 存储库中看到硬件规格,源代码的其他部分预计很快就会发布。该许可证是类似于Uniswap BSL的“共享源代码,但在技术上要等到四年后才开源”的许可证之一,除了防止分叉之外,它还防止他们认为不道德的行为 - 他们特别列出了大规模监视和三个国际公民权利宣言

该团队的既定目标是允许并鼓励其他组织创建 Orbs,并随着时间的推移,从 Tools for Humanity 创建的 Orbs 过渡到拥有某种 DAO,批准和管理哪些组织可以创建系统认可的 Orbs。

此设计可能会在两种情况下失败:

  1. 它未能真正去中心化。这种情况的发生可能是由于联合协议的常见陷阱:一个制造商最终在实践中占据主导地位,导致系统重新集中化。据推测,治理可能会限制每个制造商可以生产的有效球体数量,但这需要仔细管理,并且它给治理带来了很大的压力,既要去中心化,又要监控生态系统并有效应对威胁:这是一项艰巨任务比例如。一个相当静态的 DAO,仅处理顶级争议解决任务。
  2. 事实证明,不可能让这种分布式制造机制变得安全。在这里,我看到了两个风险:
    • 针对不良 Orb 制造商的脆弱性:即使是一个 Orb 制造商是恶意的或被黑客攻击的,它也可以生成无限数量的假虹膜扫描哈希值,并为它们提供世界 ID。
    • 政府对 Orbs 的限制:不希望其公民参与世界币生态系统的政府可以禁止 Orbs 进入其国家。此外,他们甚至可以强迫公民扫描虹膜,让政府拿到他们的账户,而公民却没有办法回应。

为了使系统更强大地对抗不良 Orb 制造商,Worldcoin 团队建议对 Orb 进行定期审核,验证它们是否正确构建,关键硬件组件是否根据规格构建,并且在事后没有被篡改。这是一项具有挑战性的任务:它基本上类似于国际原子能机构的核检查官僚机构,但对于 Orbs 来说。我们希望,即使审计制度的实施非常不完美,也能大大减少假球的数量。

为了限制任何确实漏掉的坏球体造成的伤害,采取第二次缓解措施是有意义的。不同宝珠制造商注册的世界ID,最好是不同宝珠注册的世界ID,应该能够相互区分。如果此信息是私人信息并且仅存储在 World ID 持有者的设备上,那也没关系;但它确实需要按需证明。这使得生态系统可以通过按需从白名单中删除单个 Orb 制造商甚至单个 Orb 来响应(不可避免的)攻击。如果我们看到朝鲜政府到处强迫人们扫描眼球,那么这些球体以及它们产生的任何帐户都可能会立即被追溯禁用。

一般人格证明中的安全问题

除了世界币特有的问题之外,还有一些影响总体身份证明设计的问题。我能想到的主要有:

  1. 3D 打印假人:人们可以使用人工智能生成假人的照片,甚至是 3D 打印的假人,这些照片甚至足够令人信服,足以被 Orb 软件接受。即使只有一个团体这样做,他们也可以生成无限数量的身份。
  2. 出售 ID 的可能性:某人可以在注册时提供别人的公钥而不是自己的公钥,从而使该人可以控制其注册的 ID,以换取金钱。这似乎已经发生了。除了出售之外,还可以租用 ID以在一个应用程序中短期使用。
  3. 电话黑客:如果一个人的电话被黑客入侵,黑客可以窃取控制其 World ID 的密钥。
  4. 政府强制窃取身份证:政府可以强迫其公民在出示属于政府的二维码时进行验证。通过这种方式,恶意政府可以获得数百万个 ID。在生物识别系统中,这甚至可以秘密完成:政府可以使用混淆的球体从护照检查站进入其国家的每个人中提取世界身份证。

[1] 特定于生物识别身份证明系统。[2] 和 [3] 对于生物识别和非生物识别设计都是通用的。[4] 两者也是共同的,尽管两种情况所需的技术有很大不同;在本节中,我将重点讨论生物识别案例中的问题。

这些都是相当严重的弱点。有些问题已经在现有协议中得到解决,有些问题可以通过未来的改进来解决,还有一些问题似乎是根本性的限制。

面对虚伪的人我们该怎么办?

对于世界币来说,这比类似人性证明的系统的风险要小得多:面对面的扫描可以检查一个人的许多特征,并且与仅仅深度伪造视频相比,很难伪造。专用硬件本质上比商用硬件更难欺骗,而商用硬件又比验证远程发送的图片和视频的数字算法更难欺骗。

有人可以通过 3D 打印最终欺骗专用硬件吗?大概。我预计,在某个时候,我们会看到保持机制开放和保持安全的目标之间的紧张关系日益加剧:开源人工智能算法本质上更容易受到对抗性机器学习的影响。黑盒算法受到更多保护,但很难说黑盒算法没有经过训练以包含后门。也许ZK-ML 技术可以给我们带来两全其美的好处。尽管在更遥远的未来某个时刻,即使是最好的人工智能算法也可能会被最好的 3D 打印假人所愚弄。

然而,从我与 Worldcoin 和 Proof of Humanity 团队的讨论来看,目前这两个协议似乎都还没有看到严重的深度虚假攻击,原因很简单,雇佣真正的低薪工人代表你注册是相当便宜又方便。

我们可以阻止出售 ID 吗?

从短期来看,阻止这种外包是很困难的,因为世界上大多数人甚至不知道身份证明协议,如果你告诉他们举起二维码并扫描他们的眼睛以获取 30 美元,他们就会去做。一旦更多的人意识到身份证明协议是什么,一种相当简单的缓解措施就成为可能:允许拥有注册 ID 的人重新注册,取消以前的 ID。这使得“ID 出售”的可信度大大降低,因为向您出售 ID 的人可以重新注册,从而取消他们刚刚出售的 ID。然而,要达到这一点,需要协议非常广为人知,并且 Orbs 必须非常广泛广泛使用,使按需注册变得切实可行。

这就是为什么将 UBI 币集成到身份证明系统中很有价值的原因之一:UBI 币为人们提供了一种易于理解的激励:(i) 了解协议并注册,以及 (ii) 立即使用如果他们代表他人注册,请重新注册。重新注册还可以防止电话黑客攻击。

我们可以防止生物特征识别系统中的强制行为吗?

这取决于我们谈论的是哪种强制。可能的胁迫形式包括:

  • 政府在边境管制和其他例行政府检查站扫描人们的眼睛(或脸部,或......),并使用它来登记(并经常重新登记)其公民
  • 政府在国内禁止 Orbs,以防止人们独立重新注册
  • 个人购买身份证后威胁说,如果发现自己的身份证因重新注册而失效,就会对其进行伤害
  • (可能是政府运行的)应用程序要求人们直接使用公钥签名来“登录”,让他们看到相应的生物识别扫描,以及用户当前 ID 和他们通过重新注册获得的任何未来 ID 之间的链接。人们普遍担心,这使得创建伴随一个人一生的“永久记录”变得太容易了。


您所有的 UBI 和投票权都属于我们。图片来源


尤其是在不熟练的用户手中,彻底阻止这些情况似乎相当困难。用户可以离开自己的国家/地区,在更安全的国家/地区的 Orb 上(重新)注册,但这是一个困难的过程且成本很高。在一个真正充满敌意的法律环境中,寻找一个独立的宝珠似乎太困难和冒险了。

可行的办法是让这种滥用行为变得更烦人、更容易被发现。要求一个人在注册时说出特定短语的人性证明方法就是一个很好的例子:这可能足以防止隐藏扫描,要求强制更加明目张胆,注册短语甚至可以包含一份声明,确认被调查者知道他们有权独立重新注册,并可能获得 UBI 币或其他奖励。如果检测到强制行为,则用于集体执行强制注册的设备的访问权限可能会被撤销。为了防止应用程序链接人们当前和以前的 ID 并试图留下“永久记录”,默认的身份证明应用程序可以将用户的密钥锁定在受信任的硬件中,从而防止任何应用程序直接使用该密钥,而无需中间的匿名 ZK-SNARK 层。如果政府或应用程序开发人员想要解决这个问题,他们需要强制使用他们自己的定制应用程序。

通过将这些技术与积极的警惕相结合,将那些真正敌对的政权拒之门外,并保持那些只是中等不良的政权(世界上大部分地区都是如此)的诚实,似乎是可能的。这可以通过像 Worldcoin 或 Proof of Humanity 这样的项目维护自己的官僚机构来完成此任务,或者通过透露有关 ID 如何注册的更多信息(例如,在 Worldcoin 中,它来自哪个 Orb)并保留此分类来完成任务交给社区。

我们可以防止租用ID(例如出售选票)吗?

重新注册并不会阻止出租您的 ID 这在某些应用中是可以的:出租你收取当日 UBI 币份额的权利的成本将只是当日 UBI 币份额的价值。但在投票等应用中,轻松售票是一个大问题。

像MACI这样的系统可以阻止你可信地出售你的选票,允许你稍后再投另一票,使你之前的投票无效,这样就没有人可以知道你是否真的投了这样的票。但是,如果行贿者控制了您在注册时获得的密钥,则这无济于事。

我在这里看到两个解决方案:

  1. 在 MPC 内运行整个应用程序。这也涵盖了重新注册过程:当一个人向 MPC 注册时,MPC 会为他们分配一个 ID,该 ID 与他们的人格证明 ID 分开且不可链接,并且当一个人重新注册时,只有MPC 会知道要停用哪个帐户。这可以防止用户对其行为进行证明,因为每个重要步骤都是在 MPC 内使用只有 MPC 知道的私人信息完成的。
  2. 分散登记仪式。基本上,实现类似面对面密钥注册协议的协议,该协议需要四个随机选择的本地参与者共同注册某人。这可以确保注册是一个“受信任”的过程,攻击者无法在此过程中窥探。

基于社交图谱的系统实际上可能在这里表现得更好,因为它们可以自动创建本地去中心化注册流程,作为其工作方式的副产品。

生物识别技术与身份证明的其他领先候选者(基于社交图谱的验证)相比如何?

除了生物识别方法之外,迄今为止人格证明的主要其他竞争者是基于社交图谱的验证。基于社交图谱的验证系统都遵循相同的原理:如果有一大堆现有的经过验证的身份都证明了您身份的有效性,那么您可能是有效的,并且也应该获得经过验证的状态。


如果只有少数真实用户(意外或恶意)验证虚假用户,那么您可以使用基本的图论技术来设置系统验证的虚假用户数量的上限。资料来源:https ://www.sciencedirect.com/science/article/abs/pii/S0045790622000611 。


基于社交图谱的验证的支持者经常将其描述为生物识别技术的更好替代方案,原因如下:

  • 它不依赖于专用硬件,使其更容易部署
  • 它避免了试图制造假人的制造商与需要更新以拒绝此类假人的 Orb 之间的永久军备竞赛
  • 不需要收集生物识别数据,更加保护隐私
  • 它可能对假名更友好,因为如果有人选择将他们的互联网生活分割成多个相互独立的身份,那么这两个身份都可能得到验证(但维护多个真实且独立的身份会牺牲网络效应,并且会产生网络效应)。成本高,所以这不是攻击者可以轻易做到的)
  • 生物识别方法给出“是人类”或“不是人类”的二元评分,这是脆弱的:被意外拒绝的人最终将根本没有 UBI,并且可能无法参与在线生活。基于社交图谱的方法可以给出更细致的数字分数,这当然对某些参与者来说可能有点不公平,但不太可能完全“非人格化”某人。

我对这些论点的看法是,我基本上同意它们!这些是基于社交图谱的方法的真正优势,应该认真对待。然而,还值得考虑基于社交图的方法的弱点:

  • 引导:对于要加入基于社交图的系统的用户,该用户必须认识已经在图中的人。这使得大规模采用变得困难,并且有可能将世界上在最初的引导过程中运气不好的整个地区排除在外。
  • 隐私:虽然基于社交图谱的方法避免收集生物识别数据,但它们通常最终会泄露有关一个人的社会关系的信息,这可能会导致更大的风险。当然,零知识技术可以缓解这种情况(例如,参见Barry Whitehat 的提议),但是图固有的相互依赖性以及对图进行数学分析的需要使得实现相同级别的数据隐藏变得更加困难您可以通过生物识别技术做到这一点。
  • 不平等:每个人只能拥有一个生物识别ID,但一个富有且社会关系良好的人可以利用他们的关系来生成许多ID。从本质上讲,同样的灵活性可能允许基于社交图谱的系统为真正需要该功能的人(例如活动家)提供多个假名,这也可能意味着更强大和人脉更广的人可以获得更多的假名。有权有势、人脉广泛的人。
  • 陷入中心化的风险:大多数人都懒得花时间向互联网应用程序报告谁是真人,谁不是。因此,存在这样的风险:随着时间的推移,系统将倾向于采用依赖于中心化权威的“简单”方式来加入,而系统用户实际上将成为其社交图谱的“社交图谱”。国家承认哪些人是公民——为我们提供集中的 KYC 以及不必要的额外步骤。

人格证明与现实世界中的假名兼容吗?

原则上,人格证明与各种假名兼容。应用程序的设计方式可以使具有单一身份 ID 证明的人可以在应用程序中创建最多五个配置文件,从而为假名帐户留出空间。甚至可以使用二次公式:N 相当于 $N² 的成本。但他们会吗?

然而,悲观主义者可能会认为,尝试创建一种对隐私更加友好的 ID 形式并希望它实际上能够以正确的方式被采用是天真的,因为当权者并不注重隐私,而且如果一个强大的演员获得了一种可以用来获取有关某人的更多信息的工具,他们就会以这种方式使用它。有人认为,在这样一个世界中,不幸的是,唯一现实的方法是在任何身份解决方案的齿轮上撒沙子,并捍卫一个完全匿名和高信任社区数字孤岛的世界。

我明白这种思维方式背后的原因,但我担心这种方法即使成功,也会导致一个任何人都无法采取任何措施来抵消财富集中和治理集中的世界,因为一个人总是可以假装为一万。反过来,这样的集权点也很容易被当权者占领。相反,我赞成采取温和的方法,我们大力倡导具有强大隐私性的身份证明解决方案,如果需要,甚至可能在协议层包含“N 个帐户 $N²”机制,并创建具有隐私性的东西 -价值观友好有机会被外界接受。

那么...我觉得怎么样?

不存在理想的人格证明形式。相反,我们至少有三种不同的方法范式,它们都有自己独特的优点和缺点。比较图表可能如下所示:


基于社交图谱 通用硬件生物识别 专业硬件生物识别
隐私 低的 相当低 相当高
可访问性/可扩展性 相当低 高的 中等的
去中心化的稳健性 相当高 相当高 相当低
防范“假人”的安全 高(如果做得好的话) 低的 中等的


理想情况下,我们应该将这三种技术视为互补,并将它们全部结合起来。正如印度 Aadhaar 所展示的那样,专用硬件生物识别技术具有大规模安全的优势。他们在权力下放方面非常薄弱,尽管这可以通过让个别球体负责来解决。如今,通用生物识别技术很容易被采用,但其安全性正在迅速下降,而且可能只能再工作 1-2 年。基于社交图谱的系统由数百名与创始团队社交关系密切的人引导,可能会面临不断的权衡,要么完全错过世界大部分地区,要么容易受到他们看不到的社区内的攻击。然而,一个由数千万生物识别 ID 持有者引导的基于社交图谱的系统实际上可以发挥作用。生物识别引导可能在短期内效果更好,


可能的混合路径。


所有这些团队都有可能犯很多错误,商业利益和更广泛社区的需求之间不可避免地存在紧张关系,因此保持高度警惕非常重要。作为一个社区,我们可以而且应该推动所有参与者在技术开源方面的舒适区,要求第三方审计,甚至第三方编写的软件,以及其他制衡。我们还需要在这三个类别中的每一个类别中提供更多替代方案。

与此同时,认识到已经完成的工作也很重要:运行这些系统的许多团队都表现出了比任何政府或主要企业运行的身份系统都更认真地对待隐私的意愿,这是我们所取得的成功。应该建立在.

建立一个有效且可靠的身份证明系统的问题,尤其是在远离现有加密社区的人手中,似乎相当具有挑战性。我绝对不会羡慕那些尝试这项任务的人,而且可能需要数年时间才能找到一个有效的公式。原则上,人格证明的概念似乎非常有价值,虽然各种实现都有其风险,但根本没有任何人格证明也有其风险:一个没有人格证明的世界似乎更有可能成为一个由中心化身份解决方案、金钱、小型封闭社区或三者的某种组合主导的世界。我期待看到所有类型的人格证明方面取得更多进展,并希望看到不同的方法最终汇聚成一个连贯的整体。


Bayesian Games with Intentions

Bayesian Games with Intentions

Adam Bjorndahl Carnegie Mellon University, Pittsburgh, PA, USA 

Joseph Y. Halpern Cornell University, Ithaca, NY, USA 

Rafael Pass Cornell University, Ithaca, NY, USA 

Abstract 

We define Bayesian games with intentions by introducing a distinction between “intended” and “actual” actions, generalizing both Bayesian games and (static) psychological games [1]. We propose a new solution concept for this framework and prove that Nash equilibria in static psychological games correspond to a special class of equilibria as defined in our setting. We also show how the actual/intended divide can be used to implement the distinction between “real” outcomes and “reference” outcomes so crucial to prospect theory, and how some of the core insights of prospect theory can thereby be captured using Bayesian games with intentions.

Neural Networks and the Chomsky Hierarchy

Grégoire Delétang∗, Anian Ruoss∗, Jordi Grau-Moya, Tim Genewein,

Li Kevin Wenliang, Elliot Catt, Marcus Hutter, Shane Legg, Pedro A. Ortega DeepMind
London, UK

Abstract

Reliable generalization lies at the heart of safe ML and AI. However, understanding when and how neural networks generalize remains one of the most important unsolved problems in the field. In this work, we conduct an extensive empirical study (2200 models, 16 tasks) to investigate whether insights from the theory of computation can predict the limits of neural network generalization in practice. We demonstrate that grouping tasks according to the Chomsky hierarchy allows us to forecast whether certain architectures will be able to generalize to out-of- distribution inputs. This includes negative results where even extensive amounts of data and training time never led to any non-trivial generalization, despite models having sufficient capacity to perfectly fit the training data. Our results show that, for our subset of tasks, RNNs and Transformers fail to generalize on non- regular tasks, LSTMs can solve regular and counter-language tasks, and only networks augmented with structured memory (such as a stack or memory tape) can successfully generalize on context-free and context-sensitive tasks.

Parametricity, Automorphisms of the Universe, and Excluded Middle

Authors

Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, Michael Shulman

Abstract 

It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instances of non-parametricity. We also address the interaction between classical axioms and the existence of automorphisms of a type universe. We work over intensional Martin-Löf dependent type theory, and for some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.

Keywords and phrases 

relational parametricity, dependent type theory, univalent foundations, homotopy type theory, excluded middle, classical mathematics, constructive mathematics

Editorial Radical Philosophy

[source] https://https//www.radicalphilosophy.com/wp-content/uploads/2018/01/rp201_editorial.pdf

Critical projects that seek to sustain themselves over a long stretch of time have to change if they are to avoid becoming part of an establishment. And if they are prepared to change, they have to change more than once. Radical Philosophy emerged out of the long 1960s, framed politically by the student movement and the New Left, and intellectually by a rebellion against what the frst issue of the journal termed ‘the poverty of so much that now passes for philosophy’. In the 1980s and 1990s, this was refashioned by a more profound engagement with feminism, ecology and the new social movements, as well as by an attempt to get to grips with both the changing forms of what was then called ‘continental philosophy’ and the consequences of the Thatcherite and Reaganite counter-revolutions. From the early 2000s, when the frst version of the radicalphilosophy.com website went live, the journal sought consistently to expand its geopolitical horizons, with contributions from Latin America, Africa and East Asia - albeit never enough - while publishing important articles that brought philosophical perspectives to a range of new disciplinary and cross-disciplinary areas from media theory, geography and flm studies to architecture, literary and art theory. Throughout this history, we have tried to remain true to our founding ambition to ‘free ourselves from the restricting institutions and orthodoxies of the academic world, and thereby to encourage important philosophical work to develop’. 

One of many self-published left-wing journals that were founded in Britain in the early 1970s, Radical Philosophy is today, however, more or less alone in its continuing independence from corporate publishing and in its political commitment to a collective editorial project. The reasons for this are not hard to see. The material, intellectual and political contexts within which a publication such as ours operates have clearly changed beyond all recognition. We began as a magazine produced on typewriters and photocopiers, with images literally cut and pasted into the text, mailed out by the collective to our readers. The changing shapes and fortunes of independent spaces of the left, and the general penetration of the computer and the internet into everyday practices of writing and reading, have since then dramatically transformed what it means to autonomously produce and distribute a publication like RP. In particular, it became apparent that, for a radical journal committed to the construction of as wide a community of readers and contributors as possible – including those outside the West European and North American academy – it was getting harder and harder to justify the access restrictions under which the magazine had come to operate. Given the new possibilities made available via the internet and ‘print-on-demand’, making a commitment to an equally radical form of openness – in a context where, too often, ‘open access’ has simply meant the revivifcation of the zombie forms of commercial academic publishing – became an increasingly pressing priority. By the end of 2016, as we approached both our forty-ffth birthday and our 200th issue, it thus became evident that we required a renewed confrontation with the altered demands of the philosophical and political present. As such, when fve members of the previous editorial group stepped down in early 2017, we took the opportunity not only to open up and diversify membership of the collective, but also to commit ourselves to rethinking our own means and relations of production – editorial as well as technical – in order to bring new life to the project. 

The means of producing Radical Philosophy evolved from its original DIY ethic to proprietary publishing software that required not simply costly licences and machines for its operation but also an outsourcing of labour and a paywall system to fnance itself. To shake this and the greater problem of centralising the collective’s power around those with the relevant skills and licences, we reconceived our means of production around Free and Open Source Software that inherently accommodates a distribution of labour, and created a new in-house engineering collective to work alongside our editors to develop the journal’s tools and distribution channels. Taking our cue mostly from science publications, we have now turned to the markup language LATEX to produce our print edition and to interface with our newly designed website. Where we formerly relied on software developed according to a logic of capital accumulation, we now operate more autonomously thanks to that developed by our own engineering collective. 

In this new form, Radical Philosophy remains, as it has always been, a collectively edited, independently published and self-produced journal – but one with what is, we hope, a renewed editorial energy and collaborative ethos (if with no less philosophical rigour or critical bite). The longer and newly designed print journal, which will generally appear three times a year, is accompanied by a new website through which we will now be publishing all of our content in freely available form. At the same time, the archive of the last forty-fve years of Radical Philosophy, all the way from issue 1 to 200, is being made fully open with downloadable pdfs of everything that we have published since 1972. 

In the Founding Statement of the Collective published in our frst issue, the journal’s aim was articulated as one of challenging a situation in which philosophy had been made ‘into a narrow and specialised academic subject of little relevance or interest to anyone outside the small circle of Professional Philosophers’. Yet such a challenge was never about just a simple widening of the discipline. Instead, Radical Philosophy has always been about a breaking down of those fundamental institutional divisions that have so impoverished philosophy itself by separating it off both from other knowledges and from a wider political and intellectual culture of the left. The need to elaborate what Adorno once called a philosophising beyond philosophy, whether or not it originates in actual departments of academic philosophy, remains as relevant a task today as it did in 1972. 

There are many reasons for this. In an editorial published on the occasion of our 100th issue, it was remarked that for all the changes it has seen, institutionally, ‘philosophy remains the most traditional and least reformed discipline in the humanities; not least with regard to race and gender’. Sadly, little has changed in this respect over the subsequent years. Amidst the current groundswell of demand for the decolonisation of knowledge, philosophy remains a central battleground, stubbornly resistant to the change that those storming its bastions wish to see. The analysis of how philosophical texts are entangled in the sordidness of the world and the evaluation of what, if anything, might be salvaged from their disentanglement, can be destabilising for a whiteness and a patriarchy that regard such texts as foundational to their very self-conception. We hope that, among other things, the pages of Radical Philosophy will become a venue for refection upon the question of what it might mean to decolonise philosophy today. Alongside the translation and introduction of new authors, such an enterprise entails a profound questioning of the very notion of canonicity and the essence of the method of reason that calls itself philosophical. It is in keeping forever open the question of what it might mean to do philosophy that the project of a radical philosophy can remain truly radical. RADICAL PHILOSOPHY 2.01 3

Nash, Conley, and Computation: Impossibility and Incompleteness in Game Dynamics

Jason Milionis Columbia University jm@cs.columbia.edu Christos Papadimitriou Columbia University christos@columbia.edu Georgios Piliouras SUTD georgios@sutd.edu.sg Kelly Spendlove University of Oxford spendlove@maths.ox.ac.uk 

Abstract 

Under what conditions do the behaviors of players, who play a game repeatedly, converge to a Nash equilibrium? If one assumes that the players’ behavior is a discrete-time or continuous-time rule whereby the current mixed strategy profile is mapped to the next, this becomes a problem in the theory of dynamical systems. We apply this theory, and in particular, the concepts of chain recurrence, attractors, and Conley index, to prove a general impossibility result: there exist games for which any dynamics is bound to have starting points that do not end up at a Nash equilibrium. We also prove a stronger result for 𝜖-approximate Nash equilibria: there are games such that no game dynamics can converge (in an appropriate sense) to 𝜖-Nash equilibria, and in fact, the set of such games has a positive measure. Further numerical results demonstrate that this holds for any 𝜖 between zero and 0.09. Our results establish that, although the notions of Nash equilibria (and their computation-inspired approximations) are universally applicable in all games, they are also fundamentally incomplete as predictors of long-term behavior, regardless of the choice of dynamics.