Agent-Based Auditing of Mathematical Proofs in Research Papers

Motivation

• Known: Lean, Coq, Isabelle/HOL, Mizar 같은 formal theorem prover는 axiom으로부터 결론이 도출됨을 절대적으로 검증할 수 있으며, LLM 기반 formal proof generation(GPT-f, Llemma, ReProver, APOLLO 등)과 agentic theorem-proving 프레임워크(ImProver, QED)들이 활발히 연구되고 있다. 또한 Gemini 기반 STOC 2026 리뷰 지원 시스템처럼 LLM을 활용한 informal 수학 리뷰 보조 도구도 등장하고 있다.
• Gap: Formal theorem prover는 informal 수학 서술을 formal language로 변환해야 하는 de Brujin factor(약 10배의 노력)로 인해 실제 연구 논문에 직접 적용하기 어렵고, 기존 LLM 기반 formal proving 시스템들은 새로운 증명을 찾는 데 초점을 맞추며 개별 정리 단위로 동작해 문서 전체 수준의 dependency 추적이 부족하다. 또한 기존 AI 보조 리뷰 시스템은 closed-source이거나 stateless query 수준에 그쳐 전체 문서에 걸친 논리적 의존성을 지속적으로 추적하지 못한다.
• Why: Peer review만으로는 수학 논문의 오류를 충분히 걸러내지 못하고 정정 논문(corrigenda) 발표율도 낮은 상황에서, formal verification 없이도 informal 논문 상태 그대로 증명의 논리적 결함과 표기 불일치를 자동으로 감지할 수 있다면 인간 저자와 AI가 생성한 수학 연구 모두의 신뢰성을 실질적으로 높일 수 있다.
• Approach: 저자들은 definitions, propositions, lemmas, theorems 간의 dependency graph를 구축하여 지역적(local) 논리 검증과 전역적(global) 일관성 분석을 결합하는 stateful agent 기반 감사 파이프라인을 제안하고, 이를 실제 오류가 존재하는 machine learning theory 논문 데이터셋으로 평가한다.

Achievement

Figure 2. Dependency graph of the mathematical proof in Pham et al. (2026) showing the hierarchical structure of assumpt

1. Agent 기반 stateful auditing 시스템 제안: 원래 LaTeX 프로젝트 파일 구조 위에서 직접 동작하며 lemma와 theorem을 감사하는 stateful assistant를 구현했다.
2. 3단계 감사 파이프라인 설계: structural mapping, local component verification, source-level error validation의 3단계로 구성되어 dependency graph 생성, atomic proof step 분해(Audit Proof table), 그리고 원본 소스 코드와의 대조 검증을 수행한다.
3. 영속적(persistent) audit artifact 생성: audit/ 디렉터리에 component별 상태를 지속적으로 기록함으로써 context window 한계를 넘는 긴 논문 처리와 반복적 human-AI 협업을 지원한다.
4. 실증적 평가: 자연 발생 증명 오류를 포함한 machine learning theory 논문 큐레이션 데이터셋에서 견고한 탐지 성능을 입증했다.

How

Figure 1. Dependency graph of mathematical components in the proof auditing pipeline. Nodes represent definitions, lemma

• Phase 1 (Structural Mapping): definitions, assumptions, lemmas, theorems을 순차적으로 인덱싱해 audit 파일을 생성하고, 중앙 error registry(error_table.md)를 초기화하며 document-level dependency graph를 Graphviz dot 파일과 prose summary로 생성. 순환 의존성이나 undefined notation 같은 전역 구조적 오류를 스캔.
• Phase 2 (Local Component Verification): dependency 순서를 따라 각 컴포넌트의 원래 증명을 (Step ID, Claim, Premises, Justification)으로 구성된 Audit Proof table로 원자적(atomic) 논리 단계로 재구성하고, assumption drift, quantifier 변화, dimension mismatch, 누락된 boundary case 등을 검사해 반증(falsification) 시도.
• Phase 3 (Error Validation): Phase 2에서 의심된 오류를 원본 LaTeX 소스와 대조해 정확한 라인 번호로 위치를 추적하고, 실제 논리적 결함인지 false positive인지 확인한 뒤 Error Index와 개별 파일에 검증 결과와 수학적 근거를 반영.
• 모든 단계의 중간 산출물을 audit/ 워크스페이스에 영속적으로 저장해 provenance tracking, 재현성, 반복적 다중 패스 정제를 지원.

Originality

• Formal theorem prover의 엄격한 formalization 요구를 우회하면서도 구조화된 dependency graph 기반 감사를 도입해 informal LaTeX 논문에 직접 적용 가능하게 한 점이 독창적이다.
• 기존 stateless query 기반 AI 리뷰 도구와 달리, persistent audit workspace를 통해 문서 전체 수준의 논리적 의존성을 추적하고 human-AI 반복 협업을 지원하는 구조를 제시했다.
• 증명을 (Step ID, Claim, Premises, Justification) 형태의 Audit Proof table로 원자적으로 분해해 암묵적 추론을 최소화하는 방법론적 기여가 있다.

Limitation & Further Study

• 워크숍 논문 발췌 내용만으로는 정량적 평가 지표(정밀도, 재현율 등)와 baseline 비교가 구체적으로 제시되지 않아 "robust detection performance"의 실질적 근거가 부족하다.
• 데이터셋이 "curated"된 machine learning theory 논문에 국한되어 있어 다른 수학 분야나 더 복잡한 증명 구조로의 일반화 가능성이 검증되지 않았다.
• False positive/negative에 대한 체계적 분석이나 사람 평가자와의 비교(inter-rater agreement) 결과가 제시되지 않아 실제 신뢰도 검증이 제한적이다.
• 후속 연구로는 더 큰 규모의 벤치마크 구축, 다양한 수학 분야 확장, formal prover와의 하이브리드 검증, 그리고 human expert와의 직접 비교 연구가 필요하다.

Evaluation

총평: Formal verification의 높은 진입장벽과 기존 AI 리뷰 도구의 stateless 한계를 동시에 극복하려는 실용적이고 시의적절한 접근으로, dependency graph 기반 구조적 감사라는 아이디어는 신선하나 워크숍 논문 특성상 정량적 검증이 아직 충분히 제시되지 않아 향후 확장된 평가가 필요하다.