이론 규모의 자동 형식화(Autoformalization)를 위한 충실성 정렬

자동 형식화(Autoformalization, AF)는 컴파일을 넘어선 것을 요구합니다: 형식적 진술은 비형식적 출처의 의미를 보존해야 하며, 이는 충실성(faithfulness)으로 알려진 속성입니다. 이 속성의 자동 평가가 떠오르는 최전선이지만, 기존 방법 대부분은 진술 수준에서 작동하며 전체 항목에 대한 판결을 내릴 뿐, 개별 표현이 어떻게 대응하는지 또는 어떤 문맥적 해석이 판단을 뒷받침하는지를 밝혀내지 못합니다. 이러한 누락은 AF가 본질적으로 이론 규모(theory-scale)이기 때문에 중요합니다: 목표 진술은 주변의 수학적 자료와 명시되지 않은 관습으로부터 의미를 도출하기 때문입니다. 우리는 충실성 평가를 문맥 인식적인 정렬 후 레이블링 문제로 공식화합니다: 비형식적 진술과 형식적 진술 간의 구(phrase)-수준 대응 관계를 식별하고, 명시적으로 지정된 문맥적 해석 및 가정 하에 각각에 충실성 레이블을 할당하는 것입니다. 또한 우리는 460개의 항목과 4,982개의 주석이 달린 구-수준 링크로 구성된 최초의 이론 규모 충실성 벤치마크인 FaithAlign과, 비형식적 문맥 및 가정이 숨겨진 146개 항목으로 구성된 보조 세트인 FaithAlign-Gap을 소개합니다. 각 FaithAlign 항목에는 목표 진술 쌍, 관련 문맥, 형식적 의존성이 포함되며, 필요한 경우 주어진 해석을 명시하는 가정도 포함됩니다. 8개 모델에 걸쳐 GPT-6 Astra가 47.8%로 가장 높은 결함 F1 점수를 달성했으며, 두 개 이상의 결함을 가진 항목의 경우 단지 4.5%에서 모든 결함을 식별했습니다. FaithAlign-Gap에서는 Astra가 판정 불가능한 항목 중 28.2%만을 그렇게 식별했습니다. 이러한 결과는 문맥 의존적 대응 관계를 복구하는 것의 어려움을 보여주며, FaithAlign을 세밀하고 문맥 인식적인 충실성 평가를 위한 테스트베드로 확립합니다.