Computer-assisted Proof Under Audit: Typos, Certificate Errors, and Reproducible Exact Checks for a Symbolic Invertibility Proof

기술 요약: 감사 중인 컴퓨터 보조 증명

문제 정의
본 논문은 근사적 자기 유사 Boussinesq 프로파일 주변의 선형화된 연산자의 가역성에 관한 기발표된 컴퓨터 보조 증명(CAP)에 대하여, 독립적이고 버전이 고정된 소스 레벨 감사를 제시한다. 대상 증명은 원래 arXiv:2310.19781v2로 발표되었고 이후 Communications in Mathematical Physics (CMP)에 게재되었으며, 비압축성 유체의 특이점 형성을 증명하는 데 필요한 경계 및 재구성 단계를 확립하기 위해 MATLAB을 통해 생성된 심볼릭 인증서(symbolic certificate)에 의존하고 있다. 본 감사는 공개된 계산 인증서가 주장된 결론을 엄밀하게 뒷받받하는지 여부를 조사하며, 특히 수학적 산문, 공개된 소스 코드, 그리고 정확한 산술 결과 사이의 일관성을 검증한다.

방법론
저자는 "인쇄된 오타"(코드가 정답이거나 주변 논리가 올바르지만 텍스트에 오기가 있는 경우)와 "인증서 오류"(공개된 계산이 필요한 함의를 확립하는 데 실패하는 결함)를 구분하는 포렌식 감사 방법론을 채택한다. 과정은 다음과 같다:

1. 버전 고정 (Version Pinning): 저자는 SHA-256 다이제스트를 사용하여 특정 arXiv v2 소스 아카이브와 CMP 버전을 정렬함으로써 정확한 출처를 보장한다.
2. 정확한 산술 검증 (Exact Arithmetic Verification): 부동 소수점 재실행에 의존하는 대신, 특정 경계, 계수 루프 및 재구성 공식을 검증하기 위해 유리수를 사용하는 재현 가능한 정확한 산술 스크립트를 구성한다.
3. 소스 레벨 비교 (Source-Level Comparison): 논문의 수학적 정의와 공개된 MATLAB 스크립트(예: invertibility.tex, shorttime_sym.m, profile.m)의 실제 구현을 비교하여 인덱스, 부호, 도메인 범위 및 누락된 항의 불일치를 확인한다.
4. 반례 구성 (Counterexample Construction): 결함이 발견된 경우, 저자는 특정 경계나 방정식이 정의된 조건 하에서 실패함을 보여주는 정확한 반례를 생성한다.

주요 결과 및 성과
감사는 몇몇 타이포(typo)와 함께 **11개의 증명에 영향을 미치는 결함(proof-affecting defects)**을 식별하였다. 결정적으로, CMP 출판물은 이러한 항목 중 어느 것도 수정하지 않았다. 결함은 다음과 같이 분류된다:

• 인증서 오류 (증명에 영향을 미침):

  • 단기 계수 루프 (Short-Time Coefficient Loops): 코드 내의 잔여 계수 루프는 텍스트에서 암시된 것처럼 성분별(componentwise)이 아니며, 상단 끝점이 잘못된 하이브리드 모드로 취급되었다.
  • 피카드 곱셈 (Picard Multiplication): 부호에 민란한 피카드 곱셈의 구현은 방향성 포위(directed enclosure) 로직을 무효화하는 오류를 포함하고 있다.
  • 프로파일 경계 (Profile Bounds): 기록된 $L^\infty$ 테스트는 주장된 예산(budget)을 뒷받침하기에 5배나 너무 약하며, 이후의 예산 할당(113)은 교정된 경계로부터 도출되지 않는다.
  • 0차 모멘트 (Zeroth Moment): 0차 모멘트 계산에 유효한 꼬리 허용치(tail allowance)가 결여되어 있어, 관련 경계가 무효하다.
  • 방정식 (27) 및 직사각형 장부 정리 (Rectangular Bookkeeping): 직접적인 반례는 v2 및 CMP의 방정식 (27)이 거짓임을 보여준다. 또한, 분해에 필요한 두 개의 유한 직사각형이 코드에서 평가되지 않았으며, 커널 상한 역시 동일한 유한 간극을 공유한다.
  • 장기 재구성 (Large-Time Reconstruction): 점값 캐스케이드(point-value cascade)에서 하나의 강제 항(forcing term)이 누락되었으며, 방정식 (30)은 두 재구성 부호를 반대로 나타낸다. 또한, 코드는 꼬리 추정(tail estimate)에 필요한 지수적 할인 인자를 누락하였다.

• 인쇄된 오타 (증명에 영향을 미치지 않음):

  • 텍스트에 오류가 포함되어 있으나(예: 합계의 하한값이 틀림, 꼬리 전개에서의 계수 이름 오류, beta-tail 표기법에서의 지수 누락), 공개된 코드나 주변의 논리적 논증이 이미 올려진 의도된 버전을 사용하고 있는 경우의 불일치가 여러 건 발견되었다. 이들은 인증서 오류(C)가 아닌 오타(T)로 분류된다.

의의 및 주장
본 논문은 분석학 분야의 기발표된 컴퓨터 보조 증명에 대해, 공개된 계산 인증서 내의 다수 증명 영향 결함을 식별한 최초의 독립적, 버전 고정형, 소스 레벨 감사라고 주장한다.

• 실패의 본질: 본 결과는 의도된 정리나 그 해석적 축소(analytic reduction) 자체를 반박하는 것이 아니다. 대신, 발표된 인증서가 주장된 결론을 증명하지 못함을 입증한다. 격차는 수학적 논증을 계산 인증서로 번역하는 과정에서 발생하며, 구체적인 상수, 부호 및 도메인 범위가 잘못 처리되었다.
• CAP에 대한 시사점: 본 감사는 해석적/수치적 CAP에서 프로그램이 실행되거나 정수 산술이 내부적으로 일관됨을 확인하는 것만으로는 불충분함을 강조한다. 감사는 공식, 코드, 그리고 연속적인 대상(예: 도메인 범위, 절단, 꼬리 거동, 부호 전파) 사이의 인터페이스를 검증해야 한다.
• 향 향후 과제: 저자는 향후 작업에서 기계적 보조를 훨씬 적게 사용하는, 더 구조적으로 단순하고 교정된 증명을 제공할 것이라고 밝힌다.

결론
본 감사는 의도된 정리는 여전히 유효할 수 있으나, 논문과 함께 공개된 특정 심볼릭 인증서는 결함이 있다고 결론짓는다. 출판 과정(CMP)은 이러한 결함을 식 발견하거나 수정하는 데 실패했다. 본 논문은 CAP의 엄밀한 감사가 인쇄된 실수와 구조적 인증서 오류를 구분해야 하며, 단순한 코드 재실행이 아닌 재현 가능한 정확한 검증을 요구한다는 것을 보여주는 방법론적 시연 역할을 한다.