기술 요약: 한 번 정형화하고 나머지는 편집하라 (BASE)

1. 문제 정의

대규모 언어 모델(LLM)이 수학적 추론에 점점 더 많이 적용됨에 따라, 단일 문제에 대해 여러 개의 서로 다른 추론 경로와 후보 답안을 생성하는 경우가 많아지고 있습니다. 여기서 발생하는 핵심적인 과제는 **답안 선택(answer selection)**입니다. 즉, 테스트 타임 스케일링(test-time scaling) 중에 정답 라벨에 접근할 수 없는 상태에서 어떤 후보가 정답인지 어떻게 검증할 것인가 하는 문제입니다.

다수결 투표(majority voting)나 학습된 보상 모델(learned reward models)과 같은 기존 방식은 통계적 신호를 제공하지만, 형식적 보증(formal guarantees)은 부족합니다. 최근 연구들은 형식적 증명 보조 도구(특히 Lean 4)를 활용하여 후보들을 검증하는 방식을 활용해 왔습니다. 이 패러다임에서 "오토포멀라이저(autoformalizer)"는 문제와 후보 답안을 정답의 정당성을 단언하는 Lean 정리 문장으로 변환합니다. 그러면 증명기(prover)가 이 문장을 검증하려고 시도합니다.

그러나 중요한 병목 현상이 존재합니다. $K$개의 후보 답안을 검증하기 위해 오토포멀라이저를 $K$번 독립적으로 호출해야 한다는 점입니다. 이는 샘플 수에 따라 선형적으로 증가하는 $\Theta(K)$의 계산 비용을 발생시킵니다. 저자들은 단일 문제에 대해 $K$개의 형식적 문장들이 문제 구조를 공유하며 답안 표현식만 다를 뿐 거의 동일하다는 점에 주목했습니다. 핵심 문제는 선택 정확도를 희생하지 않으면서, 정형화 비용을 $\Theta(K)$에서 $\Theta(1)$로 줄이기 위해 이 공유된 구조를 어떻게 활용할 것인가 하는 것입니다.

2. 방법론: BASE 파이프라인

저자들은 하나의 "베이스(base)" 후보를 정형화하고 나머지 $K-1$개의 문장은 국소적 편집을 통해 유도하는 파이프라인인 BASE(Base-and-Substitute-Edit)를 제안합니다.

2.1 베이스 발견 (Base Discovery)

파이프라인은 상위 솔버가 신뢰도 순으로 정렬된 $K$개의 후보 답안 리스트 $S(x) = (a_1, \dots, a_K)$를 생성하는 것으로 시작됩니다.

• 시스템은 순위 순서대로 후보들을 순회합니다.
• 각 후보 $a_i$에 대해, 문제-답안 쌍 $(x, a_i)$를 Lean 문장 $F_i$로 정형화하려고 시도합니다.
• Lean에서 성공적으로 **타입 체크(type-checks)**되는 첫 번째 후보 $a_b$를 찾으면 프로세스를 중단합니다.
• $F_b$는 **베이스 정형화(base formalization)**가 되고, $a_b$는 **베이스 답안(base answer)**이 됩니다.
• 만약 어떤 후보도 타입 체크에 성공하지 못하면, 시스템은 가장 순위가 높은 첫 번째 후보 $a_1$으로 회귀(fallback)합니다.

2.2 치환 캐스케이드 (Substitution Cascade)

유효한 베이스 $F_b$가 확립되면, 시스템은 다른 후보들을 반영하기 위해 $F_b$를 제자리에서 편집하여 나머지 $K-1$개의 문장을 생성합니다. 이는 두 단계의 캐스케이드로 처리됩니다.

1. Tier 1 (R1): 규칙 기반 직접 국소화 (Rule-Based Direct Localization)

   • 시스템은 "게이트 영역"(주석/헤더를 제외한 정리 본문) 내에서 정확한 문자열 매칭을 통해 답안 표현을 찾으려고 시도합니다.
   • 고유한 매치(unique match)가 발견되면, 시스템은 답안 문자열의 직접적인 치환을 수행합니다.
   • 매치가 여러 개 발견되면, 작은 모호성 해소 모델(disambiguation model)이 올바른 슬롯을 선택합니다.
   • 이 단계는 효율적이지만, 오토포멀라이저가 답안을 단순 문자열이 아닌 다양한 구문적 형태(예: 별도의 바인딩으로 인코딩된 튜플 (3, 5) 또는 Prod 값)로 인코딩할 경우 실패합니다.

2. Tier 2 (R2): LEANSCRIBE (학습된 재작성기)

   • R1이 실패하는 경우, 시스템은 특화된 미세 조정 LLM인 LEANSCRIBE를 호출합니다.
   • 입력: 문제 $x$, 베이스 정형화 $F_b$, 베이스 답안 $a_b$.
   • 출력:
     • 로컬 블록 $s$: 답안 의존적 표현을 포함하는 $F_b$의 연속된 세그먼트.
     • 채우기 함수 $f$: 임의의 비형식적 답안 $a_i$를 대응하는 Lean 표현식으로 매핑하여 $s$를 대체하는 경량 파이썬 함수.
   • 실행: LEANSCRIBE는 문제당 단 한 번 실행됩니다. 생성된 함수 $f$는 나머지 모든 후보 $a_i$에 적용되어 $F_i = f(a_i)$ 형태의 형식적 문장을 생성합니다. 이를 통해 모델 호출 비용을 $K-1$개의 후보 전체에 걸쳐 분담(amortize)합니다.

