Guoxin Chen Jing Wu Xinjie Chen Wayne Xin Zhao Ruihua Song Chengxi Li Kai Fan Dayiheng Liu Minpeng Liao

초록

자연어로 표현된 수학 문제를 기계 검증 가능한 형식적 문장으로 변환하는 '자동형식화(autoformalization)'는 자연어로 제시된 수학 문제를 형식적 수학 추론을 통해 해결하는 데 핵심적인 역할을 한다. 대규모 언어 모델(Large Language Models, LLM)은 문법적으로 올바른 형식적 문장을 생성할 수는 있지만, 원래 문제의 의미적 의도를 정확히 보존하지 못하는 경우가 많다. 이 한계는 LLM 기반 접근 방식이 자동형식화를 단순한 번역 작업으로 간주하기 때문이며, 인간 전문가들이 자연스럽게 사용하는 자기 반성과 반복적 보완의 메커니즘이 부족하기 때문이다. 이러한 문제를 해결하기 위해, 본 연구는 의미 일관성 평가를 자동형식화 과정에 밀접하게 통합한 'ReForm'(Reflective Autoformalization)을 제안한다. 이 방법은 모델이 형식적 문장을 반복적으로 생성하고, 생성된 문장의 의미적 정확성을 평가하며, 식별된 오류를 점진적 보완을 통해 자가 수정할 수 있도록 한다. 이러한 반성적 모델을 효과적으로 훈련하기 위해, 시퀀스 내 각 위치에 다른 보상 값을 부여하는 '전망 기반 제한 시퀀스 최적화(Prospective Bounded Sequence Optimization, PBSO)'를 도입한다. 이는 모델이 정확한 자동형식화와 올바른 의미 검증 능력을 동시에 개발하도록 하여, 반성의 목적을 훼손할 수 있는 표면적 평가를 방지한다. 네 개의 자동형식화 벤치마크에서 실시한 광범위한 실험 결과, ReForm은 가장 강력한 기준 모델 대비 평균 17.2%의 성능 향상을 달성했다. 평가의 신뢰성을 further 확보하기 위해, 859개의 전문가 주석이 달린 항목을 포함하는 'ConsistencyCheck'를 제안한다. 이 벤치마크는 LLM이 심사관으로서의 유효성을 검증하는 동시에, 자동형식화가 본질적으로 어려운 과제임을 드러낸다. 실제로 인간 전문가조차도 38.5%의 경우에서 의미 오류를 범하는 것으로 나타났다.