证明论学习笔记4:直觉主义逻辑和相继式演算

目录:类型论驿站写作计划

上一篇:证明论学习笔记3:自然演绎


在讨论直觉主义逻辑之前,我们先看一下用相继式演算(sequent calculus)表示的经典逻辑的自然演绎规则:


相继式式的经典逻辑( \mathcal{C} )自然演绎规则

  • 合取引入: \frac{\Gamma \vdash A \phantom{two} \Delta \vdash B}{ \Gamma, \Delta \vdash A\wedge B}\wedge i
  • 合取消除: \frac{\Gamma \vdash A\wedge B}{\Gamma \vdash A}\wedge e_1,\frac{\Gamma \vdash A\wedge B}{\Gamma \vdash B}\wedge e_2
  • 析取引入: \frac{\Gamma \vdash A}{\Gamma \vdash A\vee B}\vee i_1,\frac{\Gamma \vdash B}{\Gamma \vdash A\vee B}\vee i_2
  • 析取消除: \frac{\Gamma \vdash A\vee B\phantom{tw} \Delta,A\vdash C\phantom{tw} \Theta,B\vdash C }{\Gamma,\Delta,\Theta \vdash C}\vee e
  • 箭头引入: \frac{\Gamma,A \vdash B}{\Gamma \vdash A\to B}\to i
  • 箭头消除: \frac{\Gamma \vdash A\phantom{tw}\Delta\vdash A\to B}{\Gamma,\Delta\vdash B}\to e
  • 否定引入: \frac{\Gamma,A\vdash B}{\Gamma\vdash A\to B}\neg i
  • 否定消除: \frac{\Gamma\vdash A\phantom{tw}\Delta \vdash \neg A}{\Gamma,\Delta\vdash \bot}\neg e
  • 谬误没有引入规则
  • 谬误消除: \frac{\Gamma \vdash \bot}{\Gamma \vdash A}\bot e
  • 全称引入: \frac{\Gamma \vdash A(y)}{\Gamma \vdash \forall x.A(x)}\forall i
  • 全称消除: \frac{\Gamma \vdash \forall x.A(x)}{\Gamma \vdash A(t)}\forall e
  • 存在引入: \frac{\Gamma \vdash A(t)}{\Gamma \vdash \exists x.A(x)}\exists i
  • 存在消除: \frac{\Gamma \vdash \exists x.A(x)\phantom{tw} \Delta,A(y)\vdash B }{\Gamma,\Delta \vdash B}\exists e
  • 双重否定: \frac{\Gamma \vdash \neg\neg A}{\Gamma \vdash A}\neg\neg

在全称引入中, y 不能在 \GammaA(x) 中自由出现;在存在消除中, y 不能在 \GammaA(x) 或者 B 中自由出现。


除了"双重否定"之外,其余的规则要么是引入规则,要么是消除规则,具有很好的对称性。将"双重否定"这一规则删去,我们就得到了直觉主义逻辑 \mathcal{I} .


但值得注意的是,直觉主义逻辑否定的只是经典逻辑中 A\Leftrightarrow \neg\neg A 的一个方向。由于证明必须具有构造性,我们无法证明 \neg \neg A\Rightarrow A ,但是却可以证明 A\Rightarrow \neg\neg A 。先对 A\vdash A\neg A\vdash \neg A 应用否定消除,得到 A,\neg A\vdash \bot ,再应用否定引入规则,得到 A\vdash \neg A\to \bot ,而 \neg A\to \bot 恰恰是 \neg\neg A 的一未归约式。


从实际证明的角度来讲,有些自然演绎规则是很有用的,例如合取引入规则 \frac{\Gamma \vdash A \phantom{two} \Delta \vdash B}{ \Gamma, \Delta \vdash A\wedge B}\wedge i 。如果我们要找到 \Gamma,\Delta \vdash A\wedge B 的证明,只需要分别找到 \Gamma\vdash A\Delta\vdash B 的证明就好了。但是,有些规则对于寻找证明来说帮助不大,例如合取消除规则。如果要证明"张三是老师",沿着合取消除规则,我们可以证明"张三和李四是老师"。但"张三和李四是老师"的证明其实比"张三是老师"的证明更难。此外,我们也无法运用否定消除规则来证明 \Gamma\vdash \bot


为此,根岑提出了一种新的子逻辑式概念(参见:证明论学习笔记1:预备知识):


根岑子逻辑式(Gentzen subformula):

  • \bot 是所有逻辑式的子逻辑式
  • AA\neg A 的子逻辑式
  • ABB\vee C, B\wedge CB\to C 的子逻辑式
  • 如果 \forall x.B\exists x. BA 的子逻辑式,那么 B[x:=t] 也是 A 的子逻辑式。其中 t 是所有不包含 x 的项。


定义(子逻辑式特性,subformula property):

证明法则 \frac{\Gamma\vdash A}{\Gamma' \vdash A'} 拥有子逻辑式特性,如果 \Gamma\cup\{A\} 中的每一个逻辑式都是 \Gamma'\cup\{A'\} 中一个逻辑式的子逻辑式。


子逻辑式特性可以用来逆推证明。自然演绎规则里的引入规则都具备子逻辑式特性。但它的消去规则都不具备子逻辑式特性。为了确保子逻辑式特性,我们可以将消去规则删除,增加新的一组引入规则,即在语境中引入逻辑运算符的规则,我们称之为"左引入规则",与之前介绍的引入规则("右引入规则")相对应。


