AI가 수식 변형을 할 때, 동치성을 확인하는 방법: 제곱으로 늘어난 해를 대입하여 검증하기

AI로부터 방정식의 해법을 받았을 때, 마지막 '따라서 해는 두 개입니다'라는 문구 앞에 후보를 원래 식에 대입하는 과정이 있는지 확인해야 합니다.

양변을 제곱하면, 원래의 해는 유지되지만 불필요한 후보가 추가되는 경우가 있습니다. 계산이 정확하더라도, 변형된 방정식을 푸는 것만으로는 원래 방정식의 해를 구했다고 할 수 없습니다.

본 기사에서는 정의역(定義域)・화살표 방향・대입 세 가지 지점을 확인할 수 있습니다.

제곱한 등식으로부터 원래 등식으로 돌아가지 못하는 경우

실수

예를 들어,

제곱한 등식만으로는 인수분해에 의해
이 되고, 또는
AI의 증명안을 Lean 4로 검증한 기사에서는 이 비음 조건(非負条件)을 추가하면 다른 명제가 된다는 것을 다루었습니다. 이번에는 그 차이를 방정식 해법에 적용합니다.

$ ext{sqrt}(x+2)=x$ 의 해법 점검

예: 실수

먼저 좌변이 실수로 정의되려면, 원래 방정식의 해라면 입니다.

이 두 가지는 역할이 다릅니다.

'해라면 비음'이라고 유도한 것은 문제를 임의로 비음 실수로 변경해서가 아닙니다. 원래 등식에서 따라오는 조건을 추출하고 있는 것입니다.

설명용으로 불충분한 해법

양변을 제곱하면
입니다. $x+2=x^2$
인수분해하여 따라서, 해는 $(x-2)(x+1)=0$ 입니다. $x=2,-1$
인수분해까지의 계산은 맞지만, 마지막 '해'는 아직 후보일 뿐입니다. 원래 방정식에서 제곱한 방정식으로 진행하더라도, 역으로 돌아갈 수 있는지 확인하지 않았습니다.

먼저, 여기까지만 일방향 화살표로 쓸 수 있습니다.

처음만

후보를 원래 식에 대입하기

| 후보 | 원래 좌변 | 원래 우변 | 판정 |
|---|---|
| 원래 식을 만족하는 | |||
| 원래 식을 만족하지 않는 | | |

정의역만 확인한다고 충분하지 않을 수 있다는 것을 알 수 있습니다.

따라서, 원래 방정식의 해는
입니다. 이 결론에는 두 가지 근거가 있습니다.

• 원래의 해는 반드시 제곱한 방정식도 만족한다. 그 방정식을 모두 풀면,
  밖에 없습니다. $x=2,-1$
• 두 후보를 원래 식에 대입하고,
  을 남기고, 2를 제외했습니다. -1

후보가 빠지지 않은 이유와, 남긴 후보가 정말 해인 이유를 정리했습니다.

처음부터 동치(同値)로 쓸 거라면, 조건도 함께 남기기

원래 방정식과 동치가 되는 형태는 다음과 같습니다.

좌측은 제곱근이 정의되는

좌에서 우로의 변화는, 좌변의 비음성과 제곱에 의해 알 수 있습니다. 우에서 좌로의 변화는,
이 됨으로써 알 수 있습니다. 마지막
일반적으로
우측에서는

약분에서도, 원래 식이 정의되는 조건을 지우지 않기

다른 조작에서도 같은 확인을 사용할 수 있습니다. 실수 방정식
을 생각해 봅시다. 원래 좌변에는
입니다. 하지만,

AI에게 물어볼 때는, 계산 수정과 화살표 점검을 분리하기

다음은 같은 문제로 바로 사용할 수 있는 입력 예시입니다. 답변을 받으면 위 대입표와 비교해 보세요.

실수 x에 대해 $	ext{sqrt}(x+2)=x$ 를 풀고 있습니다.
$	ext{sqrt}$는 비음 실수에 대한 비음의 제곱근입니다.
다음 설명을 점검해 주세요.
...

자신의 문제에서는 다음 다섯 줄을 채웁니다.

원래 식과, 식이 정의되는 조건:
원래 식에서 유도 가능한 부호・비영 조건:
각 변형의 방향과, 역방향에 필요한 조건:
...

중간에

Lean으로 넘어갈 때도, 무엇을 확인할지 미리 정하기

제곱한 방정식의 해가
형식화한다면, 먼저 다음 세 항목을 일본어로 고정합니다.

• 원래 등식으로부터, 정의역・부호 조건과 제곱한 등식이 따라야 함.
• 필요한 조건을 보존한 후보로부터, 원래 등식으로 돌아갈 수 있음.
• 마지막에 남긴 해의 집합이, 원래 방정식의 해의 집합과 일치함.

수학에서는 미정의로 하는 식에 대해, 라이브러리가 모든 입력에 값이 주어지는 정의를 채택하는 경우도 있습니다. 제곱근이나 나눗셈을 사용할 때는, 기호가 비슷할 뿐 대응으로 결정하지 말고, 사용하는 정의와 조건을 확인해야 합니다. 본고에서는 Mathlib의 API나 정리명을 제시・실행하고 있지는 않습니다.

코드 포함 실례와, 원래 명제와의 대조는, AI에게 수학 증명을 맡겨도 되는지? Lean 4로 실제로 검증해 보는 단계로 넘어갑니다.

연습: 후보를 두 개 내고 돌아가기

실수 방정식

정의역, 원래 식에서 나오는 부호 조건, 제곱한 후의 후보, 원래 식으로의 대입을 순서대로 씁니다.

확인용 정답

정의역은
제곱하면

원래의 해는 반드시 제곱 후 후보에 포함되며, 모든 후보를 대입했으므로, 해는

자신의 답안의 '따라서 해는' 부분으로 돌아가서, 그 직전에 후보들이 모두 소진되었고 원래의 식을 만족한다는 두 가지 점을 설명할 수 있는지 확인해 주세요.

수학적 조건을 Lean의 타입(type), 가정(assumption), 결론(conclusion)에 대응시키는 연습으로 넘어가고 싶은 분들은 『Lean 4로 배우는 형식 증명과 선형대수【제1권】』의 무료 서문에서 대상 독자와 학습 범위를 확인할 수 있습니다. Lean의 사전 지식은 필요하지 않으며, 후반부는 선형대수의 기초를 전제로 합니다. 서문, 제1장, 제2장이 무료로 공개되어 있습니다.

Discussion