이 기사는 다음 두 기사 사이에 있는 질문을 대화 형식으로 정중하게 파고드는 내용입니다.

Python의 타입 힌트(type hint)의 한계를 넘어서는 「사이형(refinement types)」 입문 ―― "x > 0"을 타입에 쓰면 어떤 일이 일어나는가 (LiquidHaskell・F*・Typed Racket・Idris 2로의 초대)

AI Agent는 사회 규범에 어긋나더라도, 논리적으로 옳다면 실행 가능하다고 판단해 버린다 ── 「무엇을 해도 되는가」를 결정하는 책임은, AI가 똑똑해질수록 인간에게 집중된다

전자의 기사에서는 사이형(refinement types)이나 의존 타입(dependent types)에 대해 해설했습니다. 나아가 Lean 4・Coq・F*와 같은 증명 지원계 언어가 코드의 정확성을 기계적으로 증명할 수 있다는 점을 다루었습니다.

후자의 기사에서는 AI Agent가 생성한 코드는 그럴듯하게 작동하는 것처럼 보여도, 인간 설계자・개발자・운영자가 의도한 사양(specification)에서 벗어나 있을 가능성이 있다고 언급했습니다.

이 두 기사 사이에는 다음과 같은 질문이 놓여 있습니다.

형식 증명(formal proof)을 사용하면, AI Agent가 생성한 코드가 「인간의 의도대로 작동하고 있는가」를 판정할 수 있을까?.

이 기사에서는 위의 질문에 마주해 보고자 합니다.

이 질문을 학부생인 타로 군이 전임 강사를 찾아가 질문합니다.

이하, 대화 형식으로 전달합니다.

또한, 이 기사에서 「사양(specification)」이라고 말할 때, 그것은 인간이 자연어나 수리적 기술을 통해 외부화한 요구사항 전체를 가리킵니다.

• 자연어로 작성된 요구 사양
• F*와 같은 증명 지원계 언어로 작성된 형식 사양(formal specification)
• Lean 4나 Rocq(구 Coq)와 같은 증명 지원계 언어로 작성된 형식 사양
• 그 중간에 있는 반형식적(semi-formal) 사양 등

「사양」이라는 단어는 적어도 이 기사에서는 위의 모든 것을 포함하는 넓은 의미로 사용합니다.

타로 군

선생님, 잠시 시간 괜찮으신가요? 요전에 읽은 Qiita의 기사에서 조금 신경 쓰이는 점이 있어서요.

전임 강사
물론 괜찮지. 말해 보게. 어떤 기사인가?

타로 군
사이형에 관한 입문 기사와 AI Agent에 관한 기사, 이렇게 두 편입니다.
같은 저자분이 쓰신 것이라 둘 다 흥미롭게 읽었습니다.

전임 강사
아, Etale Cohomology 님의 기사구나. 나도 읽었네.

타로 군
네, 그 두 기사를 읽다 보니 도저히 이해되지 않는 점이 생겼습니다.
그것이 바로 다음 질문입니다.

타로 군
형식 증명을 사용하면, 『인간이 의도한 사양대로 작동하고 있는지』를 판별할 수 있습니까?

전임 강사
좋은 질문이군.
그 질문은 형식 기법(formal methods)의 세계에서 오랫동안 논의되어 온 질문의 핵심에 있네.

타로 군
그렇게 깊은 질문인가요?

전임 강사
그렇다네.
결론부터 말하자면, 답은 **「조건부로, 예」**라네.
다만, 여기에는 주의해야 할 점이 있지.
Correctness(정확성)와 Appropriateness(적절성)라는 두 가지 개념을 올바르게 식별하는 것이라네.
두 개념을 혼동하면 형식 증명의 진정한 힘과 그 한계를 볼 수 없게 되지.

타로 군
그 두 개념의 경계에 대해 알려주세요.

전임 강사
그 경계를 파악하기 위해서는 우선 한 가지 밑준비가 필요하네.
AI Agent가 생성한 코드가 인간의 의도대로 작동하기까지는 사실 4단계가 있네.
이 4단계를 머릿속에 넣어 두면, Correctness와 Appropriateness의 경계가 높은 해상도로 떠오를 걸세.
차례대로 살펴보지.

전임 강사
AI Agent가 생성한 코드가 인간의 의도대로 작동하기까지는 사실 4단계가 있네. 차례대로 살펴보지.