简而言之,如果引入的运算符出现在 \vdash 左侧,则为左引入规则,如果引入的运算符出现在 \vdash 右侧,则为右引入规则。根岑的 \mathcal{I} 规则罗列如下:


结构规则(structural rules)

  • \Gamma,A\vdash A (包含)
  • \frac{\Gamma\vdash C\phantom{tw}\Delta,C\vdash A}{\Delta,\Gamma \vdash A} cut (切)
  • \frac{\Gamma\vdash\bot}{\Gamma\vdash A}mono_r (右单调)
  • \frac{\Gamma\vdash A}{\Gamma, B\vdash A}mono_l (左单调)


逻辑规则(logical rules):

  • 右合取: \frac{\Gamma \vdash A \phantom{two} \Delta \vdash B}{ \Gamma, \Delta \vdash A\wedge B}\wedge r
  • 左合取: \frac{\Gamma, A, B \vdash C}{\Gamma, A\wedge B \vdash C}\wedge l
  • 右析取: \frac{\Gamma \vdash A}{\Gamma \vdash A\vee B}\vee r _1,\frac{\Gamma \vdash B}{\Gamma \vdash A\vee B}\vee r_2
  • 左析取: \frac{\Gamma, A \vdash C\phantom{tw} \Delta, B\vdash C}{\Gamma,\Delta, A\vee B \vdash C}\vee l
  • 右箭头: \frac{\Gamma,A \vdash B}{\Gamma \vdash A\to B}\to r
  • 左箭头: \frac{\Gamma \vdash A\phantom{tw}\Delta,B\vdash C}{\Gamma,\Delta, A\to B\vdash C}\to l
  • 右否定: \frac{\Gamma,A\vdash B}{\Gamma\vdash A\to B}\neg r
  • 左否定: \frac{\Gamma\vdash A}{\Gamma,\neg A\vdash \bot}\neg l
  • 右全称: \frac{\Gamma \vdash A(y)}{\Gamma \vdash \forall x.A(x)}\forall r
  • 左全称: \frac{\Gamma, A(t)\vdash C}{\Gamma,\forall x.A(x)\vdash C}\forall l
  • 右存在: \frac{\Gamma \vdash A(t)}{\Gamma \vdash \exists x.A(x)}\exists r
  • 左存在: \frac{\Gamma, A(y) \vdash C}{\Gamma,\exists x.A(x) \vdash C}\exists l


除了"切"之外,上述规则均满足子逻辑式特性。根岑于是又提出了著名的"切消定理",即所有用到切的证明均可用没有用到切的证明来代替。



目录:类型论驿站写作计划

上一篇:证明论学习笔记3:自然演绎



参考文献:

Basic proof theory

Handbook of Logic in Computer Science



来源:知乎 www.zhihu.com
作者:Arjuna

【知乎日报】千万用户的选择,做朋友圈里的新鲜事分享大牛。 点击下载

2018 年汉诺威工业展(HANNOVER MESSE)都有哪些值得关注的看点?

今年的汉诺威工业博览会已经落下帷幕,我们也借机为您带来一篇由西门子两位专家共同撰写的文章,不仅总结了本次博览会上诸多企业展示的领先科技,也分享了他们从本次博览会看到的未来制造业。

以下为原文:


见龙在田——2018汉诺威五大趋势注解智能制造未来

谷雨,是中国二十四节气中春季的最后一个节气,每年过了这个时候,华夏大地都会呈现出一幅「杨花落尽子规啼」的暮春画卷。可此时德国的北方小镇汉诺威,却依旧时不时下起冰冷的细雨,不过这依旧阻不住世界各国制造业的同仁们不远万里欣然来此云集,共赴一年一度的全球制造业盛宴——HANNOVER MESSE(汉诺威工业博览会)。

之所以如此,是因为HANNOVER MESSE始终代表着世界制造业发展的风向标。

2013年HANNOVER MESSE,德国首次吹响了工业4.0的集结号,翻开了制造业走向数字化、网络化、智能化的新篇章。

近三年的汉诺威博览会以「产业集成」为核心,为我们展示了走向工业4.0的道路会是什么样的。

2016的年HANNOVER MESSE以「产业集成——探索未来」为主题,德美两大全球工业技术先驱强强联手,再度点燃第四次工业革命的圣火,以西门子为代表的数字化领跑者以落地的智能制造解决方案首次填补了一度被公众所质疑的理论与实践之间的鸿沟,再次将工业4.0推向舆论之巅。

「产业集成——创造价值」为主题的2017年HANNOVER MESSE,业界同仁越发立足于实际、更具有针对性地聚焦制造与能源企业痛点等特性,真正开辟世界制造业全面走向数字化的新纪元。这一年,工业物联网与生态系统的概念尚在襁褓之中,西门子围绕其基于云的工业物联网操作系统MindSphere所构建的生态系统便已经初具规模。

今年HANNOVER MESSE的主题是「产业集成——连接与协作」。又经过一年的荡涤与积淀,智能制造开始真正从概念走向落地,在探索与实践中,业界的广泛共识是,多方以多种形式连接,形成能够通力协作的有机整体,方能更有效地应对智能制造这种复杂系统工程。而笔者在今年的展会上的所见所闻,也恰恰印证了这一主题。

纵观2018年HANNOVER MESSE,笔者认为至少有五大趋势值得业界同仁关注:

一、从单兵作战到生态系统整合

正所谓「孤掌难鸣」,似乎大家都越来越清楚地意识到,单凭一己之力,根本无法应对数字化转型的需求,更莫谈实现智能制造与未来工业4.0愿景。

