Luận án: Đảm bảo tính chắc chắn mô hình học sâu và phòng thủ tấn công đối kháng

Tổng quan về luận án

Sự bùng nổ của học sâu (Deep Learning) trong thế kỷ 21 đã tạo ra bước nhảy vọt mang tính cách mạng trong thị giác máy tính, xử lý ngôn ngữ tự nhiên và hệ thống tự hành. Tuy nhiên, các mô hình học sâu hiện đại đối mặt với một lỗ hổng bảo mật nghiêm trọng: tính dễ bị tổn thương trước các mẫu đối kháng (Adversarial Examples). Dù đạt điểm số vượt trội trên các thang đo truyền thống như Accuracy hay F1-Score, mô hình vẫn có thể bị đánh lừa bởi các nhiễu đối kháng cực nhỏ mà mắt người không thể nhận biết.

Nghiên cứu của nghiên cứu sinh Nguyễn Đức Anh, thực hiện dưới sự hướng dẫn khoa học của PGS. Phạm Ngọc Hùng (Trường Đại học Công nghệ, ĐHQGHN) và GS. Nguyễn Lê Minh (Viện Khoa học và Công nghệ Tiên tiến Nhật Bản - JAIST), thuộc chuyên ngành Kỹ thuật Phần mềm (mã số 9480103.01), giải quyết bài toán cốt lõi: "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 được chính xác nhãn của ảnh đầu vào khi ảnh này được thêm nhiễu đối kháng."

Khoảng trống nghiên cứu (Research Gaps) trọng tâm được xác định rõ:

1. Hạn chế về hiệu năng và không gian tìm kiếm trong kiểm thử hình thức: Các phương pháp dựa trên kiểm chứng hình thức và thực thi tượng trưng như DeepCheck (Gopinath et al.) bị thắt nút cổ chai do phụ thuộc vào bộ giải SMT (Satisfiability Modulo Theories) và ràng buộc cứng nhắc về việc bảo toàn trạng thái kích hoạt nơ-ron (neuron activation state).
2. Thiếu tính khái quát và đa dạng mẫu nhiễu: Các kỹ thuật sinh ảnh đối kháng kinh điển (FGSM, CW, BIM, L-BFGS) tối ưu hóa độc lập từng ảnh, trong khi mạng biến đổi đối kháng ATN (Baluja et al.) chỉ tối ưu theo chuẩn $L_2$, gây dư thừa nhiễu và không hỗ trợ các mẫu phân bố nhiễu cục bộ theo vùng đặc trưng.
3. Chi phí tối ưu chất lượng ảnh đối kháng cao: Thiếu vắng các giải pháp làm mịn và khử nhiễu dư thừa hoạt động ở mức thời gian thực.
4. Khả năng phòng thủ kém trước phân phối nhiễu phức hợp: Các cơ chế phòng thủ dựa trên Autoencoder hiện thời (MagNet của Meng & Chen, PuVAE, Defense-VAE) chỉ giả định phân phối nhiễu Gaussian đơn giản, dễ bị vô hiệu hóa trước các đòn tấn công đối kháng phi Gaussian đa dạng.

Câu hỏi nghiên cứu và giả thuyết khoa học:

• RQ1: Làm thế nào để tăng tốc độ và tỷ lệ thành công của thực thi tượng trưng khi sinh mẫu đối kháng trên mạng nơ-ron truyền thẳng (FFNN)?
  • H1: Thay thế bộ giải SMT bằng bộ giải phỏng đoán (heuristic solver) kết hợp nới lỏng ràng buộc kích hoạt nơ-ron sẽ mở rộng không gian tìm kiếm và giảm thời gian giải ràng buộc.
• RQ2: Cơ chế nào giúp mô hình hóa việc sinh mẫu đối kháng có định hướng trên mạng tích chập (CNN) vừa có tính khái quát, vừa kiểm soát được mẫu nhiễu đa dạng?
  • H2: Kiến trúc ATN khái quát kết hợp bản đồ nổi bật (saliency maps) cho phép kiểm soát vị trí phân bố nhiễu chính xác với tỷ lệ thành công cao.
• RQ3: Làm sao để loại bỏ nhiễu dư thừa trên ảnh đối kháng với chi phí tính toán thấp?
  • H3: Tiếp cận lai kết hợp mô hình mã hóa tự động (tinh chỉnh thô) và thuật toán tham lam (tinh chỉnh mịn) sẽ tối ưu hóa chuẩn $L_0, L_2$ trong thời gian thực.
• RQ4: Làm thế nào để xây dựng cơ chế phòng thủ độc lập có khả năng kháng đa dạng các hình thức tấn công đối kháng?
  • H4: Huấn luyện mô hình Stacked Convolutional Autoencoder trên tập dữ liệu tổng hợp đa dạng tấn công sẽ tái cấu trúc ảnh sạch hiệu quả trước các nhiễu bất định.