전임 강사
먼저, 다음 4단계라네.

타로 군
선생님, 조금 납득이 가지 않는 부분이 있습니다.
④의 「컴파일러나 증명기가 증명을 검사한다」 부분 말입니다.
③에서 「구현이 사양을 만족함」을 형식 증명으로 증명할 수 있다고 하셨습니다.
하지만 ④에서 갑자기 「증명을 검사한다」는 말이 나옵니다.
증명을 만드는 것과 증명을 검사하는 것은 별개의 행위인가요?

전임 강사
좋은 직감이야. 이 부분은 형식 증명을 처음 배우는 사람이 거의 전원서 넘어지는 지점이지.
차례대로 설명해 주겠네.

전임 강사

우선, ③과 ④는 사실 서로 다른 활동이라네.

전임 강사

③ ── 「구현이 사양을 만족함」을 형식 증명 (Formal Proof)으로 나타내는 것.

이것은 Lean 4와 같은 프로그래밍 언어 안에서, "이 구현은 이 사양을 만족한다"라는 주장의 **증거 (evidence)**를 데이터로서 구축하는 활동이지.

이 "증거 데이터"를 **증명 (proof)**이라고 부른다네.

전임 강사

증명을 만드는 것은 사실 프로그래밍과 매우 흡사한 창조적인 활동이라네.

인간(혹은 AI Agent)이 머리를 써서 증명을 조립해 나가지.

이것은 기계가 완전히 자동화하기 어려운 창조적인 업무의 측면을 가지고 있다네.

전임 강사

④ ── 「컴파일러나 증명기가 증명을 검사함".

반면 이것은 기계가 담당해야 할 역할이지.

③에서 만들어진 증명 데이터가 형식적인 규칙에 따라 올바르게 구성되었는지를 기계가 하나하나 기계적으로 체크하는 것이라네.

이를 **증명 검사 (proof checking)**라고 부르지.

전임 강사

흥미로운 점은 말이야, 증명을 만드는 것은 창조적이지만, 증명을 검사하는 것은 기계적이라는 사실이라네.

기계는 아직 증명을 "떠올리는" 데는 능숙하지 않아.

하지만 이미 작성된 증명이 맞는지 기계적으로 검사하는 것은 아주 잘하지.

Lean 4도, (구) Coq도, F* 도 이 "증명 검사의 기계화"를 정확하고도 빠르게 수행해 준다네.

전임 강사

이 구조에는 깊은 이유가 있어.

증명을 만드는 것은 무수한 가능성 중 하나를 선택하는 탐색의 활동이지.

반면 증명이 맞는지 검사하는 것은 정해진 규칙에 따라 하나하나 확인하는 기계적인 활동이라네.

양자는 복잡성의 수준이 근본적으로 다르지.

타로 군

그렇군요. ③과 ④는 각각 다른 활동이고, ③은 창조적, ④는 기계적이라는 말씀이시죠?

그리고 ④를 기계화할 수 있다는 점이 형식 증명의 실용성에 있어 근본적인 부분이군요.

전임 강사

그 이해가 거의 맞네.

이 구조는 AI Agent 시대에도 큰 의미를 갖게 될 거야.

AI Agent가 증명을 "만드는" 일에도 조금씩 손을 대기 시작하고 있기 때문이지.

하지만 말이야, AI Agent가 만든 증명이 맞는지 최종적으로 보증하는 것은 어디까지나 기계적인 증명 검사라네.

이것이 AI Agent 시대에 형식 증명이 가진 독특한 강점이기도 하지.

타로 군

AI Agent 시대에 형식 증명이 담당해야 할 사회적 역할도 변하고 있군요!

방금 전 표에서 ①과 ②는 인간이 결정하고, ③과 ④는 기계가 담당할 수 있다고 정리한 방식도 납득이 가요.

전임 강사

이 4단계를 하나의 흐름으로 쓰면 다음과 같다네.

전임 강사

형식 증명이 보증해 주는 것은 이 흐름의 하단부뿐이라네.

전임 강사

구체적으로는, **「프로그램 ⇒ 사양」의 관계, 즉 「프로그램이 작성된 사양을 올바르게 만족하고 있음」**은 Lean 4, Coq, F*와 같은 형식 증명 언어가 엄격하게 보증해 주지.

전임 강사

