골드 스탠다드 없는 추론: 자동 형식화(Autoformalization)를 위한 프록시 판사(Proxy-Judge) 이론

복잡한 추론 (Reasoning) 작업은 단일 참조 (Reference)와의 정확한 일치 (Exact match) 여부로는 정답을 판단할 수 없는 출력을 생성하는 시스템을 점점 더 많이 요구하고 있습니다. 자동 형식화 (Autoformalization, AF)가 대표적인 예입니다. 이는 모델에게 비형식적인 (Informal) 수학적 또는 논리적 추론을 형식적으로 검증 가능한 객체 (Formally checkable object)로 번역하도록 요구하지만, 전문가가 검증한 형식화 결과물은 토이 케이스 (Toy cases)를 넘어 확장하기 어렵고, 하나의 비형식적 논증은 여러 개의 유효한 형식적 표현을 가질 수 있습니다. 따라서 발전 여부는 부분적이고 구조화된 프록시 (Proxies)가 정확한 참조를 대체할 수 있는지에 달려 있습니다. 본 논문에서는 골드 스탠다드 (Gold-standard) 매칭을 축별 속성 검사 (Per-axis property checks) 벡터로 대체하는 AF를 위한 참조 없는 프록시 판사 (Reference-free proxy-judge) 프레임워크를 소개합니다. 이 프레임워크는 유도된 객체의 전역적 속성 (Global properties), 하위 구성 요소 내부의 모듈별 속성 (Per-module properties), 그리고 비형식적 소스에 다시 정렬시키는 교차 도메인 속성 (Cross-domain properties)을 다루는 세 가지 구조적 범위에 따라 프록시를 구성하며, 각 축을 평결 벡터 (Verdict vector)로 집계합니다. 이 벡터는 성찰적 정교화 루프 (Reflective refinement loop)를 구동하며, 위반된 좌표는 컨트롤러 (Controller)를 일치하는 수정 대상 (Repair target)으로 안내하므로, 각 반복 (Iteration)은 잘못되었다고 판단된 부분만을 변경합니다. 제한된 판사 노이즈 (Judge noise) 하에서, 기대되는 내재적 격차 (Expected intrinsic gap)는 노이즈에 의존하는 고원 (Plateau)까지 기하급수적으로 수축합니다. miniF2F, ProofNet, e-SNLI, 그리고 ProntoQA 상의 7개 형식화 백본 (Formalization backbones)에 대해 실험한 결과, 정교화 (Refinement)는 단일 샷 ICL (In-context learning) 베이스라인보다 통과율 (Pass Rate)을 일관되게 높였으며, 축별 프록시는 베이스라인의 개선 여지가 있는 벤치마크에서 매칭된 스칼라 프록시 (Matched scalar proxy)보다 우수한 성능을 보였습니다. 따라서 구조화된 프록시 판단은 정확한 참조를 사용할 수 없는 경우 실질적인 정교화 신호와 수렴 (Convergence)에 대한 이론적 수단을 모두 제공합니다.