2.3 검증 및 선택 (Verification and Selection)

파이프라인은 주요 선택 신호로 **문장 수준의 타입 체크(statement-level type-checking)**에 의존합니다.

• 후보의 형식적 문장 $F_i$가 Lean에서 타입 체크되면(즉, 잘 형성된 명제이면) "검증된" 것으로 간주합니다.
• 시스템은 타입 체크를 통과하는 가장 높은 순위의 후보 $a_j$를 선택합니다.
• 만약 어떤 후보도 타입 체크를 통과하지 못하면, 가장 순위가 높은 후보 $a_1$을 선택합니다.
• 저자들은 증명 수준의 검증(증명기를 실행하는 것)이 더 엄격하지만, 현재의 증명기들은 낮은 pass@1 비율을 보이므로, 예산이 제한된 환경에서는 문장 수준의 타입 체크가 선택을 위한 더 실용적인 신호라고 언급합니다.

3. 주요 기여

1. BASE 파이프라인: 단일 검증된 베이스 문장을 여러 후보와 공유함으로써 정형화 비용을 $\Theta(K)$에서 $\Theta(1)$로 줄이는 최초의 연구입니다.
2. LEANSCRIBE 모델: 답안 의존적 블록을 국소화하고 재사용 가능한 편집 함수를 생성하도록 학습된 전문 재작성기로, 규칙 기반 치환이 처리할 수 없는 다양한 구문적 변형을 처리합니다.
3. 파레토 개선 (Pareto Improvement): 이 방법은 모든 테스트 구성에서 계산 비용을 크게 줄이면서도 더 높은 선택 정확도를 달ach합니다.

4. 실험 결과

저자들은 네 가지 벤치마크(MATH-500, OlympiadBench, AMC-AIMO, AIME 2024)에서 세 가지 서로 다른 상위 솔버(Gemini 3 Pro, Qwen3-8B, DeepSeek-R1-Qwen3-8B)와 $K=8$개의 후보를 사용하여 BASE를 평가했습니다.

• 정확도: BASE는 독립적인 정형화 방식과 비교하여 12개(데이터셋, 솔버)의 모든 구성에서 선택 정확도(Acc)를 개선했으며, 향상 폭은 +0.7에서 +23.3 퍼센트 포인트에 달했습니다.
• 강건성: "골드 답안 통과(Gold-Answer Pass)"율(정답의 문장이 타입 체크되는 비율인 GT-pass)이 크게 증가하여(최대 +33.3 포인트), 많은 경우 96~100%에 도달했습니다. 이는 검증된 베이스를 공유하는 것이 정답의 정형화를 더 견고하게 만든다는 것을 나타냅니다.
• 비용 효율성: $K=8$일 때, BASE는 오토포멀라이저 호출 횟수를 약 5.4배(평균 감소폭 4.7~6.5배) 줄였습니다. 비용은 $\Theta(K)$가 아닌 $\Theta(1)$로 스케일링됩니다.
• 절제 실험 (Ablation): 학습된 재작성기(LEANSCRIBE)를 제거하고 규칙 기반 치환(R1)에만 의존했을 때 후보 커버리지가 크게 감소(8~22 퍼센트 포인트)하였으며, 이는 다양한 구문 인코딩을 처리하기 위한 학습된 컴포넌트의 필요성을 입증합니다.
• 증명 수준 분석: 단일 시도당 하나의 후보를 사용하는 증명기(DeepSeek-Prover-V2)를 사용하더라도, BASE는 12개 구성 중 11개에서 증명 수준의 정확도를 개선했습니다. 이는 더 잘 구조화된 형식적 문장이 다운스트림 증명기에 도움이 된다는 것을 시사합니다.

5. 의의 및 주장

본 논문은 BASE가 Lean 기반 답안 선택을 위한 파레토 개선을 나타낸다고 주장합니다. 한 번 정형화하고 나머지를 편집함으로써, 이 방법은 동시에 다음을 달성합니다:

• 비용 절감: 형식적 검증의 추론 비용을 획기적으로 낮추어, 큰 $K$를 가진 테스트 타임 스케일링을 더 실현 가능하게 만듭니다.
• 정확도 향 향상: 공유된 베이스 구조가 오토포멀라이저의 변동성과 실패율을 줄여주기 때문에, 정답을 선택하는 신뢰성을 높입니다.

저자들은 이 접근 방식이 기존 파이프라인(FANS 파이프라인에 통합되어 입증됨)에서 정형화 단계를 대체하는 "드롭인 교체(drop-in replacement)"임을 강조하며, 이러한 이득이 상위 솔버의 생성 변화가 아니라 검증기가 공유된 검증 스캐폴드를 사용할 때 올바른 답안을 더 효과적으로 유지하는 능력에서 기인한다고 설명합니다.

이 연구는 현재의 증명기 한계로 인해 문장 수준의 타입 체크에 집중하고 있으며, 후보 답안들이 문제 측면의 구조를 공유한다고 가정한다는 점을 명시하며 한계를 인정합니다. 또한, 잘못된 답안이 여전히 타입 체크될 수 있는 오토포멀라이션의 충실성(faithfulness) 문제를 해결한다고 주장하지는 않지만, 솔버의 순위와 형식적 신호를 결려함으로써 이러한 위험을 완화할 수 있다고 제안합니다.