이 연구는 엄격한 형식화를 요구하는 전통적 정리 증명기 없이도, 비형식 과학 논문의 수학 증명을 직접 감사하는 에이전트 프레임워크를 제시한다. 정의·명제·보조정리·정리에 걸친 의존성 그래프를 구축해 논리적 간극과 숨은 가정을 잡는 국소 검증과, 표기 불일치·교차 의존 실패를 잡는 전역 일관성 분석을 함께 수행한다. 감사 결과는 구성 요소별로 지속되는 리포트로 남는다.
수학 문헌 검증은 오랫동안 사람 중심의 동료 심사에 거의 전적으로 의존해 왔다. Lean·Coq·Isabelle/HOL·Mizar 같은 형식 검증 시스템은 절대적 논리 확실성을 주지만, 비형식 수학 산문을 엄격한 형식 언어로 옮겨야 한다.
형식 증명 작성은 논문의 비형식 증명 대비 통상 약 10배의 노력을 요구한다. 학습 곡선이 가파르고, 형식 증명 과정에서 나오는 오류는 수학자에게 직관적·실행 가능한 피드백을 주지 못하는 경우가 많다. Wiedijk, 2000
순수 수학 논문조차 미묘한 모호성, 논리 비약, 명시되지 않은 가정, 대수 오류를 숨긴다. 출판된 정오표(corrigenda) 비율은 낮게 유지되어, 현행 검증 파이프라인의 결정적 공백을 드러낸다. Grcar et al., 2013
기존 비형식 감사 도구는 대개 폐쇄형이거나 상태 없는(stateless) 질의 수준 상호작용에 그쳐, 문서 전체에 걸친 논리적 의존성을 추적할 지속적 맥락 이해가 없다. 이 연구는 그 간극을 메우기 위해 상태 유지형(stateful) 대화형 에이전트 프레임워크를 제안한다.
프레임워크는 세 단계로 동작하며, 각 단계는 audit/ 작업 공간 안에 지속되는 중간 산물을 남긴다.
덕분에 논문 전체를 하나의 모델 컨텍스트 창에 담지 않고도 반복 검증이 가능하다.
정의·가정·보조정리·정리 등 모든 수학 항목을 색인해 audit/에 순차 감사 파일을 만든다. 각 파일은 원 서술·증명·전제·오류 분석 자리를 추적한다. 동시에 중앙 오류 레지스트리를 초기화하고, 문서 수준 의존성 그래프를 Graphviz dot과 산문 요약으로 내보낸 뒤 순환 의존·미정의 표기 같은 전역 구조 결함을 스캔한다.
의존성 순서를 따라 각 구성 요소를 상세 감사한다. 에이전트는 원 증명을 원자적 논리 단계의 열로 재구성해 (Step ID · Claim · Premises · Justification) 감사 증명 표에 담는다. 이때 가정 표류(assumption drift), 한정자 변경, 차원 불일치, 누락된 경계 사례를 점검해 논증을 적극적으로 반증하려 시도한다. 엄밀한 정당화가 없는 단계는 국소 경고로 기록되고 전역 레지스트리에 반영된다.
국소 검토가 끝나면 조정(reconciliation) 단계로 넘어간다. Phase 2의 의심 오류를 원본 LaTeX 소스와 교차 참조해 각 지적을 소스의 정확한 줄 번호까지 추적하고, 진짜 논리 결함인지 거짓 양성(false positive)인지 확인하거나 반박한다. 오류 색인과 개별 항목 파일을 판정으로 갱신하며, 확정 오류에는 명시적 수학적 정당화를 붙인다.
핵심 설계 원리는 상태 지속성(stateful persistence)이다. 일회성 상호작용에 의존하는 대신
결과를 구조화된 audit/ 디렉토리에 점진적으로 기록한다. 이로써 컨텍스트 한계를 넘는 긴 논문의
확장 처리, 다중 패스 정제, 출처 추적, 재현성, 사람이 읽을 수 있는 중간 추론 접근이 가능해진다.
감사 작업 공간은 증명 재구성 아카이브·오류 추적기·의존성 그래프·구조화된 검토 기록을 겸한다.
| ID | Claim | Premises | Justification |
|---|---|---|---|
| S1 | x>0에서 f(x) ≥ 0 | 보조정리 2, f의 정의 | 보조정리 2가 정의된 f에 직접 적용 |
| S2 | a > 0, b > a | 정리 T1의 가정 | 정리의 가정을 명시적으로 재진술 |
| S3 | ∫ₐᵇ f(x)dx ≥ 0 | S1, S2, 적분의 선형성 | [a, b]에서 양변을 적분 |
알려진 수학 오류를 담은 monotone deep equilibrium model 수렴률 논문 초안을 테스트베드로 삼았다. 기억(memorization) 우려를 완화하면서도 현실적이고 도전적인 검증 대상이 된다. 탐지된 25개 중 23개(92%)가 수동 검증에서 유효로 확인됐다. 아래 버튼으로 심각도를 필터링할 수 있다.
각 사례는 원 서술의 문제 지점(강조)과 에이전트가 생성한 오류 설명을 함께 보여준다. 설명은 연구자가 증명을 정제하는 데 쓸 수 있는 실행 가능한 피드백을 제공한다.
그러나 W는 반대칭 부분 B − Bᵀ를 가지므로 I − W는 비대칭이다. 의도된 조건은 대칭화된 연산자 강단조성(operator strong-monotonicity)이다. PSD 표기와 실제 의도가 어긋난다.
경계값 α = 2m/L² 에서는 L[Tα] ≤ 1 이지만 엄격하게 < 1 은 아니다. 따라서 닫힌 구간 끝점에서 수축성이 보장되지 않는다. 반개구간이어야 한다.
거짓이다. Π = [J + µ(I − J)]⁻¹ 는 Πᵢᵢ = 1/[Jᵢᵢ + µ(1−Jᵢᵢ)] 이다. ReLU의 비활성 좌표에서 Jᵢᵢ = 0 이므로 Πᵢᵢ = 1/µ → ∞. Π의 노름은 비활성 좌표를 따라 발산하므로 극한에서 "∥Π∥ ≤ 1"은 수학적으로 틀렸다.
G가 최대 단조(maximally monotone)임을 검증하지 않았다. 따라서 Rɢ의 확고한 비확장성(firm non-expansiveness)이 정당화되지 않는다. 주 결과의 그래디언트 상한 유도에 쓰이는 결정적 보조정리라 파급이 크다.
Lean·Coq 같은 형식 검증기는 논리 이탈을 모두 커널 수준 오류로 취급하지만, 사람이 쓴 LaTeX 논문은 표면적 표기 실수부터 근본적 논리 붕괴까지 스펙트럼을 갖는다. Brent(2021)의 분류를 참고해 파이프라인이 탐지하도록 설계된 범주는 다음과 같다.
잘못된 아래첨자, 변수 교환, 깨진 내부 상호참조 등 표기의 표면적 오류. "사소"하게 여겨지지만 검증 경로를 크게 흐린다.
부호 오류부터 행렬 미적분 실패까지 계산의 기계적 실패. 알고리즘 구현 오류나 수치적으로 불안정한 근사 의존을 포함한다.
모든 경우·거동·경계 조건을 고려하지 않아 증명이 불완전해진다.
푸앵카레가 삼체 문제에서 카오스 거동을 초기에 누락한 사례.
수학적 조건을 명시적 정당화 없이 가정해, 주장한 정의역의 특정 부분집합에서만 성립하는 증명이 된다.
ζ(s)의 ℜ(s)>1 성질을 임계 대역에도 적용한 다수의 리만 가설 시도.
주장된 함의가 자명하지 않고 본문에 없는 중간 보조정리를 요구하는 논리 비약.
닉 카츠가 발견한 와일즈의 1993년 페르마 마지막 정리 증명의 간극.
유효한 정리를 전제가 충족되지 않는 맥락에서 쓰거나, 출처와 현 연구 사이 정의가 미묘히 다를 때 발생한다.
에르되시가 1960년 논문에서 적용 범위 밖으로 결과를 쓴 사례.
이전 심사 논문의 틀린 결과를 물려받아, 현 연구의 유효성이 결함 있는 토대에 전적으로 의존하는 "오류 트리"가 생긴다.
틀린 정리에 의존해 일반화 리만 가설 증명을 잘못 주장한 사례.
개념적으로는 타당해도 모호한 표기, 누락된 단계, 손짓 같은(hand-wavy) 전이로 형식 검증을 불가능하게 만든다.
난해한 표기로 논란이 이어진 모치즈키의 abc 추측 주장.
감사 파이프라인은 Claude Code(Claude Opus 4.7 기반) 위에서 구현되어 LaTeX 소스 디렉토리에 직접 실행된다.
아래는 재현을 위해 제공된 SKILL.md의 디스패치 규칙이다. 저장소 상태와 인자에 따라 실행할
단계가 결정된다.
이 작업은 비형식 LaTeX 증명을 감사하는 에이전트 프레임워크로 수학·이론 기계학습 연구의 신뢰성을 높이는 것을 지향한다. 잠재적 이점과 한계는 다음과 같다.
구조화된 증명 표현과 지속되는 감사 산물로 사람 심사를 보강한다.
증명 재구성 아카이브가 학습·검토 도구로 기능한다.
탐지 결과가 항상 옳지는 않다. 25개 중 2개는 오탐(False Alarm)으로 확인됐다.
충분한 사람 감독 없이 자동 검증에만 의존하는 것은 위험하다. 최종 판단은 연구자의 몫이다.
"오류를 바로잡는 일이 흥미로운 수학으로 이어질 수 있다."
— Richard P. Brent
에이전트 기반 구조적 감사는 사람이 쓴 증명과 기계가 생성한 증명 모두의 신뢰성을 높이는 매우 유망한 방향이다. 감사 산물은 공개 저장소에 지속된다.
github.com/NNHieu/math_auditing_examples