站在解决方案供应商的角度,这种体会更加明显。因此大家纷纷开始通过「合纵连横」扩展自己的疆域,在具体的操作方法上,可谓八仙过海,各显神通。

作为数字化制造领域的准全能选手,西门子基于自有软硬件产品所打造的数字化解决方案,已然足以全面覆盖离散、过程与混合行业。数字化双胞胎技术在产品设计、生产过程与后续增值服务环节的闭环应用,能够连接物理世界与数字虚拟世界,实现信息的双向流动与持续反馈,为各行各业的客户持续创造价值。

但西门子仍然不愿就此止步,而是以MindSphere为中央枢纽构建生态系统,与各领域的领军企业形成连接,对自身优势进行有效地支撑与补充,不断充实和完善自己在数字化领域的综合交付能力。

甚至自己所在的优势领域,西门子仍不断尝试与合作伙伴展开创新合作,例如与中国本土电子行业系统集成龙头企业博众精工联合展示的消费电子装配解决方案,即是合作的典型代表。生产的数字化双胞胎、AR、边缘计算等应用,都融汇于方案之中。

作为西门子在工业物联网领域合作伙伴,跨界巨人Microsoft围绕Azure云构建的生态系统,显然在谋求更大的布局,ABB、Schneider Electric、Rockwell Automation三大自动化巨头同台竞技,这种组合站位,放之以往恐怕连想都不敢想,是生态思维,把它们连在了一起。

西门子的合作伙伴SAP,在延续去年风格的基础之上,更加注重系统性,众多合作伙伴围绕制造业价值链的各个环节错落分布,而SAP本身则表现得更像一个「串连者」。

构建生态不一定非要靠大平台不可, 连接器制造商HARTING为此做了最好的诠释。HARTING以一款MICA(模块化工业计算架构),逐步向以「连接」为基础的数字化增值服务与集成解决方案供应商转型。如今,围绕MICA平台构建的生态系统已经逐步形成,与40余家合作伙伴共同为能源、电动汽车、数控机床等领域提供服务,甚至也拓展到了预测性维护服务。

类似的交叉站位不胜枚举。在这个市场上,单打独斗的越来越少,相比之下,兵团作战,甚至生态系统级别的高维战法越来越多。

二、从产品思维到系统架构思维

为什么有的展台门庭若市,有的展台却门可罗雀?

抛开跳舞、演杂技的噱头不谈,根本原因是制造业从业者们如今面临越来越复杂的问题,段位越高的玩家,越关心「什么样的顶层设计更能将数字化、智能化技术与自身业务模式匹配与结合并助推整体转型升级?」、「什么样的系统架构规划能够通过跨领域技术的有效融合达到优化整体价值链目标从而全面提升企业综合竞争实力?」、「用什么方法能够解决关键环节的关键问题,同时不影响整体系统的运行效率?」。换而言之,伴随着制造业从业者的认知升级,愿意听具体产品功能介绍的人,越来越少。

其实不仅仅是展会,笔者在日常工作中与客户交流的时候,也面临同样的问题。对客户讲「我这有一大堆好东西,您看看您要点啥」的时代已经过去,针对客户的问题、痛点以及期望通过数字化转型达到的目标,以系统的视角为客户提供整体的解决方案,才能有效满足客户需求。

西门子在工业自动化硬件与工业软件领域具有很强的比较优势,却并没有就产品而论产品,而是针对于不同行业,聚焦企业全价值链,以提供咨询规划服务开始,为客户量身定制顶层设计、整体系统架构、各关键环节的具体解决方案,并以自身技术实力为支撑,通过持续的技术验证确保方案的落地实施。其所面向的客户行业从航空航天、汽车制造、电子装配,到食品饮料,再到石油、化工,不一而足。

无独有偶,Bosch将其应用于制造业多个环节零散软件功能打包命名为Nexeed,以系统视角审视制造企业整个OTD(Order to Deliver)链。

哪怕是传统的传动设备制造商,也已然开始向系统解决方案及综合服务供应商转型,例如齿轮箱与减速机制造商SEW,如今已经以供应链与物流解决方案供应商的形象出现。

无论是传统工业自动化企业跨界工业软件,还是老牌软件供应商跨界制造,亦或两者兼具的工业老司机,似乎大家都洞悉了市场发展趋势,故而殊途同归。

三、从楚河汉界到跨领域技术加速融合

2012年前后,笔者曾经做过三年以上的竞争情报分析工作,其中一种分析方法叫做Benchmarking Analysis(即对标分析法,学名叫做定标比超分析法),这种方法讲究找到与自己业务对应的竞争对手业务,定义KPI进行对比分析。多年来,这项工作一直都非常有效,堪称市场研究与战略的基石之一。

但是后来到了2015年前后,发现越来越做不下去,为什么呢?因为大家的业务构成越来越复杂,维度越来越多,纵横交错,以至于你根本没法对标,即是勉强对上了,最后也会发现,你没有输给对标中的任何一个企业,但你仍然没有显著的增长,还在持续的丢市场份额,整体上越来越无法自恰,甚至到了最后,你连市场定义都很难,因为各领域彼此之间界限,变得越来越模糊,这是跨领域技术融合的结果。

数字化与智能制造加速了跨领域技术之间的集成与融合,OT领域的玩家向上延伸,IT领域的玩家向下延伸,不管自己原先处于什么位置,都在积极扩展自己的疆域。

