증명 도우미 도구, 스칼라 함수 추정 자동화에 성공

최근의 글에서 자동으로 추정치를 검증하는 개념 증명 도구에 대해 언급한 바 있습니다. 그 이후로 이 도구를 두 번 개선하여, 먼저 일부 명제 논리를 처리할 수 있는 기본적인 증명 보조 도구로, 그리고 그 다음에는 Sympy 패키지를 활용해 기호 대수학을 수행하고 Lean 증명 보조 도구의 주요 특성을 모방한 더 유연한 증명 보조 도구로 발전시켰습니다. 이는 이제 확장 가능한 안정적인 프레임워크가 되어, 원래 목표였던 스칼라 함수의 점근 추정치 증명 외에도 다양한 수학적 작업을 처리할 수 있도록 전술, 새로운 Sympy 타입, 그리고 보조 정리를 추가할 수 있습니다. 현재 버전의 증명 보조 도구는 여기에서 확인할 수 있습니다. 초기 코딩 단계에서는 Python과 Sympy의 세부 사항을 이해하는 데 큰 언어 모델의 도움을 많이 받았으며, 특히 GitHub Copilot의 오토완성 기능이 매우 유용했습니다. 이 도구는 완전 자동화된 증명을 지원하지만, 현재는 사용자가 고수준의 "전략"을 제공하고 증명 보조 도구가 필요한 계산을 수행하여 증명을 완료하는 반자동화된 상호작용식 증명에 초점을 맞추고 있습니다. 도구의 작동 방식을 설명하기 위해서는 예제를 들어보는 것이 가장 쉽습니다. 이 도구는 Python의 상호작용 모드에서 사용하며, 한 번에 하나씩 Python 명령어를 입력합니다. 예를 들어 다음과 같은 연습 문제를 실행해볼 수 있습니다: ```python from main import * p = linarith_exercise() 증명을 시작합니다. 현재 증명 상태: x: 양의 실수 y: 양의 실수 z: 양의 실수 h1: x < 2y h2: y < 3z + 1 |- x < 7*z + 2 ``` 이 문제는 다음과 같습니다: ( x, y, z )가 양의 실수이고 ( x < 2y ) 그리고 ( y < 3z + 1 )일 때, ( x < 7z + 2 )임을 증명하십시오. 이 문제는 선형 산술을 통해 해결할 수 있으며, Linarith() 전략을 사용하면 됩니다: ```python p.use(Linarith()) 선형 산술에 의해 목표가 해결되었습니다! 증명이 완료되었습니다! ``` 세부 과정을 살펴보고 싶다면 verbose 플래그를 사용할 수도 있습니다: ```python p.use(Linarith(verbose=True)) 다음 부등식의 가능성을 확인합니다: 1z > 0 1x + -7z >= 2 1y + -3z < 1 1y > 0 1x > 0 1x + -2y < 0 다음과 같이 합산하여 불가능함을 확인합니다: 1z > 0를 1/4 배 1x + -7z >= 2를 1/4 배 1y + -3z < 1를 -1/2 배 1x + -2y < 0를 -1/4 배 선형 산술에 의해 목표가 해결되었습니다! 증명이 완료되었습니다! ``` 때로는 증명 과정에서 여러 경우를 분석해야 하는 경우가 있습니다. 이 경우 최종 증명은 트리 구조를 가집니다. 다음은 ( x )와 ( y )가 실수이고 ( x > -1 ) 및 ( x < 1 )이며, ( y > -2 ) 및 ( y < 2 )일 때, ( x + y > -3 )와 ( x + y < 3 )임을 증명하는 예입니다: ```python from main import * p = split_exercise() 증명을 시작합니다. 현재 증명 상태: x: 실수 y: 실수 h1: (x > -1) & (x < 1) h2: (y > -2) & (y < 2) |- (x + y > -3) & (x + y < 3) p.use(SplitHyp("h1")) 가설 h1: (x > -1) & (x < 1)를 x > -1, x < 1로 분해합니다. 1개의 목표가 남아 있습니다. p.use(SplitHyp("h2")) 가설 h2: (y > -2) & (y < 2)를 y > -2, y < 2로 분해합니다. 1개의 목표가 남아 있습니다. p.use(SplitGoal()) 목표를 논리합으로 분해합니다: x + y > -3, x + y < 3 2개의 목표가 남아 있습니다. p.use(Linarith()) 선형 산술에 의해 목표가 해결되었습니다! 1개의 목표가 남아 있습니다. p.use(Linarith()) 선형 산술에 의해 목표가 해결되었습니다! 증명이 완료되었습니다! print(p.proof()) example (x: 실수) (y: 실수) (h1: (x > -1) & (x < 1)) (h2: (y > -2) & (y < 2)): (x + y > -3) & (x + y < 3) := by split_hyp h1 split_hyp h2 split_goal . linarith linarith ``` 이 도구는 점근 추정에도 지원됩니다. Sympy 내에서 이전 게시물에서 소개한 크기 순서 표현을 구현하는 방법을 발견했습니다. Sympy는 일종의 비표준 해석학을 이미 본질적으로 구현하고 있어, 기호 변수는 표준 숫자 여부를 나타내는 is_number 플래그를 가지고 있습니다. 예를 들어, 숫자 3의 Sympy 버전 S(3)는 S(3).is_number == True이므로 표준 숫자입니다. 반면, 정수 변수 n = Symbol("n", integer=True)는 n.is_number == False이므로 비표준 숫자입니다. 이를 통해 다양한 (양의) 표현 ( X )의 크기 순서 ( \Theta(X) )를 생성하고, 점근 추정치 ( X \lesssim Y ) (Sympy에서는 lesssim(X, Y)로 구현)를 정의할 수 있습니다. 예를 들어, 양의 정수 ( N )와 양의 실수 ( x, y )가 ( x \leq 2N^2 )와 ( y < 3N )일 때, ( \Theta(x)\Theta(y) \leq \Theta(N)^4 )임을 증명하는 간단한 예는 다음과 같습니다: ```python p = loglinarith_exercise() 증명을 시작합니다. 현재 증명 상태: N: 양의 정수 x: 양의 실수 y: 양의 실수 h1: x <= 2N2 h2: y < 3N |- Theta(x)Theta(y) <= Theta(N)4 p.use(LogLinarith(verbose=True)) 다음 부등식의 가능성을 확인합니다: Theta(N)1 >= Theta(1) Theta(x)1 * Theta(N)-2 <= Theta(1) Theta(y)1 * Theta(N)-1 <= Theta(1) Theta(x)1 * Theta(y)1 * Theta(N)-4 > Theta(1) 다음과 같이 곱셈을 통해 불가능함을 확인합니다: Theta(N)1 >= Theta(1)를 1제곱 Theta(x)1 * Theta(N)-2 <= Theta(1)를 -1제곱 Theta(y)1 * Theta(N)-1 <= Theta(1)를 -1제곱 Theta(x)1 * Theta(y)1 * Theta(N)*-4 > Theta(1)를 1제곱 증명이 완료되었습니다! ``` 현재의 도전 과제는 로그 선형 프로그래밍 솔버가 "최대" 형태의 표현을 잘 처리하지 못한다는 것입니다. 예를 들어, ( x \leq 2N^2 + 1 )와 ( y < 3N + 4 )일 때, ( \Theta(x)\Theta(y) \leq \Theta(N)^3 )를 증명하는 데 어려움이 있습니다. 이는 LogLinarith()가 ( \Theta(N) )와 독립적인 변수로 ( \max(\Theta(1), \Theta(N)) )와 ( \max(\Theta(1), \Theta(N)^2) )를 취급하여, 이러한 양 사이의 중요한 (비선형) 관계를 빠뜨리기 때문입니다. 이러한 문제를 해결하기 위해, LogLinarith()를 개선하여 "최대" 형태의 항들을 적절히 처리할 수 있도록 할 계획입니다. 향후에는 기호 함수의 함수 공간 노름 추정을 위한 도구를 개발할 예정입니다. 예를 들어, Hölder 부등식과 Sobolev 임베딩 부등식을 적용하는 전략을 만들 계획입니다. Sympy 프레임워크는 이러한 객체를 위한 추가 객체 클래스를 생성하는 데 충분히 유연한 것으로 보입니다. 현재로서는 산술 평균-기하 평균 보조 정리를 통해 프레임워크를 소개하는 개념 증명 레마 하나만 있습니다. 이 증명 보조 도구의 기본 프레임워크에 만족하고 있어, 새로운 데이터 유형, 보조 정리, 전략 등을 도입하거나, 현재 도구의 능력을 벗어난데서 해결해야 할 예제 문제를 제안하거나 기여하는 등의 새로운 기능 제안에 대해 열려 있습니다. 이러한 도구가 쉽게 해결할 수 있는 문제에 대한 예제를 제공한다면, 개발 과정에 큰 도움이 될 것입니다.