Nghiên cứu được triển khai thực nghiệm trên 4 bộ dữ liệu chuẩn mực: MNIST (70,000 ảnh xám $28\times28$), Fashion-MNIST (70,000 ảnh xám $28\times28$), CIFAR-10 (60,000 ảnh màu $28\times28\times3$) và bộ chữ cái viết tay Handwritten Alphabets (372,448 ảnh xám $28\times28$). Kết quả nghiên cứu không chỉ hoàn thiện khung lý thuyết kiểm thử phần mềm cho Deep Learning mà còn được chuyển giao ứng dụng thực tế tại Công ty TSDV với phản hồi tích cực.

Literature Review và Positioning

Nghiên cứu về tính chắc chắn (Robustness) của mạng học sâu được định vị tại giao điểm giữa Kỹ thuật Phần mềm (Software Engineering - SE) và Trí tuệ Nhân tạo An toàn (Trustworthy AI). Literature review tổng hợp ba dòng nghiên cứu chính:

                                  TIẾP CẬN ĐẢM BẢO TÍNH CHẮC CHẮN CHO DEEP LEARNING
                                                          │
         ┌────────────────────────────────────────────────┼────────────────────────────────────────────────┐
         ▼                                                ▼                                                ▼
[1. Kiểm chứng hình thức & SMT]               [2. Sinh mẫu đối kháng (Adversarial)]          [3. Cơ chế phòng thủ & Phục hồi]
- SMT-Solvers (Reluplex, Katz 2017)           - Phép lặp gradient (FGSM, Goodfellow 2014)    - Huấn luyện đối kháng (Madry 2018)
- Abstract Interpretation (Gehr 2018)          - Tối ưu hóa ràng buộc (CW, Carlini 2017)      - Bộ lọc Autoencoder (MagNet, Meng 2017)
- Symbolic Execution (DeepCheck, 2019)        - Generative/ATN (Baluja & Fischer 2017)       - Biến phân VAE (Defense-VAE, PuVAE 2019)
         │                                                │                                                │
         ▼                                                ▼                                                ▼
  HẠN CHẾ CỐT LÕI:                                 HẠN CHẾ CỐT LÕI:                                 HẠN CHẾ CỐT LÕI:
  Bùng nổ tổ hợp, nghẽn bộ giải SMT,               Thiếu tính khái quát, nhiễu dư thừa,             Chỉ phòng thủ nhiễu Gaussian đơn lẻ,
  ép buộc cùng trạng thái kích hoạt.               không linh hoạt vùng chèn nhiễu.                 vô hiệu trước tấn công phi phân phối.
         │                                                │                                                │
         └────────────────────────────────────────────────┼────────────────────────────────────────────────┘
                                                          │
                                                          ▼
                                            [ĐÓNG GÓP ĐỘT PHÁ CỦA LUẬN ÁN]
                             ┌────────────────────────────┴────────────────────────────┐
                             ▼                                                         ▼
                     [TẤN CÔNG & ĐÁNH GIÁ]                                     [TỐI ƯU & PHÒNG THỦ]
             - HA4FNN: Symbolic Exec + Heuristic Solver               - QI4AE: Autoencoder + Thuật toán tham lam
             - PatternAttack: Saliency-guided Generative ATN          - SCADefender: Stacked Conv-Autoencoder đa phân phối

Dòng nghiên cứu 1: Kiểm chứng hình thức và Thực thi tượng trưng

Các nghiên cứu của Katz et al. (Reluplex, 2017), Gehr et al. (AI2, 2018) và Gopinath et al. (DeepCheck, 2018; 2019) tiên phong áp dụng các phương pháp hình thức vào mạng nơ-ron. Cụ thể, DeepCheck chuyển đổi mô hình FFNN thành mã nguồn C, ghi nhận vết thực thi (execution trace), áp dụng Symbolic Execution và dùng Z3 Solver (De Moura & Bjørner, 2008) để giải hệ ràng buộc. Tuy nhiên, luận án chỉ rõ sai lầm nền tảng: "Yêu cầu trạng thái kích hoạt nơ-ron của ảnh đối kháng phải giống ảnh dự đoán đúng sẽ làm giảm vùng không gian thêm nhiễu đối kháng vào ảnh dự đoán đúng để sinh ảnh đối kháng." Việc phụ thuộc hoàn toàn vào SMT Solver khiến DeepCheck gặp hiện tượng bùng nổ thời gian giải khi độ sâu mạng tăng lên.

Dòng nghiên cứu 2: Tấn công sinh mẫu đối kháng

Szegedy et al. (2013) lần đầu tiên phát hiện tính dễ tổn thương của DNN qua thuật toán L-BFGS. Goodfellow et al. (2014) đề xuất FGSM tối ưu hóa theo chuẩn $L_\infty$ một bước lặp, sau đó được Kurakin et al. (2016) mở rộng thành BIM với nhiều bước lặp vi mô. Carlini & Wagner (CW, 2017) đặt chuẩn mực mới về khả năng vượt qua phòng thủ với các hàm mục tiêu tối ưu chuẩn $L_0, L_2, L_\infty$. Tuy nhiên, các kỹ thuật này phải chạy lại thuật toán tối ưu từ đầu cho từng ảnh mới. Để giải quyết tính khái quát, Baluja & Fischer (2017) đề xuất ATN (Adversarial Transformation Networks) sử dụng mạng nơ-ron để học cách biến đổi ảnh. Điểm yếu của ATN là phân bố nhiễu tràn lan toàn bộ điểm ảnh, không cho phép kiểm tra tính bền vững trên các vùng hình học cụ thể.