Phoenix最早期的业务是接线端子,到如今已经是从工业物联网平台,到工程组态集成软件平台,再到PLC等工控产品一应俱全了。

相比之下,海尔从传统的家电业纵身跨越全价值链的生态系统级平台与大规模定制化解决方案供应商的转变,则更加令人激赏。

华为这些年来也是日行千里,基于5G技术探索未来工厂通讯、从边缘到云端,从平台到应用,全面布局工业物联网生态,前不久华为总裁任正非发布的公开信中也提到了「从系统工程角度出发规划华为大生产体系架构,建设世界一流的先进生产体系」,华为进一步跨界无非只是时间早晚的问题。

虽然西门子在二十余年来持续迭代,一路走来,从传统自动化硬件制造商,到如今纵向贯穿企业层、管理层、操作层、控制层直至现场层、横向全面跨越从产品设计、生产规划、生产工程、生产执行直至增值服务完整价值链但是在竞争激烈的市场面前,仍然倍感压力,因此也始终未敢止步。TSN、边缘计算、人工智能、甚至对于区块链在工业领域的应用,都在积极的探索之中。

笔者认为,在数字化转型、实现智能制造,并向工业4.0愿景迈进的未来之路上,跨领域之间技术的融合,仍将不断深化,并且是最可能产生或引发变革的源头。

四、从追求无人化到科技以人为本

从工业4.0诞生伊始,「无人化」的喧哗与躁动就从未停止,时至今日,笔者很欣喜地看到,「人」再次被提升到智能制造的核心位置。显而易见,无论是今天的数字化,还是明天的智能化,都是为了更好地辅助人,而不是取代人。

展会现场上「争奇斗艳」的协作机器人们,有效佐证了这一趋势,高端玩家甚至已经开始将人工智能技术融入其中。

Festo仿生机器人的现场秀固然抢眼,但更强大的其实是他们基于仿生学的理念,借助强大的传感技术、电驱技术,结合虚拟现实与人工智能,打造的能够跟随模仿学习操作人员工作的运动轨迹完成生产作业的协作机器人,这种解决方案,远比在预编程的情况下仅能完成固定路径作业的机械手,高出不止一个段位。

Rethink的智能协作机器人Sawyer也毫无悬念的再一次震撼了我,同样无需编程,能够根据操作人员的手把手作业,在系统中自动形成编程程序,同时系统对机器人作业进行实时仿真,并对数据进行监测与可视化,从而打造数字化双胞胎。

然而,出乎笔者意料的是,以往只存在于幻想中的智能协作机器人,居然出现在西门子的展台上——西门子与KUKA联合打造的Autonomous协作机器人。

这个表面看似稀松平常的解决方案,强大之处在于:机器人作业不但不需要编程,甚至不用人工手把手试教,而是由人直接对系统发布指令(例如:组装某款产品),机器人可以通过机器视觉所「看到」的零部件的位置,自主规划最优工作路径完成作业,在这个过程中,如果有人干扰了作业,比如更换了零件的位置,机器人会根据实际情况自主判断,并重新规划路径,整个过程系统自动形成编程程序,数字化双胞胎技术,实现虚实精准映射,持续积累数据,以便为未来系统进一步优化做准备……

怎么样?有没有感觉「状多智而近妖」?别害怕,它的存在,依然是为了根据人提出的指令,更好地辅助人工作业。脱离了人,机器甚至连存在的意义都会失去。

五、从数据采集与可视化到基于第五大能源的价值链延伸

针对于工业大数据,笔者清楚地记得去年圈内广泛热议的话题是如何有效地完成数据采集,而如今已经有一半以上的解决方案供应商开始了数据可视化解决方案,不少高端玩家已经开始尝试利用数据为客户创造价值,少数终极玩家甚至已经给出了基于数据分析的高附加值服务。

显而易见,无论是传感器领域、工业自动化领域,还是互联网、IT、通讯领域的玩家,都清楚地意识到「数据」这一被誉为世界第五大能源的价值所在,于是纷纷来此竞技,希望通过数据分析,实现自身在价值链上的延伸,在工业物联网的助力之下,这种价值链延伸的半径被进一步拉长。

事到如今,要么莫谈大数据,一旦提起这个话题,如果只给大家看几个屏幕、几页PPT,无疑会被嗤之以鼻,甚至诸如设备状态监测与预警、预测性维护等服务,都已经成为比较常规的「数字化服务」,基于数据的机器学习虽然被冠以人工智能的帽子,但单机效率的优化,早已不算是独门绝学,至少已经通过SIDRIVE IQ将此付诸于实践的西门子,并不将其视为自己的竞争优势。

在数字化服务方面,西门子已经开始尝试更高阶的玩法,例如基于对自己的工厂积累的海量数据进行分析,实现整个电装生产流程的过程诊断、改善点发掘与优化,用数字化的技术手段来主推精益生产的实现。

李杰教授曾经说过,传统的大数据是发散的,而工业大数据是收敛的,重在聚焦。笔者认为,大数据在工业领域的下一步发展,将出现在基于对纵深行业工艺与知识的深度理解,针对具体目标定向精准抓取关键数据后,通过对特定KPI的分析,创造商业洞察。

仍然不足够

制造业的网络化连接,促进了更广泛的企业间协作,使智能制造生态系统不断走向成熟,智能制造的多元性、复杂性与系统性,为跨领域技术的加速融合提供了温床,人本理念让智能化回归本源,为冰冷的科技找回应有的温情,而在整个过程中,数据为我们源源不断地提供动力。