하지만, **「사양 ⇒ 인간의 진정한 의도」의 관계, 즉 「작성된 사양이 인간이 정말로 원했던 것을 올바르게 표현하고 있음」**은 형식 증명으로 보증할 수 없다네.

왜냐하면, 형식 증명 언어에는 애초에 인간의 의도를 읽어낼 수단이 없기 때문이지.

타로 군

그렇군요.

형식 증명은 「사양대로 코드가 동작하는 것」은 보증해 주지만, 「사양이 인간의 본래 의도를 올바르게 나타내고 있는가」는 보증해 주지 않는다는 말씀이시죠?

전임 강사

그 이해가 거의 맞네.

전임 강사

이 점에 대해, **형식 기법 (Formal Methods)**의 세계에서는 예전부터 다음과 같이 말해 왔지.

전임 강사

Correctness ≠ Appropriateness

타로 군

Correctness와 Appropriateness 말씀이신가요?

전임 강사

그렇다네. 일본어로 번역하면 다음과 같지.

Correctness (정확성): 구현 코드가 작성된 사양대로 동작하는 것
Appropriateness (적절성): 작성된 사양이 인간이 정말로 원했던 것인 것

전임 강사

보충하자면, 형식 기법의 전문 용어로서 Correctness란

**「구현이 형식 사양을 만족함」**을 가리른다네.

"사양대로 동작한다"는 것은 그것을 쉽게 풀어서 말한 것이지.

전문서에서 Correctness라는 단어를 만났을 때는,

이 정의를 떠올리면 된다.

전임 강사

그리고, 이 두 가지는 완전히 다른 개념이다.

하지만 많은 사람이 이 두 가지를 혼동하곤 한다.

「코드가 사양대로 동작하는 것」과 「그 코드가 인간의 바람을 실현하는 것」은 별개의 문제다.

타로 군

서두에서 언급한 AI Agent 기사의 주장과 연결되네요!

전임 강사

정확하다.

그 기사에서 언급되었던 **「AI Agent는 사회 규범에 어긋나더라도, 논리적으로 옳다면 실행 가능하다고 판단해 버린다」**라는 주장은, 형식 기법 (Formal Methods)의 세계에서 오랫동안 논의되어 온, 이 Correctness와 Appropriateness를 서로 구분해야 한다는 인식과 맥을 같이 한다.

타로 군

구체적으로 Lean 4에서는 무엇을 증명할 수 있는지 예를 보여주실 수 있나요?

전임 강사

물론이지.

정렬 (Sort) 알고리즘을 예로 들어보자.

전임 강사

예를 들어, 네가 AI Agent에게 "정수 리스트를 오름차순으로 정렬하는 함수 sort를 작성해 줘"라고 의뢰했다고 가정하자.

AI Agent는 다음과 같은 코드를 제시할 것이다.

# Python 예시
def sort(xs: list[int]) -> list[int]:
    return sorted(xs)

타로 군

이건 Python의 내장 함수인 sorted를 호출하고 있을 뿐이네요.

확실히 이 코드는 동작합니다.

전임 강사

여기서 질문을 하나 던져보지.

이 코드는 정말로 '올바르게' 동작할까?

타로 군

테스트로 확인하면 되지 않을까요?

전임 강사

테스트로는 몇 가지 입력에 대해서는 확인할 수 있다.

하지만, 모든 입력에 대해 이 함수가 정말로 올바르게 동작한다고 보장하려면, 테스트가 아니라 형식 증명 (Formal Proof)이 필요하다.

전임 강사

Lean 4에서는 다음과 같은 증명을 작성할 수 있다.

theorem sort_correct (xs : List Int) :
Permutation xs (sort xs) ∧ Sorted (sort xs)

전임 강사

실제로는 이 뒤에 증명 (proof term 또는 tactic)이 이어지며, Lean은 그 증명을 기계적으로 검사한다.

여기서는 지면 관계상 증명의 내용은 생략하겠다.

전임 강사

이 정리 (Theorem)는 다음 두 가지를 주장하고 있다.

Permutation xs (sort xs)

── sort xs는 원래 리스트 xs의 순열이다 (요소를 잃지 않고, 요소를 늘리지 않으며, 순서만 바꾼 것이다).

Sorted (sort xs)

── sort xs는 오름차순으로 정렬되어 있다.

타로 군

Lean 4 코드는 처음 보지만, 대충 어떤 의미인지는 알 것 같아요.
무엇을 의미하는지 알려주세요.

