서울시립대학교 인공지능학과 고상기 교수님의 신뢰할 수 있는 인공지능 수업을 정리임을 미리 알립니다.
신경망을 논리적인 언어로 표현한 다음, 그 표현을 바탕으로 여러 '정확성 속성' 관점에서 분석할 것이다.
1. A specification language: 시스템의 동작을 공식적으로 기술하는 언어인 명세 언어 파트 1-1) Hoare logic: 코드 실행 전후 상태를 기술하는 논리 1-2) Hoare logic in neural networks: 위 논리를 신경망에 적용
2. Correctness properties of neural networks: 신경망 잘 작동하나 검증하고 싶은 속성들 # 강건한가.. 이런거 2 -1) Hoare 논리로 표현한 신경망을 바탕으로 정확성을 판단할 수 있는 여러 속성들: Robustness, equivalence of neural networks, collision-avoidance, physics modeling, natural-language processing, and monotonicity 중간고사:인공신경망 검증 조건을 Hoare logic으로 기술
3. Advanced topics -> Correctness properties of RNN, fairness, and other semantic perturbations 중간고사: Group fairness vs. Individual Fairness
1. A Specification Language
Hoare logic ((1-1))
우리의 목표는 신경망이 정확하게 작동하는지 판단하는 것이다. 그렇기에 우리는 신경망의 동작을 '논리적 언어를 통해 표현'하고 이를 분석할 것이다. 이를 위해 이 논리적인 언어 Hoare logic를 먼저 배울 것이다.
1) Hoare logic # Hoare Triple 개념
Hoare ligic은 C++, Java와 같은 코드들을 논리적으로 추론하기 위한 Formal framework이다. 이러한 논리 언어를 사용하여 코드를 표현하면 프로그램이 의도한 대로 동작하는지를 수학적으로 증명할 수 있게 된다.
Hoare logic의 가장 중요한 특징인 Hoare Triple에 대해 공부해보면 쉽게 이해할 수 있다.
Hoare Triple: 코드 실행이 계산 상태를 어떻게 변화 시키는지 기술하는 세 가지 요소 {P} C {Q} 1) {P}: 코드 실행 전 조건 Precondition이다. 즉 코드 실행 전에 만족해야할 조건이다. 2) C: 실제로 실행되는 코드 명령이다 3) {Q}: 코드가 실행된 이후 사후 조건 Postcondition이다. 코드 실행 후 반드시 성립해야 할 조건이다.
예를 들어서x가 3보다 작으면{P}곱하기 x2를 해주는 코드가 실행{C}됐을 때의 결과는 2x여야해!!{Q} 이런 느낌인 것이다.
만약 전조건 P가 참이고, 코드 C가 제대로 실행되었다면 Q도 반드시 참이다.
해당 구조가 거짓임이 보이려면 전조건P은 참인데 Q가 참이 아닌 반례를 보이면 된다.그냥 일반적인 P -> Q 논리식 같은 느낌이다. 전제가 참인데 결론이 거짓인 논리식은 거짓이다. 예시들을 보며 감을 잡아보자.
2) Hoare logic 문제 풀이
example1
전조건이 참일 때, 숫자 하나가 더해지는 코드이다. 해당 Hoare 논리식이 틀렸다를 보여주기 위해서는 반례를 찾으면 된다. 만약 x가 0이라고 해보자. 전제는 참이고, 코드가 돌아갔을 때 x = 1이 될 것인데 이는 후 조건과 맞지 않는다. 즉 반례를 찾았으므로 해당 논리식은 거짓이다.
example2
해당 논리식이 참이 되는 전조건을 찾을 수도 있다. 사실 후조건과 코드를 통해 전조건을 예측하는 게 더 일반적이며 이 때 우리는 검증을 위해 더 많은 경우를 포함하는 약한 전조건을 찾는다.
example2 논리식이 참이 되는 전조건. b>0이 검증을 위해 더 좋을 것이다
example3
반례를 찾으면 쉽게 참 거짓을 알 수 있다. 문제에 대한 답은 T, F, T, F 이다.
Hoare logic in neural networks # Hoare Triple 적용 ((1-2))
1) Hoare logic in neural networks
위에서 코드가 의도대로 작동하는지 검증하는 Hoare logic 추론 방법에 대해 알아보았다. 이제 우리는 이걸 신경망에 대입해볼 것이다.
신경망: n차원 벡터를 받아서 m차원 결과 출력
신경망f(x)은 특정 조건의 입력{P}을 받았을 때 특정한 출력{Q}이 나와야한다. 이를 수학적으로 표현하면 {P} f(x) {Q}가 될 것이다.
ex) 강아지 사진이 들어오면 신경망이 강아지라고 출력한다.
이러한 신경망은 이미지의 약간의 변화가 있을때 등 다양한 상황에서 일관된 예측을 해야한다. 다음과 같은 전, 후 조건 그리고 신경망 예시들을 보자.
예시1 신경망의 전 조건, 후. 조건 수학적 표기는 아니다.예시 2예시 3
그냥 가볍게 읽으면 된다. 어두울 때 판다임을 예측해야하고, 영어 문장이 조금씩 달라져도 의미가 같으면 같은 감정으로 잘 판단해야하고, 같은 기능의 코드가 구성이 조금 달라도 맞는지 틀린지 잘 예측해야한다. 즉 뒤에서 배울 검증 속성 중 Robustness이다. 이 모델, 이런 상황((Correctness-properties))에서도 제대로 동작하냐? 이런 느낌이다. 뒤에서 더 자세히 다룰 것이다.
예시 4
참고로 상황이 바뀌면 유연하게 움직일 수 있는 non-robustness도 검증할 수 있다.
해당 예시에서 중요한건 이 전조건, 후조건을 어떻게 수학적으로 표현할 것인가? 이다. 이렇게 말로 장황하게 써놓는건 누구나 할 수 있다. 이걸 수학적으로 표기해보고 검증에 사용해보자.
2) Hoare triple in neural networks # 수학적으로 표기하기
Hoare Tripple를 사용하여 전, 후 조건을 수학적으로 작성하면 된다. 다음과 같은 형태가 될 것이다.
1) {P}: 신경망에 주어질 입력에 대한 가정 혹은 조건이다. 입력 값의 제한 및 조건을 다루게 되며 T/F 값을 갖는다. ex) 밝기가 0.1 이내로 바뀐 이미지, 단어가 2개만 바뀐 문장 등
2) r <- f(x): 신경망 함수의 호출을 의미한다. 이러한 호출 결과는 변수 r에 저장된다. 여러 차례 호출할 수도 있다.3) {Q}: P에서 등장하는 입력 변수 xi와, 계산된 출력 변수 ri들에 대한 논리 조건이다. T/F 값을 가진다. *** ex) 판다 사진의 밝기가 0.1 이내로 바뀌었으면{P}, 신경망의 결과의 변화는 없이 판다여야해!! # Robustness 검증 -> 이러한 {Q}가 거짓이라면 해당 속성은 유효하지 않다고 판단한다.
예시를 좀 봐보자. Q를 좀 더 쉽게 이해할 수 있을 것이다. '입력 변수와 출력 변수에 대한 논리 조건' 임을 인지하라.
{P}: 입력 x와 c는 0.1이내 거리에 존재한다.
{Q}: 그렇다면 x와 c의 클래스 예측은 같아야한다!
당연하겠지만 ri는 각 클래스에 대한 확률을 담은 벡터일 것이다. 이를 class() 함수에 넣으면 최대값을 갖는 클래스를 뽑아낸다.
3) Counter examples
위 문제는 모델의 Robustness 속성을 검증하는 과정이었다. 만약 해당 속성이 유효하지 않음을 보이려면 즉 모델이 의도대로 작동하지 않았음을 보이려면 여기서도 똑같이 '전제가 참일 때' 결론 {Q}가 거짓인 반례를 보이면 된다.
바로 위에서 본 예시에서는 거리가 0.1 이하로 차이나는 두 입력 값이 다른 클래스로 분류되었을 때 이 Robustness가 깨진 것이다.
2. Correctness properties of neural networks # 어떤 속성을 검증할 것인가?
우리는 Hoare triple을 통해 신경망이 주어진 입력에 대해 올바르게 작동하는지 검증할 수 있는 기본적인 표현 방식과 표기 방법을 익혔다.
자 근데 여기서 중요한건 그 P와 Q를 어떻게 정하느냐?이다. 즉 어떤 상황에서 모델이 의도대로 잘 작동하고 있는지 어떻게 정의할 것이냐?이다. 이 질문에 대한 대답이 바로 Correctness Properties 정확성 속성이다.
쉽게 말하면 이제 어떤 관점에서 해당 모델을 검증할 것인지를 고민한다. 이 검증의 관점이 바로 Correctness Properties이다.
ex) 난 신경망이 강건하게 작동하는 걸 보고 싶어, 난 신경망이 유연하게 대처하는 지 보고싶어 등... 다양한 관점이 있다.
1) Robustness
-> 모델이 입력 데이터나 환경에 변화, 불확실성, 불완전성이 있을 때도 성능을 유지하고 신뢰할 수 있는 출력을 제공하는 능력
데이터는 주로 노이즈가 있거나 불완전할 수 있고, 공격을 받을 수 있으므로 신경망에서 매우 중요한 정확성 속성이다.
Robustness를 알기 위해 먼저 자주 사용하게 될 Norm에 대해 알아보고, 이후 두 종류의 Robustness를 알아볼 것이다.
Norm 기반의 perturbation
신경망이 입력 데이터의 작은 변화에 대해 견고한지 여부를 검증할 때, 얼마나 바뀌는지 알아볼 때 사용되는 l-norm 기반의 perturbation을 먼저 봐보자. 뭐 근데 사실 다 아는 내용일 것이다.
1. L2-norm2. Linfi-norm
Global Robustness
신경망의 예측이 모든 입력과, 그 주위의 모든 perturbation에 대해 일관되게 유지된다면 해당 신경망은 Global Robustness를 가진다고 한다.
여기서 중요한건 '모든 입력'에 대해서라는 것이다. 예를 들어 이 Task가 운전이라면 모든 나라, 모든 도로, 모든 날씨에서도 Perturbatin이 입실론보다 작으면 신경망이 같은 행동을 취해야하는 것이다. 현실적으로 성립하기 어려운 조건이라 아래 더 약한 조건 Local robustness가 정의되었다.
Local robustness
특정 입력 x₀에 대해, 그 주변에서의 작은 perturbation이 있어도 출력이 바뀌지 않는다면 Local robustness를 가진다고 한다.
2) Equivalence of neural networks # 신경망을 다른 신경망으로 바꿔도 문제 없는가?
만약 계속 써오던 신경망 f와 요즘 새로 나온 SOTA g가 있다고 하자. f와 g의 예측 결과가 같을까? 그렇다면 g로 안전하게 대체할 수 있다.
이 또한 모든 입력 값에 r1 클래스와 r2 클래스가 같아야 한다는 대한 강한 조건이 있으며 이는 달성하기 어려우니 대안으로 비 슷한 입력에 대해 예측이 일치하면 동등하다고 보는 완화된 조건이 존재한다.
x1 근처의 x2, x3을 뽑고 얘네의 클래스를 예측했을 때 두 모델이 같은 클래스로 예측하면 교체가 가능하다고 보는 것이다.
3) Collision-avoidance
요즘 충돌 회피와 같은 시스템들은 기존의 규칙 기반의 시스템에서 벗어나 더 작고 효율적인 프로그램을 위해 학습 기반 방법론으로 변화하고 있다. 이러한 신경망이 특정 상황에서 올바른 판단을 내리는지 논리적으로 검증할 수 있다.
이러한 상황에서는 위험도 스코어가 낮아서 뭐 별다른 충돌 회피를 안해도 된다 이런 식이다.
4) Physics modeling
신경망이 물리 법칙을 잘 따르는지 검증할 수도 있다.
에너지 보전 법칙을 잘 따르는지... 2019 논문이래...
5) Natural language processing # 동의어
길이가 n인 고정된 문장 c가 있다. 이 중 'i 번째 인덱스의 단어 하나'를 동의어 사전 T에 넣어 다른 단어 w로 바꾸었을 때의 문장을 x라고 하자. 이 두 문장은 한 단어가 다르긴 하지만 동의어이기에 같은 뜻의 문장으로 인식되어야한다.
두 개의 단어를 바꿀 수 있다.
6) Monotonicity # 단조성
더 큰 입력이 들어올수록 더 큰 출력이 유도되어야 하는 단조성은 신경망이 가지길 바라는 표준적인 수학적 속성이다.
ex) 집 값 예측: 면적이 넓을 수록 예측 가격이 올라야 이상하지 않음.
3. Advanced Topics
Correctness properties of RNN ((3-1))
RNN은 길이가 T인 입력 시퀀스를 받아 C개의 클래스 중 하나로 분류한다. 입력 시퀀스 요소 중 하나 혹은 t개의 요소 Adversarial Attack 예시는 다음과 같다.
Fairness ((3-2)) ***
1) Fairness 개념
Fairness란 사람을 공정하고 평등하게 대우하여 임의적인 기준으로 인해 차별이나 부당한 유불리를 받지 않도록 하는 개념이다.
ex) 인종, 성별
2) Individual fairness 개념
Individual Fairness는 알고리즘, 머신러닝, 결정 시스템에서 사용되는 구체적인 공정성 정의.
유사한 두 사람은 보호 속성 예: 인종, 성별, 나이에 상관없이 시스템에 의해 같은 결과를 받아야 한다.
n개의 데이터 인스턴스가 있고, 각 인스턴스는 x는 t개의 속성을 갖는다고 해보자.
이러한 속성들의 집합은 A로 나타내며 Ai는 Ii를 도메인으로 갖는다
ex) A₁ = 나이 → I₁ = [0, 100]여여기이
이러한 속성들의 집합 A 중에서 보호되어야 하는 집합은 P로 나타나며, A는 P의 부분집합이다.
ex) A = 인종, 나이, 성별, 집안, 학벌 등등등.... P = 인종, 성별
이제 Individual Fairness는 다음과 같이 정의할 수 있다. 모델 f가 개인 공정성을 만족하려면, 다음 쌍 x, x'이 없어야한다.
->보호 속성을 제외한 모든 값이 같으며, 보호 속성 중 적어도 하나가 다른데, 예측 결과가 다른 쌍이 존재하면... 페어하지 않다.
-> 직관적으로 보호 속성을 제외한 모든 속성 값이 같으면 같은 예측을 받아야한다. 이게 Individual Fairness이다.
-> 즉 이러한 페어 x, x'이 존재하지 않아야 Individual Fairness하다!!!! 헷갈리면 안된다.
이를 Hoare로 표현하면 다음과 같다. 모든 속성값이 도메인 기반 지식 내에 있어야하는게 신기하다. ㅇㅇ.. 안드로메다진 뭐 이런건 걍 무시해도 되니까.
위와 같은 x, x' 쌍이 존재한다면 개인 공정성이 위반되었다고 본다. 없어야 공정한거다.
3) ϵ-fairness and targeted fairness
P는 성역이다 건들지 않는다 ㅇㅇ.. 예를 들어 학벌이 P에 안들어갔을때 건국대랑 동국대 사이가 조금 차이가 있긴 하지만 거의 비슷하니까 이정도는 같게 대우하자 이건거다.
4) Targeted fairness
원하는 입력 변수의 범위에서 보자는 것이다. 이 target T에 속하는 입력들에 대해서는 반드시 개인 공정성이 유지되어야 한다
5) Group fairness vs. Individual Fairness **** 뭐 이런게 있다..
Group fairness모델이 서로 다른 인구 집단을 공평하게 대우하도록 보장하는 것 반면 Individual Fairness는 비슷한 조건을 가진 개인이 비슷한 대우를 받도록 보장하는 것에 초점을 맞춘다. 이러한 두 개념의 균형은 머신 러닝에서 편향과 공정성 문제를 해결하는데 중요하다.
ex) 그룹: 성별 간 일자리 제안 비율 균형 그룹 vs 개인: 동등한 자격을 가진 후보자면 배경 상관없이 기회를 받도록 보장
Demographic Parity는 AI 모델이 서로 다른 인구 집단들에 대해 유사한 긍정적 예측 비율 유지하도록 요구한다. 이 기준은 알고리즘 공정성을 증진시킬 수 있지만, 예기치 않은 결과를 초래할 수도 있다. 예를 들어, 통계적 균형을 유지하기 위해 덜 자격을 갖춘 사람을 우대하게 되는 경우가 발생할 수 있다. 그래서 많은 조직들은 정확성을 해치지 않으면서도 공정성을 보장할 수 있는 Equality of Opportunity 또는 Equalized Odds 같은 성능 기반 공정성 지표를 채택한다.
교차 공정성은 모델이 여러 소수자 집단에 동시에 속한 개인을 고려하도록 보장하는 개념이다. 이는 기존의 공정성 지표들이 놓칠 수 있는 더 복합적인 형태의 편향을 다룰 수 있게 해준다. 예: “장애가 있는 아프리카계 미국 여성”에 대한 차별은 단일한 인종, 성별, 장애라는 기준만으로는 포착되지 않을 수 있다. 이러한 이유로, 조직은 **민감한 속성들을 개별적으로가 아니라, 겹치는 형태로 분석해야 AI에서 발생하는 편향과 공정성 문제를 더 효과적으로 해결할 수 있다.
Fairness through unawareness은 AI 모델에서 인종, 성별 같은 인구통계적 속성을 단순히 무시하면 공정성이 보장된다고 가정하는 접근이다. 하지만 실제로는, 모델이 여전히 이런 속성과 상관관계가 있는 대체 변수를 통해 의도치 않게 편향을 강화할 수 있다. 따라서, 진정한 공정성을 달성하려면 단순히 민감 속성을 제거하는 것을 넘어서 알고리즘 편향 탐지 및 공정성 평가가 반드시 병행되어야 한다.
Other semantic perturbations ((3-3)) # 의미 기반 변형
1) Semantic perturbations
lₚ-norm 기반 Robustness 검증은 픽셀 변화에만 검증할 수 있다. 하지만 물체를 바꾸거나 배경을 바꾸던가 등의 의미를 바꾸는 변형에 대해서는 모델이 치명적일 수 있다. 그래서 우리는 semantic level의 검증을 볼 것이다.
ex) 문장 부정의 부정, 물체 바꿈, 포즈 바꿈 등..
이미지 입력 데이터를 Semantic level에서 조작해서 모델의 예측을 바꾸려는 공격을 수학적으로 모델링하면 다음과 같다.
만약 모든 의미 변형에 대해 명시적인 함수 g를 정의할 수 있고, 픽셀 공간이 아닌 의미 공간 ϵk에서 lₚ 노름을 통해 의미 변형의 크기를 측정할 수 있다면, → 우리는 의미적 위협 모델을 수학적으로 다룰 수 있게 된다.