凡此过往,皆为序章。

在可以预见的未来,制造业将在这五大趋势的彼此融通与交互作用中羽翼渐丰,但与此同时,笔者仍然认为变数无疑是存在的,事实上眼下就已经有很多黑应用正在酝酿,例如可能打破传统生产线概念的可重构制造系统,仿生学与机器人、人工智能的结合,以及当前被市场广泛热议的工业区块链,而这也恰恰是最具趣味与令人满怀憧憬的,不是么?


作者简介:

黄昌夏

西门子数字化工厂集团数字化业务高级顾问,南山工业书院研究组成员,参与撰写《中国汽车产业发展报告2017(汽车蓝皮书)》、《美国制造创新研究院解读》等著作。在数字化工厂、工业互联网、制造企业技术战略、智能制造市场发展与生态演进等领域具有独到的见解,业界人称黄小邪。微信号huangchangxia001

王永宗

西门子数字化工厂及过程工业与驱动集团高级销售经理,南开大学MBA,天津市自动化学会理事,数字化研习社数字化制造板块版主,畅销书《大话工业4.0》作者之一,公众号《帝企鹅说》主编。微信号supersamren



来源:知乎 www.zhihu.com
作者:西门子中国

【知乎日报】千万用户的选择,做朋友圈里的新鲜事分享大牛。 点击下载

此问题还有 3 个回答,查看全部。

毕业回国进四大咨询还是四大审计更合适?

题目里面有一些修改,所以答案也相应修改一下吧。

先把评论里的回答放在这里,当作结论:


从一个过来人的角度看,传统四大审计的"咨询"部门根本没资格说审计起点低...


-----------------------------------------------------------------

谢邀。

什么叫"做审计的起点感觉较低"?感觉相当好么……

针对题主的提问,我觉得最不合适的一句话就是这句了。题主也说在内资所有实习经验,也在考CPA了,不懂为什么还觉得审计的起点低。是觉得审计没什么好做了么?我看是因为根本没理解什么是审计吧。

先不说现在的四大咨询部门现在在做什么,或者在招收怎样的人。曾经的四大咨询部门原本都是依托在原有的审计业务中生长起来的。四大咨询部门工作的几大特点:

  1. 业务来自于审计的客户需求;
  2. 人员很多从审计人员(有相当工作经验的)中转;
  3. 核心业务知识点来自于原有的审计业务。

估计头两条都看得懂。第三条看不懂没关系,因为可能你们没有体验更多。

首先,财务审计到底做的是什么。从20年前,面向风险或面向控制的审计概念已经提出。其实审计已经不是单纯的"会计审核"了,审计师从单纯的会计做帐高手,逐步转型为业务专家或行业管理专家。审计师需要知道怎么管理采购,怎么管理销售,怎么管理生产与成本,怎么管理人力资源与薪酬。因而做着做着,开始考虑做咨询业务了。

于此同时,客户的需求也在发生变化,从单纯需要了解怎么做帐,到寻求专业建议,提高管理精细度。因为这方面审计师有优势,他们审计很多客户,知道很多行业里好的做法,可以分享更多的经验给客户。

因此传统四大开始衍生更多的咨询业务。

要知道这类咨询业务与战略咨询,诸如麦家或者波士顿都有不同细分层次。四大的咨询偏重实际操作,更接地气。战略咨询则更加高瞻远瞩一点。因而其实不存在起点低或高端的比较。话说这两类咨询企业是互相diss,看不上的。

现在话说回来,毕业了找什么工作好。审计看似"低端"但是其实给职业生涯能打下不错的基础,包括专业经验、职场经验和人际交往经验。反而直接进入咨询公司,挑战会很大。咨询公司对人的快速学习能力、适应能力都有很高的要求。同时对于专业知识,由于咨询行业是给客户提出咨询建议,所以往往毕业的"小朋友"会被客户视为没有经验,或没资格。所以咨询公司会让小朋友做大量基础工作,这方面和审计公司区别也不大。反而"小朋友"会有很大的失落,以为自己进入"豪门",其实最终也没什么区别。

所以我原答案说了,起点高低在这里其实逻辑不通:

  1. 题主是在比较传统四大的咨询和审计业务,结论是基本没差别;
  2. 题主没有拿战略咨询四大和四大审计比较,他们直接有区别的,但是题主明显没有像这么比;
  3. 题主如果要追求更高工资,那也许可以考虑四大咨询,毕竟上来比审计的工资高一点。然而,一个人的职业生涯很长,难道纠结这头几年的工资差别么?

差不多就这样了。不想把话说太透,题主自己体会。



来源:知乎 www.zhihu.com
作者:行到水穷处

【知乎日报】千万用户的选择,做朋友圈里的新鲜事分享大牛。 点击下载

此问题还有 2 个回答,查看全部。

英国议会人工智能报告十大解读

作者:曹建峰,腾讯研究院高级研究员

【导语】日前,英国议会发布人工智能报告,从其概念、设计、研发和其对工作、生活、医疗等领域的影响以及应对人工智能威胁、塑造人工智能未来等层面进行了有益探索。报告呼吁英国政府制定国家人工智能战略。对于舆论热炒的人工智能监管,报告认为当前不需要对人工智能进行专门监管,各个行业的监管机构完全可以根据实际情况对监管做出适应性调整。相反,报告呼吁英国政府制定国家层面的人工智能准则(AI Code),为人工智能研发和利用设定基本的伦理原则,并探索相关标准和最佳实践等,以便实现行业自律。

