Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance

Motivation

• Known: 기존 연구들은 coding agent를 활용해 mathlib에 이미 잘 정리된 수학 분야(예: 대수적 조합론, 해석학)의 교재 전체를 Lean 4로 formalize하는 데 성공했으며, 그 성공 여부를 오로지 kernel acceptance(컴파일 및 sorry 없음)로만 측정해왔다.
• Gap: 첫째, 기존 연구는 mathlib에 이미 잘 구축된 분야에 편중되어 있어 agent가 새로운 이론을 처음부터 구축해야 하는 상황에서의 능력이 검증되지 않았다. 둘째, kernel acceptance는 formalization이 well-formed하고 컴파일된다는 것만을 보장할 뿐 statement가 원문을 충실히 반영하는지, vacuous하거나 quantifier scope를 잘못 해석했는지 등 semantic correctness를 전혀 보장하지 않으며, 기존 whole-textbook 연구들은 이런 품질을 제한적이고 주관적인 spot-check로만 평가해왔다.
• Why: Lean/mathlib 기반 대규모 autoformalization이 실제 연구 수준 수학 지식 검증의 실용적 기반이 되려면, 단순 컴파일 성공을 넘어 formalization이 실제로 원문 수학을 신뢰성 있게 표현하는지 검증하는 방법론이 필수적이며, 이는 향후 autoformalization 시스템 평가의 신뢰도를 크게 좌우한다.
• Approach: Claude Opus/Sonnet 기반 Planner-Worker-Evaluator-Consultant 역할을 GitHub Actions로 조율하는 자율 루프형 coding agent 파이프라인을 구축해 수치해석 교재를 formalize하고, 이를 자체 및 RepoProver, M2F의 결과물에 대해 LLM-as-judge 기반 3차원 품질 감사 프레임워크로 평가한다.

Achievement

Figure 3. LOC vs active compute time.

1. 새로운 도메인으로의 확장: mathlib에 거의 존재하지 않는 수치해석학(상미분방정식의 수치해법) 교재를 대상으로 coding agent formalization을 수행하여, agent가 기존 라이브러리를 검색·재사용하는 것이 아니라 새로운 이론을 처음부터 구축하는 능력을 스트레스 테스트했다.
2. 3차원 품질 평가 프레임워크 제시: semantic correctness, mathlib reuse, cross-file reuse라는 세 축으로 구성된 체계적이고 재현 가능한 LLM-as-judge 기반 감사 방법론을 도입했다.
3. kernel acceptance의 한계 실증: 자체 formalization과 RepoProver, M2F의 공개 결과물에 이 프레임워크를 적용해, 불완전한 다부분 statement, 추가된 약화 가정(weakening hypotheses), 파라미터 제한 등 반복적으로 나타나는 불충실한 formalization 패턴을 발견함으로써 kernel acceptance 기반 지표가 formalization 품질을 상당히 과대평가함을 보였다.

How

• Python orchestrator가 매 cycle마다 Planner, Worker, Evaluator, (필요시) Consultant 네 가지 LLM 역할을 반복 호출하는 stateless agent 구조를 사용하며, 모든 cycle 간 통신은 저장소에 커밋된 파일(strategy.md, task_results, issues, history.jsonl 등)과 GitHub Actions를 통해서만 이루어진다.
• Planner/Worker는 Claude Opus 4.6, Evaluator는 Claude Sonnet으로 구현되며, RepoProver의 sketcher/prover/reviewer 구조나 M2F의 고정된 2단계(statement→proof) 파이프라인과 달리, 매 cycle 저장소의 현재 상태에서 목표를 동적으로 선택하는 개방형 루프를 사용한다.
• 매 cycle은 Synchronization(빌드 상태 확인 및 우선 수정), Planning(전략 수립), Execution(Worker가 sorry-first 전략으로 정리를 완성하며 LeanSearch, Loogle 등 Mathlib 검색 도구 활용), Evaluation(Evaluator의 구조화된 평가) 단계로 진행된다.
• 완성된 코드를 대상으로 자동화된 코드 분석과 LLM-as-judge를 결합해 semantic correctness(원문 충실성), mathlib reuse(기존 mathlib 결과 재사용 여부), cross-file reuse(프로젝트 내 이미 formalize된 결과의 재사용 여부)를 감사한다.

Originality

• mathlib에 거의 없는 수치해석 분야를 대상으로 한 최초의 project-scale coding agent formalization 시도로, 기존 연구들이 다루지 않은 "새 이론 구축" 상황을 다룬다.
• kernel acceptance를 넘어선 품질 평가를 개별 statement 단위가 아닌 project 전체 스케일에서, 그리고 mathlib reuse·cross-file reuse라는 구조적 차원을 새롭게 도입해 라이브러리·프로젝트 통합성까지 평가하는 점이 기존 LLM-as-judge 기반 평가 연구와 차별화된다.
• 자체 결과뿐 아니라 RepoProver, M2F 등 공개된 타 연구 결과물에도 동일한 감사 프레임워크를 적용해 비교·검증하는 재현 가능한 방법론을 제시한다.

Limitation & Further Study

• 발췌된 본문에서는 LLM-as-judge의 구체적 프롬프트, 채점 기준, 인간 평가와의 일치도(agreement) 검증 등이 충분히 제시되지 않아 평가 프레임워크 자체의 신뢰성 검증이 부족해 보인다.
• 단일 교재(수치해석 ODE)에 대한 사례 연구로, 다른 미커버 분야로의 일반화 가능성은 추가 검증이 필요하다.
• Claude Opus/Sonnet이라는 특정 모델 조합에 의존한 파이프라인이라 다른 LLM 백본에서의 재현성과 견고성은 불명확하다.
• 후속 연구로 다양한 미커버 수학 분야에 대한 확장 적용, 자동화된 semantic correctness 판정의 정밀도 개선, 그리고 인간 전문가 평가와의 상관관계 분석이 필요해 보인다.

Evaluation

총평: autoformalization 연구가 컴파일 성공 여부에만 의존해온 관행에 정면으로 문제를 제기하고, mathlib 미커버 영역과 구조적 품질 차원을 함께 다룬 실용적이고 시의적절한 기여이나, 평가 프레임워크의 엄밀성 검증이 더 보강되면 좋을 것이다.