【译】The challenge of verification and testing of machine learning
在這篇文章中，我們探討了一個機器學習模型能夠擁有的保證類型 。 我們認為，現有防御的局限性表明缺乏對機器學習模型的驗證。 事實上，為了設計可靠的系統，工程師通常參與測試和驗證：
通過測試 ，我們的意思是在幾種條件下評估系統并觀察其行為，觀察缺陷。
通過驗證 ，我們的意思是提出一個令人信服的論點，即該系統不會在非常廣泛的情況下行事不端。
與此問題正交的是哪些輸入值應該經過驗證和測試的問題。 我們是否打算僅對“自然發生的”合法投入進行驗證或測試該系統，還是打算為其任意的退化投入行為提供保證？ 許多軟件系統（如編譯器）對某些輸入有未定義的行為。
我們應該測試還是驗證？ 在哪些投入？
機器學習從業人員傳統上主要依靠測試。 分類器通常通過將分類器應用于從測試集中繪制出的幾個示例并測量這些示例的準確性來進行評估。 根據定義，這些測試程序無法找到可能被錯誤分類的所有可能的以前不可見的例子。
測量測試集錯誤的驗證模擬是統計學習理論[V98]。 統計學習理論保證測試錯誤率不可能超過某個閾值，但這些保證通常非常保守，以至于工程師在實踐中不使用這些保證。
即使應用了統計學習理論，通常也只考慮“自然發生”的輸入：保證是用與訓練數據相同的分布得出的點表示的。
在等式中引入對手
為了提供安全保證，有必要沿著兩條軸進行改進：1）我們必須使用驗證而不是測試; 2）我們必須確保模型在攻擊者制作的異常輸入中安全行事。 從業者想要保證的一個研究得很好的財產是對敵對案例的穩健性 。
測試對抗性示例的魯棒性的自然方法是簡單地評估模型在已經被敵對擾動的測試集上的準確性以創建對抗示例[SZS13]。 這將機器學習中使用的傳統測試方法應用于一組新的輸入。
不幸的是，測試不足以提供安全保證，因為攻擊者可以發送與用于測試過程的輸入不同的輸入。 例如，經過測試并發現對抗對抗式示例生成[GSS14]的快速梯度符號方法的模型可能容易受到更多計算上昂貴的方法的攻擊，如基于數值優化[SZS13]或顯著圖[PMJ16]的攻擊。
一般來說，測試是不夠的，因為它提供了系統故障率的下限 ，當提供安全保證時， 上限是必要的。 換句話說，測試標識 n
導致故障的輸入，所以工程師至少可以得出結論 n 投入導致失敗; 工程師寧愿擁有一種最多變得相當有信心的手段 n輸入導致失敗。
在機器學習環境中遇到的這些測試限制讓人想起在許多其他類型的軟件設計中遇到的情況。 在討論保證程序正確性的方法時，Edsger Dijkstra說：“測試表明存在，而不是缺少缺陷?！?/span>
很顯然， 測試 自然發生的輸入對于傳統的機器學習應用程序是足夠的，但是對于安全保證來說， 驗證 異常輸入是必需的。 我們應該驗證，但到目前為止，我們只知道如何測試 。
當前的機器學習模型非常容易被破壞，因此對異常輸入進行測試足以揭示其缺陷。 希望在不久的將來我們能夠更好地防范敵對的例子。 測試可能不足以揭示這些模型中的缺陷，我們將需要驗證技術來研究新防御的有效性。 正確處理投入空間的保證的發展是ML在對抗環境下的未來的核心，并且它幾乎肯定會以形式驗證為基礎。
ML的理論驗證
機器學習模型對敵對案例的魯棒性的驗證尚處于起步階段。 目前的方法驗證分類器將相同的類分配給點的指定鄰域內的所有點 x
。 在下面的動畫中，我們演示了這種類型的方法，并將其與在同一鄰域中測試各個點進行比較。
研究人員正在努力構建神經網絡的驗證系統。 不幸的是，這些系統還不成熟。 Pulina等人 開發了第一個驗證系統，用于證明神經網絡的輸出類別在所需的鄰域內保持不變[PT10]。 這第一個系統僅限于一個隱藏層，并且僅在具有少于十幾個隱藏單元的網絡上進行演示。 另外，使用約束來近似S形激活函數以將問題減少到SAT。
后來，黃等人。 對這種初始方法進行了改進，并提出了適用于現代神經網絡體系結構的新驗證系統[HKW16]。 該系統擴展到更大的網絡，例如ImageNet分類器。 新驗證系統的一個局限性在于它依賴于各種假設 - 例如，神經網絡中只有一部分隱藏單元與每個輸入相關。 這些假設意味著系統不能再提供絕對保證缺乏對抗性的例子，因為違反這些假設的對抗性例子（例如，通過操縱被假定為無關的單位之一）可以逃避檢測。
Reluplex [KBD17]是另一種使用LP解算器擴展到更大網絡的驗證系統。 Reluplex能夠通過專門研究整流線性網絡[GBB11，JKL09，NH10]及其分段線性結構而變得更加高效。
這些現行的核查制度的范圍有限，因為它們僅核實某些特定地點某個指定地區的產出類別保持不變 x
。 這有兩個限制：
我們沒有辦法詳盡列舉所有 x
分類器應該近似于常數的點（我們無法想象所有未來自然發生的輸入）
周圍的社區 x
我們目前使用的是有些武斷和保守的; 我們傾向于使用 Lp由于人類觀察者認為，對于一個足夠小的標準球，所有封閉點應該具有相同的類別，但是實際上，常量類別的區域應該更大并且具有不同的，不規則的，不太容易指定的形狀。
總之，驗證機器學習模型首先要求我們定義一組合法輸入，即我們希望模型正確分類的一組輸入。 這套法律輸入通常比大多數基準中包含的“測試集”大得多。 然后研究人員將不得不設計驗證技術，以有效地保證對整套法律輸入所做的機器學習預測的正確性。 機器學習中經常遇到的挑戰 - 例如需要推廣到新的投入 - 可能使這成為一個特別困難的目標，正如本文中引用的努力[PT10，HKW16，KBD17]所表明的那樣。 如果是這樣的話，其他社區開發的技術可以通過更接近測試的程序對機器學習模型進行部分驗證：一個很好的例子就是模糊測試在計算機安全領域的積極影響。
對抗環境中有沒有“免費午餐”定理？
值得考慮的是沒有驗證系統可能存在的可能性，因為沒有機器學習模型將永遠是完全健壯和準確的。 特別是，在接近新的，以前看不見的合法投入的情況下推廣投入的挑戰 x
似乎很難克服。
在傳統的機器學習環境中，機器學習系統在新的測試點上的預期能力有多明確的理論限制。 例如，“無免費午餐”定理[W96]指出，當對所有可能的數據集進行平均時， 所有監督分類算法在新測試點上具有相同的準確度。
一個重要的開放理論問題是，“不免費午餐”定理是否可以延伸到對抗環境。 如果我們假設攻擊者通過對測試集進行小擾動來操作，那么“無免費午餐”定理的前提是，平均值被用于所有可能的數據集，包括小擾動不應該被分類器忽略的數據集，否更久適用。
根據這個問題的解決方案，攻擊者和維權者之間的軍備競賽可能會有兩種不同的結果。 由于與預測新測試點的正確值相關的固有統計困難，攻擊者可能從根本上具有優勢。 如果我們幸運的話，防御者可能對廣泛的問題類有一個基本的優勢，為設計和驗證具有魯棒性保證的算法鋪平了道路。
有興趣的讀者可以在[PMS16]中找到關于這個問題的初步討論。 該分析描述了模型準確性和對抗性努力的穩健性之間的權衡。 它表明，在存在能夠找到增加學習者損失的分布的對手的情況下，學習者從移動到更豐富的假設類別中受益。 更豐富的假設類被非正式地定義為一個更復雜的假設類別，它可以為任何分布提供較低的最低損失。 因此，在數據有限的情況下可能會出現緊張局勢 - 因為學習更復雜的假設通常需要更多的實踐數據。
使用CleverHans進行可重復測試
盡管從理論角度來看驗證具有挑戰性，但從實際角度來看，即使是簡單的測試也是具有挑戰性的。 假設研究人員提出了一種新的防御程序，并針對特定的對抗性示例攻擊程序評估了防御。 如果最終的模型獲得高準確性，這是否意味著辯護是有效的？ 可能，但也可能意味著研究人員對攻擊的執行力度很弱。 當研究人員針對他們自己的共同防御程序的實施測試所提出的攻擊技術時，會出現類似的問題。
為了解決這些困難，我們創建了CleverHans庫 。 這個庫包含幾個攻擊和防御程序的參考實現。 研究人員和產品開發人員可以使用cleverhans來測試他們的模型，以對抗標準化，最先進的攻擊和防御。 通過這種方式，如果防御對抗cleverhans攻擊獲得高準確性，測試結果顯示防御力強，而且如果攻擊獲得了對抗cleverhans防御的高失敗率，測試結果顯示攻擊強烈。 此外，發表的研究結果可以相互比較，只要它們在類似的計算環境中使用相同版本的CleverHans制作即可。
結論
機器學習模型的驗證仍處于起步階段，因為方法會做出假設，阻止它們提供缺乏對抗性例子的絕對保證。 我們希望我們的讀者能夠得到啟發，解決其中的一些問題。 另外，我們鼓勵研究人員使用CleverHans來提高敵對設置中機器學習測試的可重復性。
致謝
我們要感謝Martin Abadi對這篇文章的草稿的反饋。 感謝Marta Kwiatkowska指出動畫圖例中的顏色錯誤，將測試與驗證進行比較。
References
[GBB11] Glorot, X., Bordes, A., & Bengio, Y. (2011, April). Deep Sparse Rectifier Neural Networks. In Aistats (Vol. 15, No. 106, p. 275).
[GSS14] Goodfellow, I. J., Shlens, J., & Szegedy, C. (2014). Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.6572.
[HKW16] Huang, X., Kwiatkowska, M., Wang, S., & Wu, M. (2016). Safety Verification of Deep Neural Networks. arXiv preprint arXiv:1610.06940.
[JKL09] Jarrett, K., Kavukcuoglu, K., & LeCun, Y. (2009, September). What is the best multi-stage architecture for object recognition?. In Computer Vision, 2009 IEEE 12th International Conference on (pp. 2146-2153). IEEE.
[KBD17] Katz, G., Barrett, C., Dill, D., Julian, K., & Kochenderfer, M. (2017). Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. arXiv preprint arXiv:1702.01135.
[NH10] Nair, V., & Hinton, G. E. (2010). Rectified linear units improve restricted boltzmann machines. In Proceedings of the 27th international conference on machine learning (ICML-10) (pp. 807-814).
[PMJ16] Papernot, N., McDaniel, P., Jha, S., Fredrikson, M., Celik, Z. B., & Swami, A. (2016, March). The limitations of deep learning in adversarial settings. In 2016 IEEE European Symposium on Security and Privacy (EuroS&P) (pp. 372-387). IEEE.
[PMS16] Papernot, N., McDaniel, P., Sinha, A., & Wellman, M. (2016). Towards the Science of Security and Privacy in Machine Learning. arXiv preprint arXiv:1611.03814.
[PT10] Pulina, L., & Tacchella, A. (2010, July). An abstraction-refinement approach to verification of artificial neural networks. In International Conference on Computer Aided Verification (pp. 243-257). Springer Berlin Heidelberg.
[SZS13] Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., & Fergus, R. (2013). Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199.
[V98] Vapnik, V. (1998). Statistical Learning Theory.
[W96] Wolpert, D. H. (1996). The lack of a priori distinctions between learning algorithms. Neural computation, 8(7), 1341-1390.
總結
以上是生活随笔為你收集整理的【译】The challenge of verification and testing of machine learning的全部內容，希望文章能夠幫你解決所遇到的問題。
- 上一篇： 【译】Privacy and machi
- 下一篇： 【译】Federated Learnin