英国议会人工智能报告

引言

英国政府高度重视人工智能对经济和社会发展的巨大潜力。此前已发布五份针对或涉及人工智能的政府报告,抢抓机遇并应对挑战。2018年4月16日,英国议会下属的人工智能特别委员会发布长达180页的报告《英国人工智能发展的计划、能力与志向》(AI in the UK: ready, willing and able?),认为英国在发展人工智能方面有能力成为世界领导者。

英国全球一流的人工智能公司,活跃的学术研究文化,生机勃勃的创业生态系统以及法律、伦理、金融和语言学等方面的能力汇聚,为其发展人工智能创造了独一无二的条件。报告旨在支持英国实现人工智能对社会和经济的巨大潜力,同时保护社会免受潜在威胁和危险。

笔者通读报告,总结出了英国议会眼中的人工智能法律政策十大热点问题及相关建议,希冀为国内相关讨论提供借鉴。

1.促进数据访问和共享,最大化公共数据的价值

数据对于人工智能进步的重要性不言而喻。数据是机器学习的核心,有数据,就有巨大优势。这意味着硅谷的科技巨头在开发、应用人工智能系统方面具有巨大优势。相反,中小企业和公共部门则毫无优势。在此背景下,数字技术和人工智能相关的数据争议将持续复杂化。

首要的是区分数据和个人数据。在数据的问题上,所有权的概念与数据不相容,以打电话数据为例,参与的各方都可能主张所有权。因此在法律规则层面使用数据保管和控制等概念更为明确。

在促进数据访问和共享方面,欧盟GDPR规定了数据可携带权,企业必须向用户免费提供其全部的个人数据的副本,这可以避免"锁定"效应,方便用户无缝切换到其他服务,从而促进竞争。此外,医疗、交通、科学、教育等领域存在大量公共数据,自由、公开获取公共数据对于最大化这些数据的价值是极为重要的。

在最大化利用数据的同时,必须最小化对隐私的侵犯。所以需要在数据开放和数据隐私之间寻得平衡。匿名化是有效的技术措施。虽然去识别化后很容易再识别(比如通过与其他数据集交叉引用),但英国数据保护法已将再识别规定为犯罪。

为了促进数据访问和共享,英国议会提出如下建议:1.成立数据信托(data trusts),加强数据访问和共享。2.开放公共数据,同时进行匿名化处理,以维护安全和隐私;公共数据的开放可采取单点分享模式,政府AI办公室和数据伦理和创新中心负责制定需要遵守的适当条款和条件,保护隐私。3.完善和加强个人控制数据的法律和技术机制,实现安全分享个人数据,开放银行数据机制(Open Banking,英国为了促进银行金融服务创新采取的一种金融数据分享机制,通过API工具允许用户将其金融数据安全地分享给第三方)可资借鉴。

2.实现可理解、可信赖的人工智能,避免在特定重大领域采用"黑盒"算法

让人工智能可被开发者、用户、监管者等理解是重要的。然而深度学习系统也就是所谓的"黑盒"系统给理解人工智能提出了挑战。在数据输入和输出的多个分层间,开发者也不清楚到底是哪个因素导致系统做出特定决策。

解决人工智能系统的不可理解性(intelligibility)的一种方案是增加系统的技术透明(technical transparency)。比如将人工智能系统的源代码开放。透明包括事前的透明和事后的透明,不能一味追求事前的透明。

英国议会认为,就如今特定类型的人工智能系统而言,完全实现技术透明是困难的,甚至是不可能的。然而,在安全攸关的特定场景中,技术透明是必须的。这些领域的监管者必须强制要求使用更加透明的人工智能系统,为此可以牺牲系统的能力和准确性。

另一种方案是可解释性,意味着人工智能系统可以解释其决策背后的数据和逻辑。很多企业包括谷歌、微软等都致力于开发可解释的机器学习系统。欧盟GDPR第22条提出的"解释权",某种程度上可以促进解决可解释的人工智能系统的问题。英国数据保护法吸收了"解释权"并更进一步地要求企业将自动化决策的结果告知用户,而且用户有权请求重新考虑该决策或不被算法决策。

英国议会认为,如果人工智能想要成为人类社会中完整且可信赖的工具,研发可理解的人工智能系统就是根本性的。如果人工智能会对个人生活产生重大影响,除非其能够为其决策提出令人满意的解释,否则就不应采用此种系统。就深度神经网络而言,由于不可能实现可解释性,故在找到替代性方案之前应推迟将其用于特定重大领域。数据伦理和创新中心应和相关机构一起制定可理解的人工智能系统的要求指南,并指导企业贯彻指南和相关标准。

3.理解算法歧视,探索针对训练数据和算法的审查、测试机制

新一代人工智能的核心是机器学习,体现为从大量的训练数据集中自动发现模式。如果数据的代表性不足或折射出歧视,则将来决策也可能代表性不足或具有歧视。歧视可能通过多种方式潜入系统,比如可能来源于训练数据、处理的数据或创建算法的人和机构,也可能由于不准确、不完整的数据或算法自身的偏差。如果数据库不准确地反映了现实,或准确地反映了社会中不公平的一面,同样可能产生歧视。