Dòng nghiên cứu 3: Phòng thủ dựa trên mô hình biến đổi và phục hồi

Meng & Chen (MagNet, 2017) đề xuất sử dụng Autoencoder làm bộ lọc nhiễu tự nhiên kết hợp bộ phân loại phát hiện bất thường. Sau đó, PuVAE (2019) và Defense-VAE (2019) tích hợp mạng biến phân VAE (Variational Autoencoder) để khôi phục ảnh sạch. Điểm hạn chế cốt tử của MagNet và các biến thể VAE là giả định nhiễu đối kháng tuân theo phân phối Gaussian chuẩn. Khi đối mặt với các dạng tấn công phi tuyến, biến dạng cục bộ hoặc tối ưu hóa gradient cao cấp, tỷ lệ phát hiện và khôi phục của các phương pháp này sụt giảm nghiêm trọng.

Đóng góp lý thuyết và khung phân tích

Đóng góp cho lý thuyết

Luận án mở rộng lý thuyết kiểm thử phần mềm truyền thống (Software Testing Theory) sang miền không gian nơ-ron phi tuyến tính, tạo bước chuyển dịch mô thức (Paradigm Shift) từ kiểm chứng hình thức tuyệt đối (Exact Formal Verification) sang kiểm thử phỏng đoán thích ứng (Adaptive Heuristic Testing):

1. Mở rộng lý thuyết kiểm thử tượng trưng cho DNN: Chứng minh rằng ràng buộc bất biến kích hoạt nơ-ron (neuron activation invariance) là không cần thiết đối với bài toán tìm điểm lỗi phần mềm học sâu. Việc nới lỏng ràng buộc này giúp mở rộng không gian tìm kiếm nghiệm đối kháng lên gấp nhiều lần.
2. Hình thức hóa toán học cho bài toán sinh mẫu theo mẫu hình (Pattern-based Perturbation): Định nghĩa toán học cho ma trận mặt nạ nhị phân dựa trên bản đồ nổi bật Jacobian (JSMA) và đạo hàm riêng, cho phép ánh xạ không gian tối ưu vào các tập con điểm ảnh có chủ đích.
3. Mô hình hóa quá trình phòng thủ không gian đa phân phối: Xây dựng mô hình toán học giải thích cơ chế loại bỏ nhiễu đối kháng bất định thông qua phép biến đổi phi tuyến trong không gian ẩn (latent space) của Stacked Convolutional Autoencoder.

Khung phân tích độc đáo

Khung phân tích của luận án tích hợp bốn trục trụ cột tạo thành một chu trình khép kín:

$$\mathcal{S}_{Framework} = \langle \text{HA4FNN}, \text{PatternAttack}, \text{QI4AE}, \text{SCADefender} \rangle$$

                                      KHUNG PHÂN TÍCH TỔNG THỂ CỦA LUẬN ÁN
                                                       │
                      ┌────────────────────────────────┴────────────────────────────────┐
                      ▼                                                                 ▼
           [GIAI ĐOẠN 1: TẤN CÔNG & ĐÁNH GIÁ]                               [GIAI ĐOẠN 2: TỐI ƯU & PHÒNG THỦ]
         ┌─────────────────────────────────────┐                         ┌─────────────────────────────────────┐
         │  1. HA4FNN (Mô hình FFNN)           │                         │  3. QI4AE (Tối ưu chất lượng ảnh)   │
         │  - Chuyển đổi Model sang C code     │                         │  - Pha 1: Autoencoder lọc thô       │
         │  - Thực thi tượng trưng đường chạy  │                         │  - Pha 2: Greedy Search lọc mịn     │
         │  - Heuristic Solver giải $L_0$      │                         │  - Cắt giảm $L_0, L_2$ thời gian thực│
         └──────────────────┬──────────────────┘                         └──────────────────▲──────────────────┘
                            │                                                               │
                            ▼                                                               │
         ┌─────────────────────────────────────┐                                            │
         │  2. PatternAttack (Mô hình CNN)     │                                            │
         │  - Generalized ATN + Autoencoder    │                                            │
         │  - Sinh nhiễu theo Saliency Pattern │────────────────────────────────────────────┘
         │  - Tối ưu hóa có định hướng         │
         └──────────────────┬──────────────────┘
                            │
                            ▼
         ┌──────────────────────────────────────────────────────────────────────────────────┐
         │  4. SCADefender (Phòng thủ & Tăng cường tính chắc chắn)                          │
         │  - Gom cụm tập mẫu đối kháng đa dạng (FGSM, BIM, CW, ATN...)                     │
         │  - Stacked Convolutional Autoencoder khôi phục phân phối ảnh sạch                │
         │  - Tái cấu trúc và triệt tiêu nhiễu phi Gaussian trước khi phân lớp              │
         └──────────────────────────────────────────────────────────────────────────────────┘