전임 강사

함께 읽어보자.

전임 강사

theorem sort_correct는 이 정리에 sort_correct라는 이름을 붙이는 선언이다.
Python으로 치면 함수 이름을 붙이는 것과 비슷하다.

전임 강사

(xs : List Int)는 이 정리가 "임의의 정수 리스트 xs에 대해 성립한다"는 것을 말한다. Python의 타입 힌트(Type Hint)인 xs: list[int]에 해당한다.

전임 강사

그리고 콜론 뒤의 Permutation xs (sort xs) ∧ Sorted (sort xs)가 바로 증명해야 할 명제다.
∧는 "그리고 (and)"를 의미한다.

타로 군

그렇군요.

이 정리를 Lean 4로 증명할 수 있다면, 모든 정수 리스트에 대해 sort 함수가 「순열이며, 동시에 오름차순이다」라는 것이 수학적으로 보장된다는 뜻이군요?

전임 강사

그렇다.

테스트로 하나하나의 입력을 확인하는 것과는 근본적으로 다른 보장의 강도다.

전임 강사

이 부분이 형식 증명의 가장 아름다운 점이다.

이 단 한 줄의 타입 정의가 모든 입력에 대한 테스트를 겸하고 있다.

테스트 코드를 1만 줄, 10만 줄 작성하더라도, 그것은 유한한 개수의 입력을 확인할 뿐이다.

하지만 이 정리를 Lean 4로 증명할 수 있다면, 이 세상에 존재하는 모든 정수의 리스트에 대해 sort 함수가 올바르게 작동한다는 것이 단번에, 수학적으로 보장된다.

전임 강사

Lean 4의 타입 시스템(Type System)은 이 정리를 증명으로서 구축할 수 있을 때에만 컴파일을 통과시킨다.

증명이 완성되지 않는 한, 코드는 받아들여질 수 없다.

이런 의미에서, Lean 4는 Correctness(정확성)를 엄격하게 보장해 준다.

타로 군

**"타입(Type)"**이 등장했군요!

이 부분은 형님이 타입 시스템론과 함수형 언어, 그리고 형식 증명·정리 증명기(Theorem Prover) 사이의 관계성에 대해 강한 흥미를 느끼고 있는 것 같습니다.

또한 다른 대화편에서, 타입 시스템론과의 오늘 논의의 관계성에 대해서도 알려주세요.

전임 강사

좋은 착안점이네.

오늘의 대화에서 아주 살짝 언급한 **의존 타입 이론 (Dependent Type Theory)**은 사실 그 거대한 지도 속의 하나의 봉우리란다.

• 함수형 프로그래밍 언어의 타입 시스템
• Curry-Howard 대응 (Curry-Howard Correspondence)
• 선형 타입 (Linear Type), 篩 타입 (Sieve Type), 의존 타입 (Dependent Type)

이것들은 각각 독립된 화제처럼 보이지만, 깊은 곳에서 하나로 연결되어 있어.

그 연결의 전체상을 또 다른 기회에 시간을 두고 차근차근 이야기해 보자.

타로 군

네, 기대하고 있겠습니다!

타로 군

Lean 4는 Correctness의 보장, 즉 구현이 사양(Specification)을 충족하고 있다는 보장에 대해 훌륭한 메커니즘을 제공해 주는 것이군요!

전임 강사

그렇지.

하지만 여기서 한 가지, 매우 중요한 질문이 남는다.

전임 강사

애초에, "오름차순으로 정렬한다"라는 사양이 고객의 진정한 요구사항이었을까?

타로 군

네?

전임 강사

예를 들어, 네 고객이 "상품 리스트를 잘 팔리는 순서대로 정렬하고 싶다"라고 생각했다고 가정해 보자.

너는 그 요구사항을 "상품 리스트를 매출액이 높은 순으로 정렬한다"라고 사양으로 작성했어.

그리고 AI Agent가 그 사양을 올바르게 구현하는 코드를 작성했지.

Lean 4에서도 그 코드가 사양대로 작동한다는 것을 증명할 수 있었어.

전임 강사

하지만, 사실 고객이 정말로 원했던 것이 "지난주 매출액" 순이 아니라 "향후 1개월의 예측 매출" 순이었다면 어떨까?

타로 군

그 경우, 코드는 사양대로 올바르게 작동하더라도 고객의 진정한 의도와는 다른 것이 되어 버리네요...