英国议会建议,需要采取更多措施确保数据真正具有代表性,能够代表多元化的人群,并且不会进一步加剧或固化社会不公平。研发人员需要更加深入地理解算法歧视的问题。必须确保处理的数据尽可能平衡且有代表性,研发团队的人员构成是多元化的,能够代表不同社会群体。除了数据歧视的问题,研发人员还必须考虑他们自己有意或无意带入系统的偏见——人类开发者为机器学习算法设置了参数,他们做出的选择不可避免地折射出他们的信念、假设和偏见。这就需要确保研发人员具有多元的性别、种族和社会经济背景并遵守伦理行为准则。

英国议会还建议配置权威的工具和系统,以便审查、测试训练数据,从而确保其足以代表不同群体,确保当被用来训练人工智能系统时,不会导致歧视性决定。

4.警惕数据垄断,更新伦理、数据保护和竞争框架

数据访问和控制是现代人工智能进步的关键要素。数据网络效应(data network effect)可导致特定企业创建私人所有的数据库,占据市场优势。然而,对于数据垄断,人们众说纷纭,未有定论。国际智库数据创新中心认为不存在所谓的基于数据的垄断,赢家也不可能通吃。

英国议会认为,数据的垄断表明需要更强健的伦理、数据保护和竞争框架。并督促政府和竞争执法部门积极审查在英国的大型科技公司的数据使用及潜在的垄断问题。

5.研究并应对法律责任挑战,阐明责任规则及其适用

新技术尤其是人工智能的广泛研发和使用给既有法律和监管框架提出了挑战。比如可能挑战现在的私法概念(合同或侵权)下的法律义务的基础。一个重大的问题是,谁应当为借助或由人工智能做出的决定负责。这可能涉及发放抵押贷款、诊断疾病或自动驾驶汽车做出的决定。最重要的问题可能还是涉及自主机器(autonomous machines)的事故的责任,因为按照既有责任规则,法律主体(自然人或公司)将最终承担责任。

解决法律责任问题是重要的。因为想让人工智能被广泛采用,就必须首先跨越法律责任的障碍。而且法律责任框架和保险对于允许这些系统被实际使用是至关重要的。法律责任和保险的缺失将阻碍技术的采用。

然而,对于是否需要制定新的法律责任规则,各方众说纷纭。有人认为人工智能会给基于合理期待和可预测的责任规则提出重大挑战。另有人认为基于过错的责任体系,依赖于因果链条,将难以适用,因为算法缺乏"合理的可预见性"。但也有人认为法律只适用于人类及其使用技术的方式,所以肯定会有人使用算法,那么可以将责任分配给使用者。

在英国议会看来,可以肯定的是,人工智能系统可能出错,造成损害。但不确定的是,是否需要新的法律责任机制,或者既有责任机制是否是充分的。所以需要进一步研究。英国议会建议法律委员会考虑当前立法在解决人工智能法律责任问题上的充分性,并阐明法律适用问题。并且应当提出关于可责性和可理解性的明确原则。

6.应对人工智能和数据相关的新型网络犯罪活动

人工智能可能成为传统网络攻击的帮凶,导致更大规模的网络攻击。虽然人工智能系统越来越多地被用来增加网络安全,但攻击者可能欺骗人工智能驱动的网络安全系统,导致恶意软件绕过防火墙。

现在关于"恶意人工智能"的研究正在增多,即研究人员如何来欺骗其他人工智能系统做出不准确的归类或决策。图像识别系统最容易遭受此类攻击,比如对图片、三维模型和标志作出细微调整就可以让人工智能系统将其识别为完全不同的物体。在自动驾驶场合,这可能造成汽车车祸。

英国议会认为,初衷美好的人工智能研究可能被用来造成损害,这值得重视。研发人员必须积极考虑其工作的伦理影响,并采取措施防止人工智能滥用。

此外,由于数据成为训练人工智能系统的重要资源,将会产生关于数据破坏的新型犯罪活动,比如摧毁数据,改变数据,注入大量欺骗性数据。因此,英国议会认为应采取措施确保数据的完整性和精确性不被损害,并为私营部门提供如何防止数据库被恶意使用的建议。因此,需要加强研究防止数据破坏的方法,将来形成相关指南。

7.统一自主武器的国际概念,就其开发和使用形成国际共识

人工智能研发最能刺激公众神经的莫过于将其用于军事目的。将人工智能用于后勤、军事战略等非暴力军事应用无可厚非,各界争议最大的主要是所谓的自主武器或者杀手机器人。对于自主武器可能在概念界定上存在困难。但问题的核心在于人类如何控制或监督自主武器,尤其是完全的自主武器,意味着在没有人类干预和指定攻击目标的情况下自主确定攻击目标。

2016年4月,联合国召集94个国家讨论致命自主武器系统(lethal autonomous weapons systems)的问题。讨论是否应当依据《特定传统武器公约》禁止或限制自主武器的开发和使用。2017年11月,86个国家参加了关于武器公约的会议,现在已有22个国家禁止完全自主武器。2017年9月,英国国防部表态称英国当前不拥有完全自主武器(fully autonomous weapon),也无意开发此类武器;并区分了自主武器和自动化武器(automated weapon),其他国家则未作区分。

英国议会认为,英国政府将自主武器界定为"能够理解高级别的意图和指令",这与其他国家的定义不符。这不利于国际社会就自主武器达成共识。因此,建议英国对自主武器的界定和世界其他国家保持一致。

8.成立新的人工智能机构,发挥全方位的战略、咨询和领导作用

为了适应、促进人工智能的发展,英国政府已经宣布成立几个新的人工智能机构。

