Conformal Risk Control for AI-Assisted Mathematical Derivations: A Workflow with Finite-Sample Correctness Guarantees

Motivation

• Known: conformal prediction 및 conformal risk control은 분류·회귀 문제에서 finite-sample coverage guarantee를 제공하는 것으로 잘 알려져 있으며, LLM의 self-reported confidence score는 poorly calibrated 되어 있다는 사실도 선행 연구(Kadavath et al., 2022; Xiong et al., 2024)에서 보고되었다.
• Gap: 기존에는 연구자가 LLM이 생성한 수학적 증명 단계를 전부 수동 검증하거나, 신뢰도 낮은 자기보고 confidence에 의존해 휴리스틱하게 수용하는 두 가지 방식만 존재했고, 어느 쪽도 형식적 정확성 보장(formal correctness guarantee)을 제공하지 못했다.
• Why: LLM을 활용한 수학 유도 보조가 급증하는 상황에서 중간 단계의 오류가 조용히 전파되어 전체 증명을 무효화할 수 있으므로, 인간-루프(human-in-the-loop) 검증 부담을 줄이면서도 통계적으로 보장된 오류율을 제공하는 방법은 연구 생산성과 신뢰성 모두에 실질적 영향을 미친다.
• Approach: conformal risk control 이론을 수학 증명 단계 수용/거부 결정 문제에 적용하여, 소규모 도메인별 보정 데이터셋(calibration set)으로부터 데이터 기반 임계값 τ̂(α)를 산출하고 이를 이론적으로(6개 정리)와 실증적으로(3,100개 주석 단계, 10명 연구자 대상 사용자 연구) 검증한다.

Achievement