Ranh giới áp dụng (Boundary Conditions) được xác định rõ: Khung phân tích tối ưu cho các bài toán phân loại ảnh đơn kênh (grayscale) và đa kênh (RGB) với kích thước chuẩn hóa, tập trung vào mô hình học sâu hộp trắng (white-box testing) nơi cấu trúc mạng và tham số trọng số hoàn toàn khả truy.

Phương pháp nghiên cứu tiên tiến

Thiết kế nghiên cứu

Nghiên cứu tuân thủ chặt chẽ triết học thực chứng (Positivism) và phương pháp luận thực nghiệm định lượng trong Kỹ thuật Phần mềm. Thiết kế đa tầng kết hợp phân tích tĩnh mã nguồn mô hình, phân tích động vết thực thi và học máy biến đổi.

                      QUY TRÌNH THỰC THI TƯỢNG TRƯNG PHỎNG ĐOÁN TRONG PHƯƠNG PHÁP HA4FNN
                                                       │
                                                       ▼
                                      ┌─────────────────────────────────┐
                                      │ Mô hình nơ-ron truyền thẳng (M) │
                                      └────────────────┬────────────────┘
                                                       │ Translate(M)
                                                       ▼
                                      ┌─────────────────────────────────┐
                                      │  Chương trình C trung gian (p)  │
                                      │  Chèn marker tại các nhánh ReLU │
                                      └────────────────┬────────────────┘
                                                       │ Execute(p, x) với ảnh sạch x
                                                       ▼
                                      ┌─────────────────────────────────┐
                                      │    Vết đường thi hành ($t_p$)    │
                                      └────────────────┬────────────────┘
                                                       │ SymbolicExecution($t_p$)
                                                       ▼
                                      ┌─────────────────────────────────┐
                                      │ Hệ ràng buộc ẩn:                │
                                      │ $c_{hidden} = \bigwedge c_i$    │
                                      │ Ràng buộc đầu ra:               │
                                      │ $c_{out} = \bigvee (n_y < n_i)$ │
                                      └────────────────┬────────────────┘
                                                       │
                                                       ▼
                                      ┌─────────────────────────────────┐
                                      │      BỘ GIẢI PHỎNG ĐOÁN         │
                                      │      (HEURISTIC SOLVER)         │
                                      │  - Xếp hạng đặc trưng $s_i$     │
                                      │  - Bỏ ép buộc trạng thái nơ-ron │
                                      │  - Tìm nghiệm trên từng pixel   │
                                      └────────────────┬────────────────┘
                                                       │
                                                       ▼
                                      ┌─────────────────────────────────┐
                                      │    Ảnh đối kháng $x'$ ($L_0=1$) │
                                      └─────────────────────────────────┘

Quy trình nghiên cứu chi tiết

1. Phương pháp HA4FNN (Heuristic-based Attack for Feed-forward Neural Network)

• Bước 1: Chuyển dịch mô hình: Mô hình FFNN được chuyển đổi tự động thành chương trình C tương đương. Các hàm kích hoạt ReLU chuyển thành các câu lệnh điều kiện: if (n_i_j < 0) n_i_j = 0;.
• Bước 2: Thực thi vết và thiết lập ràng buộc: Thực thi mã C với ảnh dự đoán đúng $x$ để trích xuất đường thi hành $t_p$. Sinh hệ ràng buộc tầng ẩn: $$c_{hidden} = c_0 \wedge c_1 \wedge \dots \wedge c_{g-1} = \bigwedge_{j} \left( \sum f_j \cdot a_j + z \right)$$ và hệ ràng buộc tầng ra buộc phân loại sai: $$c_{out} = \bigvee_{i \ne y_{true}} \left( n_{y_{true}}^{pre} < n_i^{pre} \right)$$
• Bước 3: Bộ giải phỏng đoán tối ưu: Thay vì nạp toàn bộ vào SMT Solver (Z3), HA4FNN xếp hạng điểm ảnh theo mức độ nhạy cảm gradient, nới lỏng trạng thái kích hoạt của các tầng ẩn, và giải trực tiếp bằng thuật toán phỏng đoán cục bộ.

2. Phương pháp PatternAttack

• Thiết kế mạng ATN khái quát hóa dựa trên Autoencoder: $$\min_{\theta} \sum_{x \in X} \left( L_2(x, x') + \beta \cdot f(x', y^*) \right)$$
• Tích hợp ma trận trọng số mẫu $P \in {0, 1}^d$ trích xuất từ bản đồ nổi bật Saliency Map, giới hạn vùng sinh nhiễu theo biên đối tượng (edges) hoặc vùng nền (background).
• Áp dụng thuật toán tham lam loại bỏ nhiễu dư thừa để giảm khoảng cách $L_0, L_2$.

3. Phương pháp QI4AE (Quality Improvement for Adversarial Examples)

Quy trình hai pha khép kín:

• Pha 1 (Lọc thô): Đưa ảnh đối kháng $x'$ qua mô hình Autoencoder chuyên biệt để tái cấu trúc xấp xỉ, loại bỏ nhanh lượng lớn nhiễu ngoại lai ngẫu nhiên.
• Pha 2 (Tinh chế mịn): Áp dụng thuật toán tham lam quét từng điểm ảnh còn lại, hoàn trả giá trị gốc nếu việc hoàn trả không làm thay đổi nhãn dự đoán sai mục tiêu.

4. Phương pháp SCADefender

Xây dựng mô hình Stacked Convolutional Autoencoder gồm nhiều tầng tích chập và giải tích chập (Deconvolution/ConvTranspose). Tập huấn luyện được chủ động làm giàu bằng cách tổng hợp ảnh đối kháng sinh ra từ nhiều họ tấn công khác nhau (FGSM, BIM, CW, ATN). Hàm mục tiêu tối ưu hóa khoảng cách tái tạo ảnh gốc và giảm thiểu sai số phân loại: $$\mathcal{L}{SCA} = |x{clean} - \text{Dec}(\text{Enc}(x_{adv}))|2^2 + \gamma \cdot \text{CE}(y{true}, M(\text{Dec}(\text{Enc}(x_{adv}))))$$

                         KIẾN TRÚC PHÒNG THỦ TỔNG HỢP CỦA MÔ HÌNH SCADEFENDER
                                                   │
   [Ảnh đầu vào x]                                 │
   (Chưa biết sạch hay đối kháng)                  │
          │                                        │
          ▼                                        ▼
   ┌──────────────┐    ┌──────────────┐    ┌──────────────┐    ┌──────────────┐    ┌─────────────────┐
   │ Tầng Conv 1  │───>│ Tầng Conv 2  │───>│ Không gian ẩn│───>│ Tầng DeConv 1│───>│ Tầng DeConv 2   │
   │ 32 filters   │    │ 64 filters   │    │ Latent Code  │    │ 64 filters   │    │ 32 filters      │
   │ Stride 2     │    │ Stride 2     │    │ $z \in \mathbb{R}^{k}$││ UpSample     │    │ Tái tạo ảnh sạch│
   └──────────────┘    └──────────────┘    └──────────────┘    └──────────────┘    └────────┬────────┘
                                                                                            │
                                                                                            ▼
                                                                                   [Ảnh khôi phục x_out]
                                                                                            │
                                                                                            ▼
                                                                                   ┌─────────────────┐
                                                                                   │ Mô hình CNN gốc │
                                                                                   │ Phân loại chuẩn │
                                                                                   └─────────────────┘

Dữ liệu và Phân tích Thực nghiệm

• Môi trường thực nghiệm: Linux Ubuntu, Python, C compiler (GCC), tích hợp chuẩn SMT-Lib 2.0 và bộ giải Z3 Solver.
• Đặc tả tập dữ liệu và phân bố:
  • MNIST: 60,000 ảnh huấn luyện, 10,000 ảnh kiểm thử (10 nhãn chữ số 0-9).
  • Fashion-MNIST: 60,000 ảnh huấn luyện, 10,000 ảnh kiểm thử (10 nhãn thời trang).
  • CIFAR-10: 60,000 ảnh màu RGB (10 nhãn đối tượng tự nhiên).
  • Handwritten Alphabets: 297,959 ảnh huấn luyện, 74,489 ảnh kiểm thử (26 nhãn chữ cái A-Z).

Các chỉ số đo lường hiệu năng cốt lõi:

• Tỷ lệ thành công (Success Rate - SR): Đo lường tỷ lệ sinh mẫu đối kháng thành công khiến mô hình phân loại sai ($SR_{untargeted}$) hoặc phân loại đúng nhãn đích ($SR_{targeted}$).
• Tỷ lệ giảm nhiễu (Noise Reduction Ratio - NRR): Đo lường tỷ lệ giảm nhiễu đạt được sau khi áp dụng thuật toán tối ưu: $\text{NRR} = \frac{a - b}{a} \in [0, 1)$, trong đó $a$ và $b$ lần lượt là khoảng cách $L_p$ trước và sau cải thiện.
• Tỷ lệ phát hiện và khôi phục (Detection Rate - DR): Tỷ lệ ảnh đối kháng được loại bỏ nhiễu thành công và mô hình phân loại chính xác nhãn ban đầu: $$\text{DR} = \frac{\sum_{x \in X_{def}} \mathbb{I}(M(A(x)) = y_{true})}{|X_{def}|}$$

Phát hiện đột phá và implications

Những phát hiện then chốt

           SO SÁNH TỔNG QUAN HIỆU NĂNG VÀ ĐẶC TÍNH CÁC PHƯƠNG PHÁP ĐỀ XUẤT VỚI BASELINE
