LiRPA XOR Demo (Python/MATLAB)

이 저장소는 완전연결 신경망(은닉층 ReLU, 출력층 Sigmoid)에 대해 LiRPA(CROWN 계열) forward/backward bound를 계산하는 교육용 예제를 제공합니다.

핵심 관찰 (XOR 게이트)

XOR 네 코너 입력 [0,0], [0,1], [1,0], [1,1]에 대해 다음이 관찰됩니다.

• 교란 반경 epsilon이 0 ~ 0.22이면 4가지 입력 모두 certified 됩니다.
• epsilon = 0.23이면 4가지 중 2가지 입력은 certified되지 않습니다.

즉, epsilon을 조금만 키워도 인증 가능 여부가 바뀌는 경계가 존재하므로, 값을 바꿔가며 결과를 확인해보는 것이 중요합니다.

Python 실행 가이드

1) 기본 실행

아래 파일이 데모 진입점입니다.

• lirpa_forward_backward_fc.py

기본값(eps=0.02)으로 바로 실행:

python lirpa_forward_backward_fc.py

2) epsilon을 바꿔 실행하기

run_xor_demo(eps=...)를 직접 호출하면 원하는 epsilon으로 실험할 수 있습니다.

python -c "import lirpa_forward_backward_fc as d; d._self_test_relaxations(); d.run_xor_demo(eps=0.22)"
python -c "import lirpa_forward_backward_fc as d; d._self_test_relaxations(); d.run_xor_demo(eps=0.23)"

권장 실험:

• eps=0.00, 0.10, 0.22, 0.23 순서로 실행
• 각 입력점별 certified=True/False를 비교
• forward/backward 결과가 어떻게 달라지는지 함께 확인

MATLAB 실행 가이드

MATLAB 버전은 아래 파일에 있습니다.

• lirpa_forward_backward_fc.m

MATLAB 콘솔에서 실행:

lirpa_forward_backward_fc_matlab

MATLAB 코드 내부의 run_xor_demo(...) 인자를 바꿔 epsilon 실험을 반복하면 동일한 경향을 확인할 수 있습니다.

C++ 실행 가이드

C++ 버전은 아래 파일에 있습니다.

• lirpa_forward_backward_fc.cpp (std::vector 기반 구현)
• lirpa_forward_backward_fc_array.cpp (배열 기반 구현)

1) 빌드

Windows PowerShell + g++(MinGW 등) 기준:

g++ -std=c++17 -O2 lirpa_forward_backward_fc.cpp -o lirpa_forward_backward_fc.exe
g++ -std=c++17 -O2 lirpa_forward_backward_fc_array.cpp -o lirpa_forward_backward_fc_array.exe

2) 기본 실행 (eps=0.02)

./lirpa_forward_backward_fc.exe
./lirpa_forward_backward_fc_array.exe

3) epsilon을 바꿔 실행하기

실행 인자로 epsilon 값을 넣으면 됩니다.

./lirpa_forward_backward_fc.exe 0.22
./lirpa_forward_backward_fc.exe 0.23
./lirpa_forward_backward_fc_array.exe 0.22
./lirpa_forward_backward_fc_array.exe 0.23

권장 실험:

• 0.00, 0.10, 0.22, 0.23 순서로 실행
• 각 입력점별 certified=True/False를 비교
• forward/backward 결과가 어떻게 달라지는지 함께 확인

출력 해석 팁

각 입력점마다 다음 정보가 출력됩니다.

• 네트워크 점 예측값 (network_output)
• forward bound와 backward bound의 하한/상한
• XOR 정답 클래스 기준으로 인증 여부 (certified=True/False)

XOR 정답이 1인 점은 보통 lower bound > 0.5, 정답이 0인 점은 upper bound < 0.5 조건으로 인증 여부를 판단합니다.

sparse.py — mMIMO Top-K 안테나 선택 강건성 검증

개요

sparse.py는 mMIMO top-k 안테나 선택 네트워크에 대한 CROWN(backward LiRPA) 연산을 희소행렬을 적용한 버전입니다.

• 네트워크: 256차원 입력(16×16 H^T H 행렬을 flatten) → 16차원 출력(안테나별 스코어)
• "정답": 데이터셋 라벨이 아니라, 섭동 없는 원본 입력 x0에 대해 네트워크 자신이 고른 top-k 결과
• 목표: L∞ eps 반경 안의 모든 섭동에 대해 top-k 선택 결과가 절대 바뀌지 않음을 증명

내부적으로 네트워크 가중치를 SciPy sparse(CSR) 행렬로 변환해서, 0인 가중치를 연산에서 제외하여 dense 행렬 대비 속도를 높입니다.

요구 사항

• Python 3.10+ (환경: conda env crown)
• numpy
• scipy

conda activate crown
pip install numpy scipy