Figure 3. Human study results (n = 10 participants, 10 tasks

1. CRC-Derive 워크플로우 제안: LLM 생성 증명 단계에 대해 score function s(z)와 conformal threshold τ̂(α)를 이용해 FAR ≤ α를 유한 표본으로 보장하는 실용적 수용/거부 절차를 설계함.
2. 6개 정리를 통한 포괄적 이론적 뒷받침: step-level FAR control(정리 3.2), Bonferroni/Šidák 기반 end-to-end 증명 합성(정리 3.3, 따름정리 3.4), 비용 기반 최적 위험 수준(정리 3.5), 비교환적(non-exchangeable) 순차 증명을 위한 online adaptation(정리 3.6), calibration sample complexity(n≥185, 정리 3.7), score 품질에 따른 efficiency ordering(정리 3.8)을 모두 증명함.
3. 대규모 실증 검증: miniF2F, ML 이론 정리, 대학원 연습문제 등 3개 도메인 3,100개 주석 단계로 구성된 데이터셋에서 4가지 score function(s1~s4)에 대해 4,000회 실험 모두에서 FAR≤α 보장이 실제로 유지됨을 확인함.
4. 인간 연구를 통한 실용성 입증: 10명의 ML 대학원생, 100개 유도 과제에서 CRC-Derive 적용 시 정답 도출 시간이 41% 감소(p=4.8×10⁻²⁹)하고 전파 오류가 77% 감소(p=5×10⁻⁴)함을 통계적으로 유의하게 보임.
5. 재현 가능한 오픈소스 패키지 공개: 코드, 프롬프트, 4가지 score function에 대한 사전 보정된 임계값을 포함한 전체 패키지를 공개하여 재현성을 확보함.

How

Figure 2. Coverage validation over 200 random splits. Left: Em-

• 증명 단계를 (목표 명제 P, 증명 맥락 C, LLM 생성 단계 H)로 구성된 인스턴스 z와 정답 레이블 S(z)∈{0,1}로 형식화함.
• 4가지 score function(자기 확신도 s1, 앙상블 합의 s2, SymPy 기반 symbolic checkability s3, Lean 4 부분 형식화 검증 s4)을 정의하고 이를 [0,1] 구간의 P(S=1) 추정치로 사용함.
• 보정 데이터셋에서 corrected empirical risk R̂+(τ)를 계산하고, 이를 α 이하로 만드는 최소 τ를 τ̂로 설정하는 conformal risk control 절차(정리 3.2)를 적용함.
• exchangeability 가정 하에 finite-sample FAR guarantee를 증명하고, Bonferroni/Šidák correction으로 다단계 증명 전체에 대한 오류 확산을 제어함.
• 비용 함수(cv, cr, ce)를 도입해 최적 α*를 결정론적으로 도출하는 decision-theoretic 분석을 수행함.
• 비교환적 순차 시나리오를 위해 online gradient-style threshold update(τ̂t)를 제안하고 시간 평균 FAR 상한을 증명함.
• miniF2F, ML 이론 정리, 대학원 연습문제 3개 소스에서 총 3,100개 단계를 전문가 annotator들의 다수결로 라벨링해 데이터셋을 구축하고, 200회의 무작위 calibration/test split(2000/1000)으로 커버리지를 검증함.
• 10명의 ML 대학원생을 대상으로 조건 A(전체 수동 검토)와 조건 B(CRC-Derive s2, α=0.10 적용) 간 비교 human study를 paired t-test로 분석함.

Originality

• LLM 기반 수학 증명 보조라는 새로운 응용 영역에 conformal risk control 프레임워크를 최초로 체계적으로 적용한 시도로 보임.
• 단일 단계 보장을 넘어 Bonferroni/Šidák correction을 통한 end-to-end 다단계 증명 합성 보장으로 확장한 점이 독창적임.
• 정적 exchangeability 가정을 완화하여 online adaptation을 통한 비교환적 순차 증명에 대한 시간 평균 FAR guarantee를 제시한 점도 이론적 기여로 평가됨.
• 비용 함수 기반 decision-theoretic 최적 위험 수준(α*) 도출 및 score function 품질에 따른 efficiency ordering 정리 등, 이론과 실무적 튜닝을 연결하는 다각적 분석 틀을 구성함.

Limitation & Further Study

• exchangeability 가정(정리 3.2~3.5)이 실제 연구자의 도메인별 증명 생성 과정에서 항상 성립하는지 검증이 부족하며, 정리 3.6의 online adaptation이 이를 완전히 대체하는지 실험적으로 충분히 입증되지 않음.
• 데이터셋(3,100개 단계)이 miniF2F, 표준 ML 이론, 대학원 연습문제 등 특정 도메인에 국한되어 있어, 더 다양하고 복잡한 최신 연구 수준의 증명에 대한 일반화 가능성이 불확실함.
• score function 중 s3(SymPy), s4(Lean 4)는 형식화 가능한 단계에만 적용 가능하여 일반적인 자연어 기반 수학적 논증 전반에 대한 적용성은 제한적일 수 있음.
• Bonferroni correction 기반 end-to-end guarantee(정리 3.3)는 단계 수 k가 커질수록 필요한 calibration sample 수(정리 3.4)가 급증하여 실용성이 떨어질 가능성이 있으며, 이에 대한 대규모 k 실험이 부재함.
• 인간 연구의 참여자 수(10명)와 과제 수(100개)가 제한적이어서 통계적으로 유의하더라도 다양한 연구 분야 및 숙련도 수준에 대한 일반화에는 한계가 있을 수 있음.
• 후속 연구로는 완전 자율 증명 탐색(autonomous proof search)과의 결합, 더 큰 도메인 다양성 확보, 그리고 exchangeability 위반이 심한 실제 연구 워크플로우에서의 강건성 검증이 필요함.

Evaluation

총평: conformal risk control을 LLM 기반 수학 증명 보조라는 실용적이고 시의적절한 문제에 적용해 이론적 엄밀성과 실증적 유효성을 모두 갖춘 견고한 연구로, 다단계 증명 합성과 온라인 적응까지 포괄하는 이론적 확장성이 돋보이나 exchangeability 가정의 실제 성립 여부와 도메인 일반화에 대한 추가 검증이 필요하다.