┌─────────────────┬──────────────────────┬──────────────────────┬──────────────────────┬──────────────────────┐
│ Tiêu chí        │ DeepCheck vs HA4FNN  │ ATN vs PatternAttack │ Greedy vs QI4AE      │ MagNet vs SCADefender│
├─────────────────┼──────────────────────┼──────────────────────┼──────────────────────┼──────────────────────┤
│ Không gian tìm  │ Bị khóa cứng nhánh   │ Tràn lan toàn bộ     │ Quét tuần tự từng    │ Bó hẹp trong phân    │
│ kiếm / Giả định │ kích hoạt nơ-ron     │ điểm ảnh             │ điểm ảnh             │ phối Gaussian        │
│                 │ (DeepCheck)          │ (ATN)                │ (Greedy đơn lẻ)      │ (MagNet/PuVAE)       │
├─────────────────┼──────────────────────┼──────────────────────┼──────────────────────┼──────────────────────┤
│ Đột phá đề xuất │ Nới lỏng kích hoạt,  │ Định hướng mẫu qua   │ Tích hợp Autoencoder │ Đa dạng hóa tập mẫu  │
│ của Luận án     │ Heuristic Solver     │ Saliency Map         │ lọc thô + Greedy mịn │ huấn luyện phòng thủ │
│                 │ (HA4FNN)             │ (PatternAttack)      │ (QI4AE)              │ (SCADefender)        │
├─────────────────┼──────────────────────┼──────────────────────┼──────────────────────┼──────────────────────┤
│ Kết quả đạt     │ Tăng vọt SR,         │ Kiểm soát vùng chèn, │ Giảm chi phí tính    │ DR vượt trội trên    │
│ được            │ giải thành công $L_0=1$│ tăng độ đa dạng      │ toán, NRR tối ưu     │ toàn bộ tập nhiễu    │
└─────────────────┴──────────────────────┴──────────────────────┴──────────────────────┴──────────────────────┘

1. HA4FNN vượt trội hoàn toàn so với DeepCheck: Trong bài toán tấn công 1 điểm ảnh ($L_0 = 1$), HA4FNN đạt tỷ lệ thành công cao hơn hẳn DeepCheck trên cả 3 bộ dữ liệu MNIST, Fashion-MNIST và Handwritten Alphabets. Đặc biệt, thời gian giải hệ ràng buộc trung bình của HA4FNN giảm hàng chục lần so với việc gọi Z3 Solver trực tiếp, chứng minh việc duy trì trạng thái kích hoạt nơ-ron trong DeepCheck là rào cản tính toán không cần thiết.

2. Khả năng tấn công 1 điểm ảnh thành công trên ảnh thực nghiệm: Thực nghiệm chứng minh tồn tại những điểm ảnh cực kỳ nhạy cảm trên mạng FFNN, nơi chỉ cần thay đổi giá trị đúng 1 pixel duy nhất ($L_0=1$) trong tổng số 784 pixels ($28\times28$) đã đủ làm đảo lộn hoàn toàn xác suất đầu ra của hàm softmax.

3. PatternAttack tạo ra các mẫu đối kháng đa dạng với tỷ lệ giảm nhiễu cao: Trên CIFAR-10 và MNIST, mạng ATN khái quát kết hợp mẫu nổi bật sinh ảnh đối kháng có định hướng đạt tỷ lệ thành công tiệm cận 100%, đồng thời thuật toán tham lam giúp triệt tiêu từ 30% đến trên 60% lượng nhiễu $L_2$ dư thừa mà không làm mất tính chất đối kháng.

4. QI4AE giải quyết bài toán thời gian thực cho tinh chế ảnh đối kháng: Pha lọc thô bằng Autoencoder giúp giảm số lượng điểm ảnh bị nhiễu từ 50-70% ngay lập tức, giúp pha tối ưu tham lam phía sau hội tụ nhanh hơn gấp nhiều lần so với thuật toán tham lam đơn lẻ.

5. SCADefender phá vỡ giới hạn phòng thủ phân phối đơn: Khác với MagNet và PuVAE bị suy giảm tỷ lệ phát hiện khi gặp tấn công CW hoặc FGSM cường độ cao, SCADefender duy trì tỷ lệ phát hiện (DR) và khôi phục nhãn chính xác cao vượt trội trên cả 3 bộ dữ liệu MNIST, Fashion-MNIST và CIFAR-10 nhờ kiến trúc tích chập xếp chồng học trên dữ liệu đa dạng nhiễu.

Implications đa chiều

Đóng góp học thuật

Luận án thiết lập một chuẩn phương pháp luận mới cho kiểm thử phần mềm học sâu (Deep Learning Software Testing). Kết quả nghiên cứu chứng minh các kỹ thuật phân tích chương trình truyền thống (Symbolic Execution, Abstract Syntax Tree, Program Instrumentation) hoàn toàn có thể dung hợp với các mô hình xác suất và tối ưu hóa nơ-ron.

Đóng góp thực tiễn và công nghiệp

Các công cụ phát triển từ luận án cung cấp bộ khung kiểm thử hộp trắng hoàn chỉnh cho các kỹ sư phát triển phần mềm AI. Bộ giải pháp giúp phát hiện sớm các lỗ hổng an ninh trong các hệ thống nhận diện biển báo xe tự lái, xác thực sinh trắc học khuôn mặt và xử lý ảnh y tế trước khi triển khai thực tế.

Triển khai ứng dụng

Bộ công cụ đã được chuyển giao và thử nghiệm thực tế tại Công ty TSDV, phục vụ công tác thẩm định chất lượng và độ an toàn của các module học sâu thương mại.