전임 강사

맞아.

이 괴리는 Lean 4가 원리적으로 검출할 수 없어.

Lean 4가 알 수 있는 것은 작성된 사양과 작성된 코드 사이의 관계뿐이야.

고객의 머릿속에 있는 "진정한 바람"은 Lean 4의 시야 밖에 있지.

전임 강사

여기서 수학적인 배경을 조금 언급해 두자.

Lean 4가 다룰 수 있는 것은 의존 타입 이론 (Dependent Type Theory)이라는 엄격한 형식 체계 위에 정의된 명제와 증명뿐이다.

타로 군

의존 타입 이론이란 무엇인가요?

전임 강사

쉽게 말하자면, **"타입이 값에 의존할 수 있다"**는 이론이야.

전임 강사

Python이나 Java, 혹은 일반적인 함수형 언어에서도 타입은 "정수"나 "문자열"처럼 값과는 독립적으로 결정되는 분류지.

하지만 의존 타입 이론에서는 **"길이가 3인 정수 리스트"**라든가, "양의 정수", **"정렬된 정수 리스트"**와 같이 값의 성질 그 자체를 타입으로 기술할 수 있어.

전임 강사

이 덕분에 "함수의 입력과 출력 사이의 관계"를 타입으로서 엄격하게 기술할 수 있지.

예를 들어, 아까 말한 sort 함수라면 "입력을 재배열하며, 동시에 오름차순인 출력을 반환하는 함수"라는 성질 그 자체를 타입으로 기술할 수 있는 거야.

그러면 Lean 4의 컴파일러는 그 성질을 만족하지 않는 구현을 컴파일 에러로 거부해 준단다.

타로 군

값의 성질을 타입으로 쓸 수 있다 ── 이것이 의존 타입 이론의 힘이군요!

타로 군

값의 성질을 타입으로 나타낼 수 있다니, 이것이 의존 타입 이론의 힘이군요. 구체적으로는 어떤 코드가 되나요?

전임 강사

응, 좋은 질문이야. 실제 코드를 한번 보자.

먼저, 의존 타입 (Dependent Type)을 다루는 대표적인 두 가지 언어 ── Lean 4와, 의존 타입에 특화된 함수형 프로그래밍 언어 Idris ── 를 통해, 「길이가 3인 정수 리스트」를 어떻게 작성하는지 차례대로 살펴보자.

전임 강사

Lean 4에서는 다음과 같이 작성할 수 있다.

-- 길이가 n인 요소 타입 α의 리스트 (Lean 4의 Vector 타입 정의)
inductive Vector (α : Type) : Nat → Type where
| nil : Vector α 0
...

전임 강사

한 줄씩 풀어보자.

전임 강사

inductive Vector (α : Type) : Nat → Type where

라는 행은,

**「Vector라는 새로운 타입을 정의한다」**는 선언이다.

(α : Type)

은 「Vector가 요소의 타입 α를 받는다」는 것을 나타내고,

Nat → Type

은 「나아가 자연수 n을 받아서 타입을 반환한다」는 것을 나타낸다.

이 「값(자연수 n)을 받아서 타입을 반환한다」는 성질이야말로 의존 타입의 본질이다.

전임 강사

| nil : Vector α 0

이라는 행은,

**「nil(빈 벡터)은 길이가 정확히 0인 Vector이다」**라는 주장이다.

즉, 빈 벡터의 타입 그 자체에 「길이가 0」이라는 정보가 새겨져 있다.

전임 강사

| cons : α → Vector α n → Vector α (n + 1)

이라는 행은,

**「cons는 요소 α와 길이 n인 Vector를 받아서, 길이 n + 1인 Vector를 반환한다」**는 주장이다.

요소를 하나 더하면 길이의 타입이 자동으로 n에서 n + 1로 늘어난다.

이 관계가 타입 레벨에서 엄격하게 관리되고 있다.

전임 강사

그리고 def myList : Vector Int 3 := ...

라는 행이,

**「myList는 길이가 정확히 3인 Int의 리스트이다」**라는 선언이다.

여기서 만약 우변의 요소 개수를 틀린다면, Lean 4의 컴파일러는 즉시 컴파일 에러를 발생시킨다.

실행 전에 타입 레벨에서 검출되는 것이다.

타로 군

그렇군요.

