下面只是我的思考笔记，所以会非常自由和不严谨，不论是验证还是AI都不是我的研究方向，存在大量谬误

最近由于课程原因，我开始读一些神经网络相关的东西。 由于我本身的研究还是黑魔法防御术， 神经网络，这种神必的计算机炼丹学的安全问题也让我感受到相比其他至少还有一点兴趣。毕竟神经网络再特殊也只是一种程序， 那么传统的安全方法理应能在这里面得到应用。

什么是神经网络

这个问题做AI的同学比我懂得实在是太多，我实在也没法班门弄斧。但是我想从更加简单的层面，单纯的程序角度，来解构一下神经网络。
首先，神经网络程序和传统程序的有一个很明显的区别，他并不是一个程序。常见的神经网络程序都会分为训练（1）和最后生成的模型（2）两个部分，两个程序。训练程序一般是一个巨大的loop函数，不断的更新矩阵中的参数值，而这个过程中的interesting part是如何更新的问题。这一步从面向语言编程(language oriented programing)的角度来说应当是可以被抽象DSL的部分。我们可以假设有理想语言, 他的语义应当是用于描述这个巨大的loop函数的中间过程，神经元链接方式, 神经元更新方式 加上程序的终止条件 loss函数。这样看来这一部分应当会有一个合适的declarative language(也许是logic式+函数式的混合语言，直觉感觉带类型系统可能会有意义)。
而训练最终得到是一个巨大的矩阵，并把矩阵上记录的输入填入被连接好的神经元当中。这个部分是另一个完全不同的程序，语言的语义在这里其实已经没有必要了。之前都在说神经元，其实我觉得这完全是个误导人的词汇，这个就是一个普通函数，而且这个函数非常简单，他只在某些情况下会有输出， 那么也就是说使用带算数的来抽象应该是够用了。训练完成后运行的那个程序本质是函数之间的组合，而且这个最后组合的函数中的绝大多数一定是deterministic的，甚至可以说逻辑分支几乎是即使是存在递归，递归的深度也非常的浅，并且大多数情况下总能停机(此处存疑，如果有谁能懂的话，希望能告诉我=。=)。

炼丹安全存在形式化表达？

如果我们希望证明一个程序是安全的，那么我们必须定义在这样的程序中什么是安全。目前绝大多数的研究主要聚焦在程序2，也就是训练以后生成好的函数。 给出一个前条件，是对输入数据的某种约束，比如用飞机做例子，两个飞机相遇为了防止碰撞我们可以大致的给出两飞机距离和机体相关数据（特征数据）范围。给出一个后条件，最后神经网络控制器无法算出一个会导致飞机相撞的值域。这个其实是类似霍尔逻辑的表达。如果模型可拆分成子模型，例如有的神经网络是多种不同神经网络的组合，那么根据霍尔逻辑的传递性，应当也可以在模型之间很自然的添加约束，并且实现证明。

说实话如果模型不怎么复杂，特别是针对forward network这个函数就必然是deterministic的，有输入输出严格11对应，那其实就退化到了一个规划问题，给出输入自变量的值域，验证函数输出不在某个返回内。这里的只要算法是complete其实就很完美了。如果再简单一点，把神经元函数限定到Relu，Relu函数基本上就是个线性函数，有的人就会选择直接把问题退化到线性规划。我不喜欢这种做法，这样的退化让方法完全失去了普适性，也就是说基本可以断言，此类方法完全无法扩展到复杂网路，我不觉得这是正确的研究趋势。

但是从这里我们不难看到目前所有的研究都只能验证程序2相关的部分，而对于程序1是直接无视的，但是从编程的角度来说，程序员能控制的最多的其实是程序1，由于神经网络的输入数据非常复杂，往往包含大量的参数（而且参数大量存在非int，bool等简单类型）。也许目前是认为1的部分不可以验证？但是如果能给出程序2的前条件，也就是说我们已经有了程序1的后条件。 对于程序1，他的输入的数据分布能不能作为某种前条件？我这么说实在是不是很好，也就是说如果我们希望验证程序1，那么我们必须找到程序1，训练过程中的不变量，就像要找loop invariant一样才对。

那么传统安全的一些东西能不能用。比如类non-interference，这么说可能不对，因为我们程序中是不存在有高安全变量和低安全变量的。但是由于AI存在某些伦理学上的担忧，比如大家希望两种feature在最终训练出来的模型中是不能有相关系的，比如，性别信息可能对数据引入bias但是我们又希望在训练的时候把这个数据放进去，这种情况产生的一种可能就是某一个至关重要的feature可能和性别之间有练习，我们能否证明在一个良好的模型中这样的联系并不存在？但是这样的话，如何形式化的描述？这是不是一种超性质？我完全没有头绪。但是我觉得存在可能性。

程序分析的视角

从我的直觉可以感受到，AI验证可能可以从传统的模式检查等技术中得到一些验证，而实际上也确实有人去做了，那么作为常见的形式化方法，程序分析能不能用呢。
传统程序分析针对就是我们日常中最常见的程序,这类程序一般拥有非常复杂的程序轨迹(trace)，而程序分析，本质就是设计一种解释器，可靠的去over approximate这些trace, 然后对抽象之后的程序进行运行，得到一些静态性质。但是对于神经网络中的程序2，似乎并不是这样的，除非网络的结构非常复杂，那样程序才会有很多分支，才有用这些技术的价值。也许对于复杂网络，这里存在某些可能性？

Fuzz

Fuzz其实面对的问题也是和程序分析一样的，如果说是trace based fuzzing,我觉得应该没有太大的作用。但是trace说到底也只是观察程序的一种方法，如果我们换个思路，从每个神经元的值变化入手，尝试去使用进化算法，不断删选优秀变异，有没有可能呢？而且这里很明显和Adversal Attack存在某种联系，法兹器可能可以用于生成counter example.但是这真的就只能是我的纯猜测了，如果能有类似的研究我也会很感兴趣？