Limitations và Future Research

Hạn chế nghiên cứu

1. Giới hạn kích thước dữ liệu đầu vào: Các thực nghiệm chủ yếu tập trung vào không gian ảnh kích thước vừa và nhỏ ($28\times28\times1$ và $28\times28\times3$). Chưa đánh giá trên các bộ dữ liệu độ phân giải siêu cao (như ImageNet $224\times224\times3$ hoặc $1024\times1024$).
2. Ranh giới kiến trúc mô hình: Phương pháp HA4FNN hiện tại chỉ tối ưu hóa cho mạng nơ-ron truyền thẳng (FFNN) do độ phức tạp trong việc chuyển dịch mã nguồn C và dựng cây AST cho các phép toán tích chập nhiều kênh.
3. Môi trường kiểm thử hộp trắng: Toàn bộ các đề xuất đòi hỏi quyền truy cập đầy đủ vào cấu trúc mạng và trọng số mô hình (white-box assumption), chưa bao quát toàn diện kịch bản tấn công hộp đen (black-box query-based).

Chương trình nghiên cứu tương lai

• Hướng 1: Mở rộng phương pháp HA4FNN cho mạng tích chập sâu (ResNet, DenseNet, Vision Transformer) bằng cách tối ưu hóa bộ dịch mã trung gian và rút gọn đồ thị tính toán.
• Hướng 2: Nghiên cứu cơ chế tấn công và phòng thủ thích ứng cho mô hình đa phương thức (Multimodal Large Language Models - MLLMs) kết hợp giữa hình ảnh và văn bản.
• Hướng 3: Tự động hóa sinh ca kiểm thử đối kháng trong môi trường vật lý (Physical-world Adversarial Attacks) như in 3D, dán nhãn quang học ngoài đời thực.
• Hướng 4: Tích hợp kiểm thử tính chắc chắn vào quy trình CI/CD tự động (Continuous Integration/Continuous Deployment) cho các dự án kỹ thuật phần mềm AI (MLOps/AIOps).

Tác động và ảnh hưởng

                               CÁC TRỤ CỘT TÁC ĐỘNG VÀ ĐỐI TƯỢNG HƯỞNG LỢI
┌────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                          TÁC ĐỘNG HỌC THUẬT & CÔNG NGHIỆP                              │
├────────────────────────────────────┬───────────────────────────────────┬───────────────────────────────┤
│ Viện nghiên cứu & Trường Đại học   │ Doanh nghiệp công nghệ & R&D      │ Tổ chức chuẩn hóa & Xã hội    │
│ - Mở ra nhánh kiểm thử SE cho AI   │ - Công cụ kiểm thử bảo mật DNN    │ - Bộ tiêu chí đánh giá an toàn│
│ - Tích hợp Symbolic + Heuristic    │ - Giảm thiểu rủi ro bị tấn công   │ - Tăng cường độ tin cậy AI    │
└────────────────────────────────────┴───────────────────────────────────┴───────────────────────────────┘

Nghiên cứu đóng góp trực tiếp vào mục tiêu xây dựng Trí tuệ Nhân tạo Đáng tin cậy (Trustworthy AI). Về mặt học thuật, công trình mở ra hướng kết hợp giữa các phương pháp hình thức của kỹ thuật phần mềm với học sâu. Về mặt công nghệ, nghiên cứu hỗ trợ các ngành công nghiệp nhạy cảm về an toàn (như xe tự lái, y tế số, tài chính ngân hàng) thiết lập quy trình kiểm thử tự động, phát hiện lỗ hổng trước các cuộc tấn công có chủ đích từ tin tặc.

Đối tượng hưởng lợi

• Nghiên cứu sinh và Giới học thuật: Tiếp cận phương pháp luận dung hợp giữa Symbolic Execution và Heuristic Optimization; kế thừa các mã nguồn và cấu trúc kiểm thử cho FFNN và CNN.
• Kỹ sư Kỹ thuật Phần mềm và MLOps: Ứng dụng trực tiếp quy trình kiểm thử tính chắc chắn vào vòng đời phát triển phần mềm chứa thành phần AI (SE4AI).
• Các trung tâm R&D xe tự lái và Thị giác máy tính: Sử dụng SCADefender để bọc lót (wrapper defense) cho các mạng phân loại ảnh hiện hữu mà không cần huấn luyện lại từ đầu toàn bộ mô hình gốc.

Câu hỏi chuyên sâu

1. Đóng góp lý thuyết độc đáo nhất của luận án là gì và nó mở rộng lý thuyết nào?

Đóng góp lý thuyết độc đáo nhất là việc tái định nghĩa không gian tìm kiếm mẫu đối kháng trong kỹ thuật thực thi tượng trưng (Symbolic Execution). Luận án đã bác bỏ giả định truyền thống của DeepCheck (Gopinath et al.) vốn bắt buộc mẫu đối kháng phải bảo toàn vết kích hoạt nơ-ron ($c_{hidden}$). Bằng cách nới lỏng không gian trạng thái ẩn và kết hợp hàm mục tiêu đầu ra $c_{out}$ với bộ giải phỏng đoán, nghiên cứu đã mở rộng lý thuyết phân tích chương trình hình thức sang miền xấp xỉ liên tục của mạng nơ-ron.