(1)AI委员会(AI Council)和政府AI办公室(Government Office for AI)。工业战略建议英国政府应与行业和专家一起建立一个AI委员会,帮助协调人工智能在英国的发展。此外,成立一个新的政府AI办公室(Government Office for AI)支持AI委员会。这两个机构的目的主要是促进研究和创新,刺激需求并加速向整个经济部门渗透,推动AI劳动力更加多元,让人们意识到高级数据分析技术的好处和优势。

(2)数据伦理和创新中心(Centre for Data Ethics and Innovation )。这也是工业战略宣布要成立的一个机构。这是全球首个旨在就"符合伦理的、安全的、创新性的数据和人工智能使用"给政府提出建议的咨询机构。该中心将与行业一道建立数据信托(data trusts)。该中心不是监管部门,将在塑造如何利用人工智能方面发挥领导作用。该中心主要职责包括:制定伦理框架,宣传技术的好处,提出政策建议,推动数据信托(即促进数据分享的机制)落地。

(3)全国AI研究所(National AI Institute)。这一角色将由阿兰图灵研究所扮演。旨在借鉴加拿大、德国等国家的成功经验,形成全国人工智能研究的枢纽,引领未来技术发展。

英国议会敦促政府在人工智能领域提供战略领导——制定一份明确的成功路线图。此外,建议政府AI办公室制定国家AI政策框架(即英国人工智能战略),与工业战略步伐一致。新的AI机构的职权范围必须明确。政府AI办公室可以作为其他人工智能机构的协调者。

9.当前阶段没必要对人工智能采取统一的专门监管

对于人工智能监管,存在三种意见:一是既有法律是足够的,因为人工智能往往融入产品和系统,这些产品和系统已经很好地受到了监管,所以不需要对人工智能进行专门监管(specific regulation)。二是需要立即采取新的立法措施,旨在避免意想不到的后果,比如针对算法歧视、不公平等。三是对人工智能监管提出更审慎和分阶段的路径,因为糟糕的监管可能阻碍人工智能发展、创新和竞争,因此可以采取事后监管或者出台伦理框架支持行业自律。此外,人工智能技术发展太快,成文的或专门的立法恐难跟上技术步伐,所以要避免严格、细致的法律要求。

英国议会认为反对专门人工智能监管的理由是让人信服的。其一,企图为所有人工智能应用制定统一的监管机制是不现实的。其二,由于技术发展太快,不可能通过立法进行简单粗暴的监管,倒是可以采取标准、最佳实践等方式。

因此,英国议会认为,在当前阶段,对人工智能采取统一的专门监管是不恰当的。因为各个行业的专门监管机构最能评估人工智能对特定领域的影响并采取适宜的监管措施。当然,政府AI办公室需要与数据伦理和创新中心一道确定潜在的监管鸿沟。

10.制定国家人工智能准则,推动形成人工智能研发和使用的全球共同伦理框架

可以肯定的是,人工智能将会对社会、政治和经济都产生影响。如果发展不好,可能削弱公众对人工智能的信任。因此必须让公众相信,人工智能的使用符合他们的利益,不会被用来剥削或操纵他们。

一些机构和企业已经提出了各自的人工智能伦理原则,如IBM提出了三条原则:AI辅助而非取代人类;AI必须透明;公民和劳动者需要为使用AI产品和服务获得教育和培训。Sage提出了五条,涉及多元化、透明性、可获取性、可责性及辅助而非取代人类。此外,SAP、Nvidia都有类似举措。DeepMind则成立了"人工智能伦理与社会部门",理解人工智能的现实影响并帮助技术人员将伦理付诸实践。在自我监管的框架中,伦理委员会和伦理审查委员会是重要的工具。此外,IEEE、美国人工智能联盟(Partnership on AI)、英国标准组织(BSI)都在推动类似举措。

但英国却缺乏国家层面的人工智能准则。虽然可以将这些原则涵盖进数字宪章(digital charter)或数据科学伦理框架(Data Science Ethical Framework)中,但这些举措进展缓慢,而现在又迫切需要一个规范人工智能系统开发和使用的伦理框架。问题还包括,企业如何将这些原则转变为实践,如不遵守,需要承担多大的责任。这些都需要进一步探讨和研究。

英国议会为人工智能准则(AI Code)的制定提出了五条初步的原则:其一,开发人工智能应当为了共同利益和人类福祉。其二,人工智能的运行应符合可理解原则和公平原则。其三,不应利用人工智能来削弱数据权利或隐私。其四,所有公民都有权获得教育,以便享有人工智能带来的好处。其五,伤害、毁灭或欺骗人类的自主权力绝不应委托给人工智能。

此外,英国议会认为,英国在人工智能领域多方面的优势,使英国有能力在国际舞台上帮助塑造人工智能研发和使用的伦理框架。因此建议政府在2019年的时候,与感兴趣的国家和政府、行业、学术界和民间团体一道在平等的基础上,在伦敦召开全球峰会。这次峰会的目的便是制定人工智能系统开发和使用的全球共同伦理框架。

结语

最后,正如本文开头所说,在人工智能的下一波发展浪潮中,英国具有独一无二的硬实力和优势,有能力成为人工智能领域的全球领导者。如今,英国议会长达180页的综合性人工智能报告,则希望打造英国的人工智能软实力。该报告显示英国不仅对人工智能监管等相关问题有着清晰的认识,而且要将英国的人工智能软实力输出为国际规则,甚至主导国际规则的制定。



来源:知乎 www.zhihu.com
作者:曹建峰(Jeff Cao)

【知乎日报】千万用户的选择,做朋友圈里的新鲜事分享大牛。 点击下载