「길이 3」이라는 정보가 타입 그 자체에 내장되어 있는 것이군요!

전임 강사

그렇다.

다음으로 Idris의 코드 예시를 살펴보자.

Idris는 의존 타입을 다루는 데 특화된 함수형 프로그래밍 언어다.

Lean 4는 「정리 증명계와 범용 프로그래밍 언어 양쪽 모두」를 지향하지만, Idris는 「의존 타입을 가진 실용적인 프로그래밍 언어」 쪽에 무게 중심을 두고 있다.

-- 길이가 n인 요소 타입 a의 리스트 (Idris의 표준 라이브러리에 Vect가 있음)
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
...

전임 강사

Idris의 작성 방식은 Lean 4와 매우 흡사하다.

Vect : Nat -> Type -> Type

이라는 행은,

「Vect는 자연수 n과 요소 타입 a를 받아서 타입을 반환한다」는 선언이다.

Z는 0 (zero), S k는 k의 후계자 (k + 1)를 나타낸다.

그리고 myList : Vect 3 Int는 「myList는 길이가 3인 Int의 리스트이다」라는 선언이다.

타로 군

Lean 4와 Idris는 작성 방식의 세부 사항은 다르지만, 의존 타입의 사고방식은 공통적이군요.

전임 강사

정확하다.

의존 타입 이론이라는 동일한 수학적 토대 위에 Lean 4도, Idris도, Coq (현재는 Rocq)도, Agda도, F*도 구축되어 있다.

각 언어의 모습은 다르지만, 뿌리가 되는 발상은 공통적이다.

전임 강사

그리고 이 「길이 3인 리스트」의 예시는 의존 타입의 하나의 응용에 불과하다.

「양의 정수」, 「정렬된 리스트」, 「특정 성질을 만족하는 함수」 등, 값의 성질을 타입으로 쓸 수 있는 모든 상황에서 의존 타입의 힘이 발휘된다.

타로 군

그렇군요.

의존 타입은 코드의 안전성을 실행 전 타입 검사 단계에서 보장해 주는 강력한 도구군요.

전임 강사

그 이해가 거의 맞다.

전임 강사

그런데 말이지, 이 의존 타입 이론은 **커리-하워드 대응 (Curry-Howard Correspondence)**이라는, 논리학과 프로그래밍 사이의 깊은 대응을 통해 수학적 증명 그 자체를 프로그램으로서 써 내려갈 수 있다는 놀라운 성질을 가지고 있어.

이것이 Lean 4가 정리 증명계 (Theorem Prover)로 사용될 수 있는 이유다.

전임 강사

하지만 말이야, 여기에 중요한 한계가 있어.

의존 타입 이론이라는 형식 체계 안에 써 내려갈 수 있는 것은, 어디까지나 형식적인 명제와 증명뿐이야.

**"고객이 정말로 원했던 것"**이라는, **아직 수식이나 타입으로 정의되지 않은 모호한 개념 (비형식적인 세계)**을, 의존 타입 이론의 형식적인 세계로 매핑하는 것 자체는 수학이나 논리학의 힘으로는 어찌할 수 없지.

타로 군

그렇군요.

형식적인 세계와 비형식적인 현실 세계 사이의 간극은 형식 체계의 힘으로는 어찌할 수 없는 것이군요.

전임 강사

그 이해가 거의 맞다.

이것이 Lean 4가 원리적으로 사양과 인간의 의도 사이의 간극을 탐지할 수 없는 진정한 이유다.

전임 강사

지금까지의 논의를 다음 3단계의 그림으로 정리할 수 있어.

전임 강사

이 3가지 단계에는 각각 역할 분담이 있다.

① 논리적으로 작동함 ── AI Agent가 비교적 잘하는 영역
② 사양대로임 ── Lean 4, Coq, F* 등의 형식 증명이 강력한 무기를 제공하는 영역
③ 인간이 정말로 원했던 것 ── 인간이 책임을 지는 영역

타로 군

그렇군요.

각 단계마다 담당자가 다르군요.

전임 강사

그렇다.

그리고 이 역할 분담이야말로, 이미 다루었던 AI Agent에 관한 기사의 주장과 깊게 공명하고 있지.

전임 강사

그 기사의 논점 2에서 제시된 **"그럴듯한 동작과 인간이 의도한 사양의 구별"**은 형식 증명이 바로 메우려고 하는 간극의 일부다.

전임 강사