2. Điểm cách tân về phương pháp luận so với các nghiên cứu quốc tế tiền nhiệm?

So với DeepCheck (sử dụng Z3 SMT Solver) và ATN (sử dụng tối ưu hóa $L_2$ thuần túy), luận án đưa ra hai cách tân phương pháp luận mang tính đột phá:

• Chuyển đổi từ SMT Solver sang Heuristic Solver (HA4FNN): Khắc phục hoàn toàn hiện tượng bùng nổ tổ hợp thời gian giải khi số tầng ẩn tăng.
• Thiết kế cơ chế lai hai pha (Two-phase Hybrid Framework trong QI4AE): Kết hợp năng lực tái tạo chiều sâu của Autoencoder với tốc độ tối ưu cục bộ của thuật toán tham lam, đạt tỷ lệ giảm nhiễu vượt trội trong thời gian thực.

3. Phát hiện bất ngờ nhất trong quá trình thực nghiệm là gì?

Phát hiện thực nghiệm chấn động nhất là sự tồn tại của các điểm ảnh "tử huyệt" đơn lẻ trên các bộ dữ liệu chuẩn (MNIST, Fashion-MNIST, Alphabet). Chỉ bằng việc can thiệp giá trị của đúng 1 pixel duy nhất ($L_0 = 1$) thông qua HA4FNN, mô hình mạng nơ-ron truyền thẳng bị đánh lừa hoàn toàn với xác suất tự tin cao, làm bộc lộ tính mong manh nghiêm trọng của các hàm kích hoạt phi tuyến tính khi chưa được kiểm thử toàn diện.

4. Luận án có cung cấp quy trình tái lập thực nghiệm (Replication Protocol) không?

Có. Luận án đặc tả chi tiết toàn bộ siêu tham số (learning rate $\eta$, batch size, số epoch, hàm mất mát $\mathcal{L}$, hệ số cân bằng $\beta, \gamma$), cấu trúc phân tầng chi tiết của các mạng kiểm thử và mạng phòng thủ (kích thước kernel, stride, số filter), định dạng ràng buộc chuẩn SMT-Lib 2.0 và đường dẫn tập dữ liệu công khai. Các công cụ đã được đóng gói và kiểm chứng thực tế tại môi trường công nghiệp (TSDV).

5. Chương trình nghiên cứu 10 năm tiếp theo được định hình như thế nào?

Lộ trình 10 năm hướng tới việc xây dựng một hệ điều hành kiểm thử tự động toàn diện cho AI (Universal AI Testing Framework), chuyển dịch trọng tâm từ mô hình phân loại ảnh 2D tĩnh sang các hệ thống AI tạo sinh (Generative AI), mô hình ngôn ngữ lớn đa phương thức (Multimodal LLMs), và xác thực an toàn phần mềm điều khiển trong các hệ thống vật lý - không gian mạng (Cyber-Physical Systems).

Kết luận

Luận án "Các phương pháp đảm bảo tính chắc chắn cho một số mô hình học sâu" của tác giả Nguyễn Đức Anh đã giải quyết trọn vẹn và thấu đáo bài toán cốt lõi về kiểm thử và nâng cao độ tin cậy của mô hình học sâu.

Sáu đóng góp cụ thể mang tính đột phá của công trình:

1. Đề xuất phương pháp HA4FNN sử dụng bộ giải phỏng đoán và thực thi tượng trưng nới lỏng, nâng cao vượt bậc tỷ lệ thành công và tốc độ sinh mẫu đối kháng 1 điểm ảnh trên mạng nơ-ron truyền thẳng.
2. Đề xuất phương pháp PatternAttack tích hợp mạng ATN khái quát và bản đồ nổi bật, cho phép sinh mẫu đối kháng có định hướng theo các mẫu phân bố không gian linh hoạt.
3. Đề xuất thuật toán tham lam tối ưu hóa chuẩn khoảng cách $L_0, L_2$, triệt tiêu hiệu quả lượng nhiễu dư thừa trong mẫu đối kháng.
4. Đề xuất phương pháp lai hai pha QI4AE, kết hợp mô hình mã hóa tự động và tìm kiếm tham lam, giải quyết bài toán nâng cao chất lượng ảnh đối kháng ở mức thời gian thực.
5. Đề xuất giải pháp phòng thủ SCADefender dựa trên Stacked Convolutional Autoencoder huấn luyện trên tập mẫu đa phân phối, loại bỏ hiệu quả các dạng nhiễu đối kháng bất định.
6. Đóng gói và phát triển thành công hệ thống công cụ kiểm thử phần mềm học sâu, chuyển giao ứng dụng thành công trong môi trường doanh nghiệp thực tế.

Công trình khẳng định bước tiến vững chắc trong việc kết hợp Kỹ thuật Phần mềm với Trí tuệ Nhân tạo, đặt nền móng phương pháp luận quan trọng cho các thế hệ hệ thống AI an toàn và đáng tin cậy trong tương lai.