필요한 파일

1. 네트워크 파일 (.bin, Custom 바이너리 포맷)

   • CustomToLirpa.py의 load_custom_network()가 읽는 포맷
   • 은닉층은 ReLU, 출력층은 linear(logit 그대로)로 고정되어 있음
   • 기본값: Custom/Baseline mMIMO FC H hard short 80 HTHNN_LAY2_491 RELU 20241018 PRUNED 0.93_NO_SIGMOID_custom.bin

2. 입력 데이터 파일 (.pickle)

   • data_split.py의 load_test_rows()로 읽음 (파일 전체를 메모리에 올리지 않고 memmap으로 test 구간만 읽음)
   • 파일 하나당 20000개 샘플이 들어있다고 가정 (no_dataInFile=20000)
   • 기본값: C:\AI_Verification\wireless\Pickle/mMIMO_AS_training_data_20000_80_H_HTH_ORG_1D-003.pickle

실행 방법

python sparse.py [network_path] [data_path] [no_test_files] [n_points] [method] [output_csv]

모든 인자는 위치 인자이며, 생략하면 아래 기본값이 사용됩니다.

순서	인자	기본값	설명
1	network_path	위 Custom .bin 경로	검증할 네트워크
2	data_path	위 .pickle 경로	입력 데이터셋
3	no_test_files	2	pickle 뒤쪽에서 test로 사용할 파일 개수 (파일당 20000개 샘플)
4	n_points	전체 사용	test 데이터 중 앞에서부터 몇 개 점만 검증할지 (생략 시 전체)
5	method	backward	bound 계산 방식: backward | backward_only | forward (아래 설명)
6	output_csv	results_{method}.csv	결과를 저장할 CSV 경로

가장 간단한 실행 (모든 기본값 사용, backward 방식):

python sparse.py

bound 계산 방식 3가지

sparse.py는 method 인자로 세 가지 bound 계산 방식을 선택할 수 있습니다. (lirpa_forward_backward_fc_sparse.py의 LiRPAForward / LiRPABackward / LiRPABackwardOnly 클래스가 각각 대응)

세 방식 모두 dense/sparse 행렬을 섞어 써도 안전하도록(scale_rows/scale_cols 헬퍼로 행렬 형태에 관계없이 올바르게 원소별 스케일링) 처리되어 있습니다.

1. backward (기본값, forward + backward 표준 CROWN)

• 각 레이어의 중간(pre-activation) bound를 forward mode로 먼저 구하고, 그 relaxation(기울기/절편)을 이용해 최종 출력 bound를 backward substitution으로 구하는 표준 CROWN 방식입니다.
• 정확도와 속도의 균형이 좋아 가장 일반적으로 쓰는 방식입니다.

python sparse.py "" "" 2 40000 backward results_backward.csv

2. backward_only (중간 bound도 backward만 사용)

• 중간(pre-activation) bound까지 전부 backward substitution만으로 구합니다 (forward mode를 전혀 쓰지 않음).
• 레이어가 깊을수록 매 레이어마다 입력까지 역전파를 다시 하기 때문에 계산량이 늘어날 수 있지만, forward 단계 없이 순수 backward 경로만 검증하고 싶을 때 사용합니다.

python sparse.py "" "" 2 40000 backward_only results_backward_only.csv

3. forward (순수 forward mode)

• 입력부터 출력까지 symbolic affine bound를 앞으로 전파만 해서 구하는 방식입니다.
• backward substitution이 없어 레이어당 계산이 단순하지만, 일반적으로 backward 방식보다 bound가 느슨(loose)합니다.

python sparse.py "" "" 2 40000 forward results_forward.csv

참고: ""(빈 문자열)을 넘기면 sparse.py가 길이 검사(len(sys.argv[1]) > 1)를 통해 기본값을 사용하도록 되어 있습니다. 즉 네트워크/데이터 경로를 기본값 그대로 쓰고 뒤쪽 인자(no_test_files, n_points, method, output_csv)만 바꾸고 싶을 때 위처럼 ""를 채워 넣으면 됩니다.

출력 결과

콘솔 출력

각 eps 값에 대해 아래 세 값을 sweep합니다.

eps_list = [1e-6, 1e-5, 1e-4 ~ 9e-4, 1e-3 ~ 9e-3, 1e-2, 1e-1, 1.0]

• T: 해당 eps에서 top-k 선택이 **강건함(certified=True)**이 증명된 점의 개수
• F: 증명에 실패한 점의 개수
• ratio: T / (T + F)

eps=     1e-06: T= 498 F=   2 ratio=0.996
eps=     1e-05: T= 495 F=   5 ratio=0.990
...
total elapsed: 12.34s

CSV 출력

output_csv에 method, eps, T, F, ratio 열로 동일한 내용이 저장됩니다.