다만, 형식 증명으로 메울 수 있는 것은 "구현과 사양의 간극"이며, "사양과 인간의 의도의 간극"은 남는다.

타로 군

선생님, 여기서 또 하나의 깊은 질문이 떠올랐습니다.

전임 강사

음, 들려주렴.

타로 군

사양과 인간의 의도 사이에 간극이 있는지 없는지를 체크할 수 있는 것은, 의도를 가진 인간뿐인 걸까요?

타로 군

AI Agent도, 형식 증명 언어도, 애초에 의도를 가지지 않는 존재잖아요.
의도를 가지지 않는 존재에게는 타자의 의도가 올바르게 반영되어 있는지를 원리적으로 판정할 수 없는 것이 아닌가 싶습니다.

전임 강사

너, 그것은 이 분야에서 가장 깊은 질문 중 하나다.

전임 강사

차례대로 생각해 보자.

전임 강사

먼저, **"의도를 가진다는 것은 무엇인가"**라는 질문부터 시작할 필요가 있어.

타로 군

네.

전임 강사

의도를 가진다는 것은 적어도 다음 세 가지 요소를 포함한다.

① 무언가를 바람 (욕구, 가치, 목적)
② 그 바람을 외부의 기술 (언어, 기호, 사양서, 코드)로 변환하려는 시도를 수행함
③ 외부의 기술이 자신의 바람을 올바르게 표현하고 있는지를 성찰적으로 판단하는 능력을 가짐

전임 강사

AI Agent는 이 중 ②의 작업은 매우 고도로 수행할 수 있어.
인간의 지시를 받아 그것을 코드로 변환하는 작업은 AI Agent의 특기 분야지.

전임 강사

하지만, 현재 실용화되어 있는 AI Agent는 인간과 같은 주체적인 가치 판단이나 목적을 자율적으로 가지는 것은 아니다.

타로 군

AI Agent에게는 애초에 "이것을 하고 싶다"라는 주체적인 바람이 없다는 말씀이시군요?

전임 강사

그렇다.

AI Agent가 생성하는 코드는 너의 지시로부터 추측한 사양에 대해 올바르게 동작하는 코드다.
하지만 AI Agent 스스로가 "이런 코드를 쓰고 싶다"라고 주체적으로 바라는 것은 아니야.
현재 실용화되어 있는 AI Agent에게는 인간과 같은 주체적인 가치 판단이나, 자율적으로 선택하는 목적이나 가치관이 없다.

전임 강사

따라서 AI Agent에게는 "너의 지시를 AI Agent가 추측한 사양"과 "네가 정말로 원했던 것" 사이에 괴리가 있는지 없는지를 판정할 근거가 되는 기준이 없다.

타로 군

그렇군요.

판단하는 기준 그 자체가 AI Agent에게는 존재하지 않는 것이군요.

전임 강사

그렇다.

같은 말이 Lean 4, Coq, F*에도 적용된다.

이러한 증명 보조 시스템 (Proof Assistant) 언어들은 극히 강력한 논리 체계를 가지고 있지만, 그곳에는 「무엇을 원하는가」라는 가치의 차원은 존재하지 않는다

전임 강사

Lean 4는 「이 정리는 이 공리계로부터 도출될 수 있다」는 것을 엄밀하게 판정한다.

하지만 「이 정리를 증명할 의미가 있는가, 이 공리계를 채택할 의미가 있는가, 애초에 무엇을 증명 대상으로 삼아야 하는가」는 Lean 4의 시야 밖에 있다.

타로 군

즉, 사양과 인간의 의도 사이의 간극을 판정할 수 있는 것은 의도를 가진 인간뿐이라는 저의 추론은 원리적으로 맞았던 것인가요?

전임 강사

그 이해가 거의 맞다. ── 다만, 이 결론에는 약간의 보충이 필요하다.

전임 강사

네 결론은 옳다.

다만, 실무 현장에서는 「의도를 가진 인간」이 누구인지가 항상 명확하지는 않다

타로 군

그 말씀은?

전임 강사

규모가 큰 조직에서 소프트웨어를 개발하는 상황을 생각해 보자.

사양을 작성하는 것은 프로덕트 매니저 (Product Manager)다.

하지만 그 사양의 배후에 있는 「진정한 의도」는 그 조직의 경영자, 고객, 혹은 그 업계의 관습 속에 있다.

전임 강사