AI의 증명안을 검증하는 방법: 존재성과 '최대 하나'를 구분하기

AI로부터 "따라서 해는 유일합니다"라는 증명안을 받았을 때, 그 직전까지 해가 존재함도 보여주고 있습니까?

"두 개의 해를 취하면 그것들은 같다"고 알아도, 해가 하나도 없을 가능성은 남아 있습니다. 이 글에서는 실수 방정식

AI의 증명안을 Lean 4로 검증한 기사에서는, 코드가 통과하는 것과 원래 문제를 해결한 것의 차이점을 다루었습니다. 이번에는 그보다 앞선 단계인, "결론 중 어느 부분까지 증명했는지"라는 읽는 방식에 초점을 맞춥니다.

'유일성'을 세 가지 질문으로 나누기

집합

존재는 다음 주장입니다.

최대 하나는 다음 주장입니다.

여기에는 해를 하나 선택할 약속이 없습니다. "만약 해가 두 개 있다면"이라는 조건부 주장입니다.

유일 존재를 보이기 위해서는, 존재와 최대 하나의 둘 다가 필요합니다. 기호로는

해가 없는데도 '최대 하나'는 성립한다

실수 방정식

어떤 실수

한편, "실수의 해"

이것은 논리의 빠져나가는 구멍(抜け道)이 아니라, '최대 하나'가 0개도 포함한다는 의미입니다.

반대쪽의 차이점도 살펴보겠습니다.

증명안이 둘 중 한쪽만이라면, '정확히 하나'라고 결론하기에는 부족합니다.

$ax=b$ 증명안 읽기

예: 설명용으로 다음 불충분한 증명안을 만듭니다.

해를 취하면 $u, v$이므로, $au=b=av$이다. 따라서 $a(u-v)=0$. 그러므로 $u=v$의 해는 유일하게 존재한다. $ax=b$

점검할 곳은 두 군데입니다.

-$ ext{에서 } a(u-v)=0 ext{으로 결론하려면, } u=v ext{가 필요하다.} ext{ 만약 최대 하나만 보여도, 해가 존재한다는 것은 아직 보여주지 않았다.}$

이 두 가지를 함께 "조금 보충하면 된다"고 처리하지 않고, 원래의 주장과 조건부 주장을 나눕니다.

$a, b$에서는 성립하지 않는다

원래의 주장은 모든 $ ext{이다. 즉, 조건 없는 '모든 실수'}$

$a

e 0$이면 유일하게 존재한다

조건부 별명제: 이것은 원래의 무조건 명제에 가정을 추가한, 다른 주장입니다. 올바른 수정 버전으로 취급할 수 있지만, 원래 주장을 그대로 증명했다고 쓰지는 않습니다.

먼저 존재를 보여줍니다.

따라서

다음으로 최대 하나를 보여줍니다. 임의의 해

존재와 최대 하나를 갖추었으므로,

조건별로 결론을 나열하기

증명안의 말을 따라가기만 해서 놓치기 쉬운 경우라면, 해의 개수로 정리할 수 있습니다.

| 고정된 | 존재 | 최대 하나 | 유일 존재 |
|---|---|
| 성립 | 성립 | 성립 | |
| ... |
두 번째 줄의 '최대 하나'는 해가 0개이므로 성립합니다. 세 번째 줄에는, 서로 다른 두 개의 해가 있기 때문에 성립하지 않습니다.

AI에게 다시 물어본다면, 두 가지 증명을 따로 요청하기

다음 입력은 그대로 시도할 수 있습니다. 돌아온 답변은, 대입과 조건 확인을 스스로 할 때까지는 증명되었다고 취급하지 마세요.

실수 $a, b$를 고정하고, 실수 $x$에 대해 $ax=b$를 생각하고 있습니다.
"모든 $a, b$에 대해 유일하게 존재한다"라는 무조건적인 주장을 점검해 주세요.
1. 존재, 최대 하나, 유일 존재를 구분해 주세요.
...

자신의 문제에서는 다음의 짧은 점검표로 대체합니다.

대상이 되는 집합:
고정하는 파라미터와 그 조건:
해가 만족하는 조건:
...

특히, 증명 도중의 "해를 취한다"를 확인합니다. 존재를 보여주기 전이라면, "만약 해가 있다면"이라는 조건부 논의일 수 있습니다. 존재가 이미 알려져 있다면, 그 근거를 한 줄 덧붙이면 됩니다.

Lean에서 확인할 때도, 먼저 결론을 읽기

Lean에 형식화할 경우에도, 처음에 "해가 있다"까지 요구한 선언인지, "두 개라면 같다"만 하는 선언인지를 비교합니다.

최대 하나만 형식화하여 증명이 통과해도, 해의 존재를 확인한 것은 아닙니다. 또한, 실수 전체 문제(real numbers)를 비음수 실수 문제(non-negative real numbers)로 바꾸거나,

원래의 일본어, 수식, Lean 선언의 대상・가정・결론을 대응시킨 후, 코드 실행 결과나 증명의 의존 관계를 확인합니다. 검사의 구체적인 진입점은 증명의 의존 관계를 확인할 기사로 나아갑니다.

이 기사의 점검표는, 자연어의 증명을 읽기 위한 것입니다. 표를 채웠다고 해서, Lean의 검증을 마친 것은 아닙니다.

연습: 두 가지 근거를 한 줄씩 쓰기

실수

확인용 정답

마지막으로, 자신의 증명안으로 돌아가서 "존재의 근거는 이 줄, 최대 하나의 근거는 이 줄"이라고 지적합니다. 둘 중 하나를 지적할 수 없다면, 다음에 조사할 곳이 결정됩니다.

AI가 증명과 원래 명제의 일치 여부를 실제 사례로 확인하기: AI에게 수학적 증명을 맡겨도 될까? Lean 4로 실제로 검증해보기

• 힌트 받기부터 백지 재구성까지: 수학과 학생이 AI를 공부에 활용한다면, 무엇을 맡기고 무엇은 스스로 생각해야 할까요?

수학적 주장을 Lean의 타입(type), 가정(assumption), 결론(conclusion)에 대응시키는 연습을 진행하고 싶은 분들은 『Lean 4로 배우는 형식 증명과 선형대수【제1권】』의 무료 서문에서 학습 범위를 확인할 수 있습니다. 선형대수를 기초로 전제로, Lean의 사전 지식 없이 타입과 증명의 읽는 법으로 나아가는 책입니다.

Discussion