Tổng quan luận án
Tính cấp thiết và khoảng trống nghiên cứu
Trong những năm gần đây, học sâu (deep learning) đã đạt được nhiều kết quả tương đương hoặc vượt trội so với con người trong các bài toán thực tiễn như phân loại ảnh, nhận dạng đối tượng, nhận dạng khuôn mặt, xử lý ngôn ngữ tự nhiên, xe tự lái, phát hiện mã độc và chăm sóc sức khỏe. Để đánh giá chất lượng của các mô hình học sâu phân loại ảnh, các độ đo truyền thống như độ chuẩn xác (accuracy), độ chính xác (precision), độ hồi tưởng (recall) và điểm số F1 thường được sử dụng phổ biến. Tuy nhiên, các nghiên cứu thực nghiệm đã chứng minh rằng dù mô hình đạt điểm số cao trên các độ đo này, mô hình vẫn bộc lộ điểm yếu lớn về tính chắc chắn (robustness).
Tính chắc chắn của mô hình học sâu là khả năng mô hình nhận diện chính xác nhãn của ảnh đầu vào khi ảnh bị thêm nhiễu đối kháng (adversarial perturbation). Kẻ tấn công có thể cố tình đưa nhiễu đối kháng vào các ảnh vốn được mô hình phân loại đúng để đánh lừa mô hình đưa ra dự đoán sai lệch. Thực tế này dẫn đến nguy cơ mất an toàn nghiêm trọng khi ứng dụng mô hình học sâu trong các hệ thống quan trọng, chẳng hạn như hệ thống nhận diện biển báo giao thông trong xe tự lái bị đánh lừa bởi các miếng dán màu.
Để kiểm thử và nâng cao tính chắc chắn cho mô hình học sâu, các phương pháp hiện hữu bộc lộ bốn khoảng trống kỹ thuật chính:
- Phương pháp kiểm thử hộp trắng sử dụng kỹ thuật thực thi tượng trưng cho mô hình nơ-ron truyền thẳng (tiêu biểu là DeepCheck) có hiệu năng và tỉ lệ tấn công thành công thấp do phụ thuộc vào bộ giải SMT và áp đặt ràng buộc duy trì trạng thái kích hoạt nơ-ron giống với ảnh gốc.
- Các phương pháp tấn công đối kháng có định hướng sinh ảnh tự động dựa trên mạng biến đổi đối kháng (ATN) thiếu tính đa dạng trong việc tạo lập các mẫu thêm nhiễu (chỉ phân bố nhiễu trên toàn bộ điểm ảnh) và tạo ra nhiều nhiễu dư thừa làm giảm chất lượng ảnh đối kháng theo khoảng cách $L_2$.
- Các giải pháp loại bỏ nhiễu dư thừa thuần túy bằng thuật toán tham lam có chi phí tính toán lớn, không đáp ứng được yêu cầu xử lý trong thời gian thực khi số lượng điểm ảnh bị thêm nhiễu gia tăng.
- Các phương pháp phòng thủ nhằm loại bỏ nhiễu đối kháng sử dụng mô hình mã hóa tự động (như MagNet, PuVAE, Defense-VAE) chưa có khả năng xử lý hiệu quả khi đối mặt với các dạng nhiễu đa dạng, phi phân phối Gaussian sinh ra từ nhiều kỹ thuật tấn công khác nhau.
Mục tiêu nghiên cứu
Mục tiêu chung của luận án là đề xuất các phương pháp nhằm đảm bảo tính chắc chắn cho mô hình học sâu phân loại ảnh, bao gồm mô hình mạng nơ-ron truyền thẳng (FFNN) và mô hình mạng tích chập (CNN).
Mục tiêu cụ thể được chia thành hai nội dung chính:
- Mục tiêu cụ thể 1: Nghiên cứu và đề xuất các phương pháp tấn công đối kháng (sinh ảnh đối kháng) nhằm kiểm thử tính chắc chắn của mô hình học sâu với tỉ lệ thành công cao, hiệu năng tốt và chất lượng ảnh đối kháng cao theo các độ đo khoảng cách $L_0$ và $L_2$.
- Mục tiêu cụ thể 2: Nghiên cứu và đề xuất phương pháp loại bỏ nhiễu đối kháng ra khỏi ảnh đầu vào (cải thiện tính chắc chắn) dựa trên mô hình mã hóa tự động để khôi phục khả năng nhận diện chính xác của mô hình học sâu.
Đối tượng và phạm vi nghiên cứu
- Đối tượng nghiên cứu: Các mô hình học sâu phục vụ bài toán phân loại ảnh, cụ thể là mạng nơ-ron truyền thẳng (Feed-Forward Neural Networks - FFNN) và mạng nơ-ron tích chập (Convolutional Neural Networks - CNN).
- Phạm vi nghiên cứu:
- Về dữ liệu: Tập trung vào các bộ dữ liệu ảnh phân loại có kích thước nhỏ, bao gồm ảnh xám kích thước $28 \times 28 \times 1$ (MNIST, Fashion-MNIST, bộ chữ cái viết tay) và ảnh màu kích thước $28 \times 28 \times 3$ (CIFAR-10). Giá trị điểm ảnh được chuẩn hóa về đoạn số thực $[0, 1]$ hoặc số nguyên $[0, 255]$.
- Về phương pháp kiểm thử: Luận án áp dụng phương pháp kiểm thử hộp trắng (white-box testing), trong đó người kiểm thử có quyền truy cập đầy đủ vào kiến trúc và trọng số của mô hình học sâu.
- Về hướng tiếp cận: Nghiên cứu sinh ảnh đối kháng không định hướng (untargeted attack), tấn công đối kháng có định hướng (targeted attack), kỹ thuật tinh lọc giảm nhiễu đối kháng và kỹ thuật phòng thủ lọc nhiễu tiền xử lý trước khi đưa vào mô hình phân loại.
Tổng quan tài liệu và vị trí của luận án
Các hướng nghiên cứu trước trong y văn
Trong việc đánh giá và đảm bảo tính chắc chắn của mô hình học sâu, tác giả điểm lại hai nhánh nghiên cứu chính:
-
Hướng tiếp cận chứng minh tính chắc chắn (Formal Verification):
- Sử dụng bộ giải SMT-Solver: Công trình của Ehlers (2017) [23] và Katz cùng cộng sự (2017) [45] với công cụ Reluplex sử dụng lý thuyết Modulo thỏa mãn để chứng minh hình thức các thuộc tính của mạng nơ-ron.
- Kỹ thuật làm mịn mức trừu tượng và giải thích trừu tượng: Gehr cùng cộng sự (2018) [24] với hệ thống AI2, Singh cùng cộng sự (2019) [102, 103], Mirman cùng cộng sự (2018) [63/85], Raghunathan cùng cộng sự (2018) [86].
- Hạn chế: Khó mở rộng và không hỗ trợ hiệu quả cho các mô hình học sâu có kiến trúc phức tạp hoặc kích thước lớn.
-
Hướng tiếp cận sinh ảnh đối kháng (Adversarial Attack):
- Tấn công không định hướng (Untargeted Attack):
- Fast Gradient Sign Method (FGSM) của Goodfellow cùng cộng sự (2014) [32] sinh nhiễu một bước dựa trên dấu đạo hàm của hàm mục tiêu theo chuẩn $L_\infty$.
- Basic Iterative Method (BIM) của Kurakin cùng cộng sự (2016) [78] mở rộng FGSM qua nhiều bước lặp nhỏ.
- DeepFool của Moosavi-Dezfooli cùng cộng sự (2016) [68] tìm khoảng cách ngắn nhất đến biên phân lớp theo chuẩn $L_2$.
- Momentum Iterative FGSM (MI-FGSM) của Dong cùng cộng sự (2018) [21] tích hợp động lượng vào quá trình lặp gradient.
- Projected Gradient Descent (PGD) của Madry cùng cộng sự (2017) [62].
- DeepCheck của Gopinath cùng cộng sự (2018) [33] sử dụng kỹ thuật thực thi tượng trưng trên mã nguồn C sinh từ mạng FFNN kết hợp bộ giải SMT để tìm ảnh đối kháng theo chuẩn $L_0$.
- Tấn công có định hướng (Targeted Attack):
- L-BFGS của Szegedy cùng cộng sự (2013) [92] tối ưu hóa khoảng cách $L_2$ kết hợp hàm mất mát phân loại đích.
- Phương pháp CW ($L_0, L_2, L_\infty$) của Carlini và Wagner (2017) [13] tối ưu hóa hàm mục tiêu dựa trên giá trị pre-softmax.
- Adversarial Transformation Networks (ATN) của Baluja và Fischer (2018) [5] huấn luyện mạng mã hóa tự động để sinh nhanh ảnh đối kháng có định hướng theo khoảng cách $L_2$.
-
Hướng tiếp cận cải thiện tính chắc chắn (Phòng thủ - Defense):
- Huấn luyện lại mô hình (Adversarial Training): Goodfellow cùng cộng sự [32], Madry cùng cộng sự [62], Tramèr cùng cộng sự [77], Wong và Kolter [53].
- Xây dựng mô hình phân lớp phát hiện ảnh đối kháng: Grosse cùng cộng sự [38], Meng và Chen [66], Metzen cùng cộng sự [104].
- Loại bỏ nhiễu đối kháng khỏi ảnh đầu vào (Denoising/Input Reconstruction):
- MagNet của Meng và Chen (2017) [66] kết hợp bộ nhận diện và bộ lọc nhiễu dựa trên autoencoder.
- PuVAE của Hwang cùng cộng sự (2019) [42] sử dụng mạng mã hóa tự động biến phân có điều kiện (CVAE) để làm sạch ảnh.
- Defense-VAE của Samangouei cùng cộng sự (2018) [57] sử dụng VAE huấn luyện trên dữ liệu đối kháng để tái tạo ảnh sạch.
- Kỹ thuật khôi phục mức điểm ảnh của Liao cùng cộng sự (2018) [109].
Khoảng trống luận án lựa chọn giải quyết
Luận án định vị nghiên cứu vào việc khắc phục các hạn chế cụ thể của các công trình đi trước:
- Khắc phục sự phụ thuộc vào SMT-Solver và việc khóa cứng trạng thái kích hoạt nơ-ron của DeepCheck bằng cách đề xuất phương pháp sử dụng bộ giải phỏng đoán kết hợp thực thi tượng trưng (HA4FNN).
- Khắc phục tính đơn điệu trong phân bố nhiễu và sự tồn tại của nhiễu dư thừa trong phương pháp ATN bằng cách đề xuất cấu trúc ATN khái quát với mẫu thêm nhiễu kết hợp thuật toán tham lam (PatternAttack).
- Khắc phục chi phí thời gian cao của thuật toán tham lam đơn thuần trong việc tối ưu hóa chất lượng ảnh đối kháng bằng mô hình hai pha thô - tinh chế (QI4AE).
- Khắc phục sự suy giảm hiệu quả của các bộ lọc MagNet, PuVAE, Defense-VAE trước các dạng nhiễu đối kháng phi chuẩn bằng mô hình mã hóa tự động tích chập xếp chồng học trên tập dữ liệu đa dạng nhiễu (SCADefender).
Cơ sở lý thuyết và phương pháp nghiên cứu
Khung lý thuyết và các khái niệm cốt lõi
- Mạng nơ-ron truyền thẳng (FFNN): Kiến trúc gồm tầng đầu vào $L_0$, các tầng ẩn $L_i$ và tầng đầu ra $L_h$. Hoạt động của nơ-ron $n_j^i$ tại tầng $L_i$ được biểu diễn bởi:
$$n_j^i = \theta_i \left( \sum_{k} w_{ij,k} n_k^{i-1} + b_j^i \right)$$
với $\theta_i$ là hàm kích hoạt (ReLU ở tầng ẩn, Softmax ở tầng đầu ra), $w_{ij,k}$ là trọng số liên kết và $b_j^i$ là độ chệch (bias). Nơ-ron ở trạng thái kích hoạt nếu giá trị trước kích hoạt lớn hơn 0.
- Mạng nơ-ron tích chập (CNN): Gồm các tầng tích chập (Convolutional), tầng giảm chiều (Pooling/Subsampling), tầng tăng chiều và tầng kết nối đầy đủ (Fully Connected). Luận án khảo sát kiến trúc chuẩn LeNet-5 gồm 7 tầng phục vụ nhận dạng ảnh chữ số.
- Mạng mã hóa tự động (Autoencoder - AE):
- Mạng mã hóa tự động thưa (Sparse AE): Gồm tầng mã hóa ánh xạ ảnh $x \in \mathbb{R}^{d \times 1}$ sang không gian ẩn $z \in \mathbb{R}^{z \times 1}$ ($z < d$) qua $z = \theta_1(W_1 x + b_1)$ và tầng giải mã tái tạo ảnh $x_{out} = \theta_2(W_2 z + b_2)$. Hàm mục tiêu tối thiểu hóa khoảng cách $L_2(x, x_{out})$.
- Mạng mã hóa tự động xếp chồng (Stacked AE): Mở rộng với nhiều tầng ẩn có kích thước giảm dần ở phần mã hóa và tăng dần ở phần giải mã.
- Mạng mã hóa tự động tích chập xếp chồng (Stacked Convolutional Autoencoder - SCAE): Kết hợp các tầng tích chập và chuyển vị tích chập (Deconvolution) nhằm bảo toàn cấu trúc không gian 2D/3D của ảnh.
- Độ đo và tiêu chí đánh giá:
- Khoảng cách $L_p$:
- $L_0$ (khoảng cách Hamming): Đếm số lượng điểm ảnh bị biến đổi.
- $L_2$ (khoảng cách Euclidean): Đo tổng mức độ biến đổi năng lượng điểm ảnh.
- $L_\infty$: Đo mức biến đổi biên độ lớn nhất trên một điểm ảnh đơn lẻ.
- Tỉ lệ thành công (Success Rate - SR):
- Tấn công có định hướng: $SR = \frac{1}{|X_{adv}|} \sum_{x' \in X_{adv}} \mathbb{I}(M(x') = y^*)$
- Tấn công không định hướng: $SR = \frac{1}{|X_{adv}|} \sum_{x' \in X_{adv}} \mathbb{I}(M(x') \neq y_{true})$
- Tỉ lệ giảm nhiễu (Noise Reduction Rate): Được tính bằng $\frac{a - b}{a} \in [0, 1)$, với $a$ là khoảng cách $L_p$ ban đầu và $b$ là khoảng cách $L_p$ sau cải thiện.
- Tỉ lệ phát hiện (Detection Rate - DR): Tỉ lệ các ảnh được khôi phục chính xác nhãn gốc sau khi đi qua bộ lọc:
$$DR = \frac{1}{|X_{def}|} \sum_{x \in X_{def}} \mathbb{I}(M(A(x)) = y_{true})$$
Phương pháp nghiên cứu thực tế
Luận án áp dụng kết hợp các phương pháp kỹ thuật phần mềm và học máy:
- Chuyển đổi mã nguồn và thực thi tượng trưng: Mô hình học sâu được dịch sang chương trình C tương đương, chèn các câu lệnh đánh dấu (markers) để thu vết thực thi (execution path) từ ảnh dự đoán đúng, sau đó trích xuất hệ ràng buộc logic.
- Giải ràng buộc phỏng đoán (Heuristic Solving): Xây dựng thuật toán heuristic tìm nghiệm thay thế việc giải bằng SMT-Solver chính xác nhưng tốn kém tài nguyên.
- Học chuyển đổi đối kháng theo mẫu (Pattern-based Adversarial Transformation): Tích hợp mặt nạ nhị phân định hướng vị trí can thiệp điểm ảnh (vùng biên, vùng nổi bật, vùng nền) vào quá trình huấn luyện mạng autoencoder đối kháng.
- Thuật toán tối ưu hóa tham lam hai mức: Loại bỏ tuần tự các điểm ảnh hoặc giá trị nhiễu không đóng góp vào việc duy trì nhãn đối kháng.
- Tái tạo ảnh sạch bằng mạng tích chập xếp chồng: Thiết kế kiến trúc SCAE huấn luyện trên tập dữ liệu hỗn hợp chứa các ảnh đối kháng sinh từ nhiều thuật toán tấn công khác nhau.
Nguồn tư liệu và dữ liệu thực nghiệm
Thực nghiệm của luận án sử dụng 4 bộ dữ liệu chuẩn trong lĩnh vực phân loại ảnh:
| Bộ dữ liệu |
Mô tả nội dung |
Số ảnh tập học |
Số ảnh tập kiểm thử |
Số nhãn phân lớp |
Định dạng màu |
Kích thước ảnh |
| MNIST |
Chữ số viết tay (0-9) |
60.000 |
10.000 |
10 |
Ảnh xám |
$28 \times 28 \times 1$ |
| Fashion-MNIST |
Hình ảnh sản phẩm thời trang |
60.000 |
10.000 |
10 |
Ảnh xám |
$28 \times 28 \times 1$ |
| CIFAR-10 |
Đối tượng tự nhiên (xe, máy bay, động vật...) |
60.000 (tổng cộng) |
10.000 |
10 |
Ảnh màu RGB |
$28 \times 28 \times 3$ |
| Bộ chữ cái viết tay |
Ký tự chữ cái viết tay tiếng Anh (A-Z) |
297.959 |
74.489 |
26 |
Ảnh xám |
$28 \times 28 \times 1$ |
Về công cụ hỗ trợ giải ràng buộc logic, luận án sử dụng chuẩn định dạng SMT-LIB cùng các bộ giải SMT phổ biến như Z3 Solver và SMT-Interpol làm cơ sở so sánh hiệu năng.
Nội dung chính theo từng chương
Chương 1. Mục tiêu và phạm vi nghiên cứu
Chương 1 thiết lập bức tranh tổng thể về đề tài nghiên cứu. Tác giả phân tích sự phát triển của học sâu trong thị giác máy tính và đặt ra vấn đề then chốt: các độ đo truyền thống không phản ánh đầy đủ chất lượng của mô hình trước các tác nhân tấn công đối kháng. Chương này trình bày chi tiết:
- Đặt vấn đề và 4 bài toán kỹ thuật cần giải quyết.
- Mục tiêu tổng quát và hai mục tiêu cụ thể (tấn công đối kháng và phòng thủ cải thiện tính chắc chắn).
- Phạm vi nghiên cứu về quy mô dữ liệu, loại mô hình (FFNN, CNN) và phương pháp kiểm thử hộp trắng.
- Cây nghiên cứu phân loại các hướng tiếp cận liên quan và định vị 4 đóng góp cốt lõi của luận án: HA4FNN, PatternAttack, QI4AE, SCADefender.
- Sơ đồ quan hệ và bố cục liên kết giữa 7 chương trong luận án.
Chương 2. Kiến thức nền tảng
Chương 2 cung cấp toàn bộ cơ sở lý thuyết toán học và nền tảng kỹ thuật phục vụ các chương đề xuất:
- Mô hình học sâu: Trình bày cấu trúc toán học của mạng nơ-ron truyền thẳng (FFNN) với các hàm kích hoạt ReLU, Softmax; cấu trúc mạng nơ-ron tích chập (CNN) với chi tiết kiến trúc chuẩn LeNet-5 (gồm các tầng $C_1, S_2, C_3, S_4, C_5, F_6$ và tầng đầu ra); thuật toán tối ưu hóa Gradient Descent ngẫu nhiên (SGD) theo công thức cập nhật trọng số $w = w - \eta \cdot \nabla_w M(x)$.
- Mạng mã hóa tự động: Phân tích chi tiết nguyên lý hoạt động, cấu trúc không gian ẩn $z$, và hàm mục tiêu tái tạo $L_2$ của mạng mã hóa tự động thưa, mạng mã hóa tự động xếp chồng, và mạng mã hóa tự động tích chập xếp chồng.
- Tấn công đối kháng: Định nghĩa hình thức về nhiễu đối kháng, ảnh dự đoán đúng, ảnh đối kháng; phân loại tấn công có định hướng và không định hướng; phân tích tính chất đa dạng và tính bất định của nhiễu.
- Các phương pháp tấn công đối chứng: Trình bày chi tiết thuật toán DeepCheck, FGSM, BIM, L-BFGS, CW $L_2$ và mạng ATN gốc kèm các công thức toán học và hàm mục tiêu.
- Các phương pháp phòng thủ đối chứng: Trình bày cơ chế hoạt động của PuVAE (với hàm mất mát kết hợp $L_{KL}, L_2, CE$), MagNet (bộ nhận diện kết hợp bộ lọc nhiễu) và Defense-VAE.
- Bộ giải SMT: Giới thiệu chuẩn cú pháp SMT-LIB, cơ chế khai báo biến, ràng buộc
assert, kiểm tra thỏa mãn check-sat, trích xuất mô hình nghiệm get-model trên công cụ Z3.
Chương 3. Phương pháp sử dụng bộ giải phỏng đoán để tấn công đối kháng không định hướng mô hình nơ-ron truyền thẳng
Chương 3 đề xuất phương pháp HA4FNN (Heuristic-based Attack for Feed-forward Neural Networks) nhằm khắc phục hai hạn chế lớn của DeepCheck là tỉ lệ thành công thấp và thời gian tính toán lớn.
- Quy trình thực hiện:
- Chuyển đổi mô hình: Dịch mô hình FFNN sang chương trình ngôn ngữ C và chèn các câu lệnh đánh dấu (markers) tại các điểm rẽ nhánh của hàm kích hoạt ReLU.
- Thực thi tượng trưng: Chạy chương trình C với đầu vào là ảnh dự đoán đúng $x$ để lấy đường thi hành $tp$, sau đó chuyển đổi đường thi hành thành hệ ràng buộc tượng trưng $C_{hidden}$ kết hợp ràng buộc đầu ra $C_{out}$ ($n_{i}^{pre} < n_{y_{true}}^{pre}$).
- Bộ giải phỏng đoán: Thay vì sử dụng bộ giải SMT với chi phí cao và bắt buộc giữ nguyên trạng thái kích hoạt nơ-ron như DeepCheck, HA4FNN sử dụng bộ giải phỏng đoán để tìm kiếm giá trị điểm ảnh đối kháng mới và cho phép trạng thái kích hoạt nơ-ron của ảnh đối kháng khác với ảnh gốc.
- Kết quả thực nghiệm: Được thực hiện trên 3 bộ dữ liệu MNIST, Fashion-MNIST và bộ chữ cái viết tay. Kết quả chứng minh HA4FNN có tỉ lệ tấn công thành công vượt trội, thời gian giải hệ ràng buộc nhanh hơn đáng kể so với DeepCheck, và có khả năng tạo ra ảnh đối kháng thành công bằng cách chỉ thay đổi duy nhất một điểm ảnh ($L_0 = 1$).
Chương 4. Phương pháp sử dụng mô hình mã hóa tự động để tấn công đối kháng có định hướng mô hình tích chập
Chương 4 giải quyết bài toán kiểm thử tính chắc chắn có định hướng cho mạng nơ-ron tích chập (CNN) thông qua phương pháp đề xuất PatternAttack.
- Nguyên lý phương pháp:
- ATN khái quát (Generalized ATN): Mở rộng mạng biến đổi đối kháng bằng cách tích hợp các mẫu thêm nhiễu (pattern) được xây dựng từ bản đồ nổi bật (saliency map). Kỹ thuật này cho phép kiểm thử viên chủ động định hướng vị trí can thiệp nhiễu vào vùng biên đối tượng, vùng điểm ảnh nổi bật hoặc vùng nền, từ đó nâng cao tính đa dạng của tập ảnh đối kháng sinh ra.
- Thuật toán tham lam khử nhiễu dư thừa: Áp dụng quy trình lặp để loại bỏ các thành phần nhiễu không cần thiết trên ảnh đối kháng do ATN sinh ra, giúp giảm khoảng cách $L_0$ và $L_2$ giữa ảnh đối kháng và ảnh gốc trong khi vẫn duy trì nhãn đích $y^*$.
- Kết quả thực nghiệm: Tiến hành trên bộ dữ liệu MNIST và CIFAR-10. Kết quả chứng minh mô hình ATN khái quát đạt tỉ lệ tấn công thành công cao trên các tập kiểm thử, và thuật toán tham lam giúp đạt tỉ lệ giảm nhiễu đáng kể so với phương pháp ATN nguyên bản.
Chương 5. Phương pháp sử dụng mô hình mã hóa tự động kết hợp thuật toán tham lam để cải thiện chất lượng ảnh đối kháng
Chương 5 phát triển phương pháp QI4AE (Quality Improvement for Adversarial Examples) nhằm khắc phục nhược điểm về hiệu năng tính toán của thuật toán tham lam đơn thuần trong PatternAttack.
- Quy trình hai pha của QI4AE:
- Pha xây dựng (Pha cải thiện mức thô): Ảnh đối kháng sinh bởi các phương pháp tấn công bất kỳ (như FGSM, L-BFGS, CW) được đưa qua một mạng mã hóa tự động (Autoencoder) chuyên biệt để nhanh chóng loại bỏ phần lớn nhiễu dư thừa với chi phí thời gian tính toán rất nhỏ.
- Pha cải thiện (Pha cải thiện mức tinh chế): Ảnh sau khi xử lý thô được đưa tiếp qua thuật toán tham lam để tinh chỉnh và loại bỏ triệt để các điểm nhiễu còn sót lại, tạo ra ảnh đối kháng có chất lượng cao nhất theo chuẩn $L_0$ và $L_2$.
- Kết quả thực nghiệm: Đánh giá trên MNIST và CIFAR-10 đối với các ảnh đối kháng sinh từ nhiều phương pháp khác nhau. QI4AE đạt chất lượng giảm nhiễu tương đương hoặc tốt hơn thuật toán tham lam thuần túy nhưng thời gian thực thi trung bình giảm đi rõ rệt, đáp ứng yêu cầu xử lý quy mô lớn.
Chương 6. Phương pháp sử dụng mô hình mã hóa tự động để cải thiện tính chắc chắn của mô hình tích chập
Chương 6 đề xuất giải pháp phòng thủ SCADefender (Stacked Convolutional Autoencoder-based Defender) nhằm khôi phục độ chính xác cho mô hình CNN khi ảnh đầu vào bị tấn công đối kháng.
- Kiến trúc và cơ chế SCADefender:
- Đa dạng hóa tập dữ liệu huấn luyện: Khác với MagNet (chỉ dùng nhiễu Gaussian) hay PuVAE (dùng ảnh sạch), SCADefender tạo tập dữ liệu học kết hợp giữa ảnh gốc và tập ảnh đối kháng sinh ra từ nhiều phương pháp tấn công không định hướng khác nhau (FGSM, BIM, CW, ATN...).
- Mạng mã hóa tự động tích chập xếp chồng: Thiết kế kiến trúc SCAE gồm nhiều tầng tích chập, tầng giảm chiều, không gian ẩn và các tầng chuyển vị tích chập để học cách tái tạo ảnh sạch từ các dạng ảnh bị biến dạng không gian phức tạp.
- Kết quả thực nghiệm: Thực nghiệm so sánh SCADefender với 3 phương pháp phòng thủ tiêu biểu (PuVAE, MagNet, Defense-VAE) trên 3 bộ dữ liệu MNIST, CIFAR-10 và Fashion-MNIST, áp dụng trên các mô hình kiểm thử $M, F, C$. SCADefender đạt tỉ lệ phát hiện (Detection Rate - DR) trên ảnh đối kháng cao hơn rõ rệt và duy trì độ chuẩn xác tốt trên ảnh sạch với thời gian xử lý trên mỗi ảnh ở mức mili giây.
Chương 7. Kết luận và hướng phát triển tiếp theo
Chương 7 tổng kết toàn bộ các kết quả đạt được của luận án, khẳng định việc hoàn thành các mục tiêu nghiên cứu đã đặt ra, đồng thời thẳng thắn chỉ ra các giới hạn kỹ thuật và vạch ra các hướng mở rộng trong tương lai.
Kết quả và những đóng góp mới
Những đóng góp mới về mặt lý luận và học thuật
- Đề xuất phương pháp HA4FNN: Kết hợp kỹ thuật thực thi tượng trưng trên mã nguồn C với bộ giải phỏng đoán (heuristic solver) để kiểm thử mô hình nơ-ron truyền thẳng. Phương pháp loại bỏ ràng buộc bảo toàn trạng thái kích hoạt nơ-ron, giúp mở rộng không gian tìm kiếm ảnh đối kháng, nâng cao tỉ lệ tấn công thành công và tối ưu hóa thời gian thực thi so với DeepCheck.
- Đề xuất phương pháp PatternAttack: Mở rộng mạng biến đổi đối kháng (ATN khái quát) kết hợp mẫu thêm nhiễu dựa trên bản đồ nổi bật và thuật toán tham lam, giải quyết bài toán tấn công có định hướng đa dạng vị trí nhiễu trên mô hình tích chập và tối ưu hóa chất lượng ảnh đối kháng.
- Đề xuất phương pháp QI4AE: Thiết lập quy trình hai pha kết hợp giữa mạng mã hóa tự động (cải thiện thô) và thuật toán tham lam (cải thiện tinh chế), cung cấp giải pháp nâng cao chất lượng ảnh đối kháng theo chuẩn $L_0, L_2$ với hiệu năng thời gian vượt trội.
- Đề xuất phương pháp SCADefender: Xây dựng mô hình phòng thủ dựa trên mạng mã hóa tự động tích chập xếp chồng được huấn luyện trên tập dữ liệu nhiễu đa dạng, cung cấp cơ chế loại bỏ nhiễu hiệu quả cho mô hình tích chập trước nhiều phương pháp tấn công đối kháng khác nhau.
Đóng góp về mặt thực tiễn
- Toàn bộ 4 phương pháp nghiên cứu đều đã được thiết kế và đóng gói thành các công cụ phần mềm hoàn chỉnh phục vụ kiểm thử và phòng thủ cho mô hình học sâu.
- Các công cụ kiểm thử tính chắc chắn của luận án đã được chuyển giao, triển khai thử nghiệm thực tế tại Công ty TNHH Phát triển Phần mềm Toshiba Việt Nam (TSDV) và nhận được các đánh giá, phản hồi tích cực về tính ứng dụng trong quy trình đảm bảo chất lượng phần mềm học máy.
Hạn chế và hướng nghiên cứu tiếp
Hạn chế của luận án
Dựa trên phạm vi nghiên cứu và nội dung trình bày trong văn bản, luận án còn một số hạn chế:
- Phương pháp HA4FNN mới chỉ hỗ trợ kiểm thử mô hình nơ-ron truyền thẳng (FFNN), chưa hỗ trợ trực tiếp các kiến trúc mạng học sâu phức tạp hơn như mô hình tích chập (CNN) do sự phức tạp và chi phí tính toán lớn trong việc sinh mã nguồn C tương đương và thực thi tượng trưng.
- Phạm vi thực nghiệm của các phương pháp chủ yếu tập trung trên các bộ dữ liệu phân loại ảnh có kích thước nhỏ ($28 \times 28 \times 1$ và $28 \times 28 \times 3$).
- Phương pháp tấn công kiểm thử trong luận án được phát triển dựa trên giả định kiểm thử hộp trắng, đòi hỏi kiểm thử viên phải nắm rõ toàn bộ kiến trúc và trọng số của mô hình mục tiêu.
Hướng nghiên cứu tiếp theo
- Nghiên cứu mở rộng kỹ thuật chuyển đổi mô hình và thực thi tượng trưng của HA4FNN để hỗ trợ các kiến trúc mạng nơ-ron phức tạp hơn như mạng tích chập hoặc mạng nơ-ron hồi quy.
- Mở rộng phạm vi đánh giá và tối ưu hóa các phương pháp đề xuất trên các bộ dữ liệu ảnh có độ phân giải cao hơn và số lượng lớp phân loại lớn hơn.
- Nghiên cứu nâng cao năng lực của mô hình phòng thủ SCADefender nhằm thích ứng với các kỹ thuật tấn công đối kháng mới xuất hiện.
Giá trị tham khảo
Luận án là tài liệu tham khảo chuyên sâu có giá trị đối với các nhóm đối tượng:
- Nghiên cứu sinh và học viên cao học chuyên ngành Kỹ thuật phần mềm, Khoa học máy tính: Có thể tham khảo phương pháp luận kết hợp giữa kỹ thuật phần mềm truyền thống (thực thi tượng trưng, sinh mã nguồn từ mô hình, giải ràng buộc logic) với các mô hình học máy hiện đại trong bài toán đảm bảo chất lượng phần mềm (Software Quality Assurance for AI).
- Giảng viên và nhà nghiên cứu an toàn học máy (Adversarial Robustness / Trustworthy AI): Cung cấp cơ sở lý thuyết chi tiết về các thuật toán tấn công đối kháng ($L_0, L_2, L_\infty$), cấu trúc mạng biến đổi đối kháng ATN và các cơ chế phòng thủ lọc nhiễu dựa trên mạng mã hóa tự động biến phân và tích chập.
- Kỹ sư kiểm thử chất lượng phần mềm và phát triển hệ thống AI trong công nghiệp: Đặc biệt hữu ích trong việc xây dựng các bộ công cụ kiểm thử độ bền vững (robustness testing suites) cho các mô hình phân loại ảnh trước khi triển khai vào các hệ thống đòi hỏi độ an toàn cao (như nhận dạng sinh trắc học, thị giác máy tính cho xe tự lái, phân tích ảnh y tế).
Câu hỏi thường gặp
1. Tại sao phương pháp DeepCheck lại có hiệu năng và tỉ lệ tấn công thành công thấp khi kiểm thử mô hình nơ-ron truyền thẳng?
DeepCheck gặp hiệu năng thấp và tỉ lệ thành công hạn chế do hai nguyên nhân chính:
- Phương pháp sử dụng bộ giải SMT chính xác để tìm nghiệm trên các hệ ràng buộc phi tuyến tính phức tạp, dẫn đến chi phí tính toán rất lớn khi số lượng tầng và nơ-ron tăng lên.
- DeepCheck áp đặt điều kiện nghiêm ngặt yêu cầu ảnh đối kháng phải có cùng trạng thái kích hoạt nơ-ron với ảnh gốc dự đoán đúng. Ràng buộc này làm thu hẹp đáng kể không gian tìm kiếm, trong khi thực tế có nhiều cách biến đổi điểm ảnh tạo thành ảnh đối kháng mà không nhất thiết phải duy trì trạng thái kích hoạt nơ-ron ban đầu.
2. Phương pháp HA4FNN đã cải tiến những điểm cốt lõi nào so với DeepCheck?
HA4FNN đưa ra hai cải tiến cốt lõi:
- Thay thế bộ giải SMT bằng bộ giải phỏng đoán (heuristic solver) để tìm kiếm nghiệm thỏa mãn hệ ràng buộc đầu ra nhanh chóng hơn.
- Loại bỏ hoàn toàn ràng buộc duy trì trạng thái kích hoạt nơ-ron của các tầng ẩn giữa ảnh đối kháng và ảnh dự đoán đúng, cho phép bộ giải tự do tìm kiếm nghiệm trong không gian biểu diễn lớn hơn, giúp nâng cao tỉ lệ thành công và giảm thời gian giải ràng buộc.
3. Phương pháp PatternAttack giải quyết nhược điểm gì của mạng biến đổi đối kháng (ATN) gốc?
Mạng ATN gốc có nhược điểm là thêm nhiễu đồng loạt lên tất cả các điểm ảnh và tạo ra nhiều nhiễu dư thừa theo khoảng cách $L_2$. PatternAttack giải quyết vấn đề này bằng cách:
- Đề xuất kiến trúc ATN khái quát cho phép áp dụng các mẫu thêm nhiễu (pattern) dựa trên bản đồ nổi bật để kiểm soát việc thêm nhiễu vào các vùng ảnh cụ thể (như vùng biên đối tượng hoặc vùng nền), làm tăng tính đa dạng của ảnh đối kháng.
- Tích hợp thuật toán tham lam để loại bỏ các điểm nhiễu không cần thiết sau khi ảnh đối kháng được sinh ra, từ đó nâng cao chất lượng ảnh theo các độ đo $L_0$ và $L_2$.
4. Cơ chế hoạt động của phương pháp QI4AE khác biệt như thế nào so với thuật toán tham lam đơn thuần?
Thuật toán tham lam đơn thuần duyệt và thử loại bỏ từng điểm nhiễu trên toàn bộ ảnh, dẫn đến thời gian tính toán rất lớn khi số lượng điểm ảnh bị biến đổi nhiều. QI4AE chia quá trình tối ưu thành hai pha:
- Pha cải thiện mức thô: Sử dụng mô hình mã hóa tự động (Autoencoder) đã được huấn luyện sẵn để nhanh chóng loại bỏ phần lớn nhiễu dư thừa trên ảnh đối kháng chỉ qua một lần truyền xuôi (feed-forward) với chi phí tính toán cực thấp.
- Pha cải thiện mức tinh chế: Áp dụng thuật toán tham lam trên ảnh đã qua xử lý thô để tinh chỉnh các điểm nhiễu còn lại. Cơ chế kết hợp này giúp đạt tỉ lệ giảm nhiễu cao nhưng tiết kiệm đáng kể thời gian xử lý so với việc chạy tham lam từ đầu.
5. Tại sao mô hình phòng thủ SCADefender lại đạt hiệu quả phát hiện và làm sạch nhiễu tốt hơn các phương pháp MagNet hay PuVAE?
Các phương pháp như MagNet chủ yếu huấn luyện bộ lọc trên nhiễu Gaussian, còn PuVAE huấn luyện trên phân phối ảnh sạch, do đó hoạt động kém hiệu quả khi gặp các dạng nhiễu đối kháng phi chuẩn sinh ra từ các kỹ thuật tấn công phức tạp. SCADefender vượt trội nhờ hai yếu tố:
- Tập dữ liệu huấn luyện của SCADefender được xây dựng đa dạng, kết hợp trực tiếp các ảnh đối kháng sinh ra từ nhiều phương pháp tấn công không định hướng khác nhau (FGSM, BIM, CW, ATN...).
- Sử dụng kiến trúc mạng mã hóa tự động tích chập xếp chồng (Stacked Convolutional Autoencoder) có khả năng học và khôi phục hiệu quả các đặc trưng không gian đa chiều của ảnh, giúp loại bỏ chính xác các dạng nhiễu đối kháng đa dạng trước khi đưa ảnh vào mô hình phân loại.
Kết luận
Luận án tiến sĩ của tác giả Nguyễn Đức Anh đã giải quyết một cách có hệ thống bài toán đảm bảo tính chắc chắn cho các mô hình học sâu phân loại ảnh thông qua 4 đóng góp kỹ thuật chính: HA4FNN, PatternAttack, QI4AE và SCADefender. Công trình bao quát từ việc nghiên cứu các cơ chế tấn công đối kháng hộp trắng trên mạng truyền thẳng và mạng tích chập, tối ưu hóa chất lượng ảnh đối kháng, cho đến việc xây dựng giải pháp phòng thủ lọc nhiễu dựa trên mạng mã hóa tự động tích chập xếp chồng. Các kết quả nghiên cứu đã được kiểm chứng thực nghiệm trên 4 bộ dữ liệu chuẩn (MNIST, Fashion-MNIST, CIFAR-10, bộ chữ cái viết tay), được đóng gói thành các công cụ kiểm thử cụ thể và đã được ứng dụng thử nghiệm thực tế tại doanh nghiệp phát triển phần mềm.