Re$^2$Math: Benchmarking Theorem Retrieval in Research-Level Mathematics

Motivation

• Known: 기존 연구는 GSM8K, MATH, OlympiadBench 등 closed-world 수학 문제 해결 능력이나 miniF2F, ProofNet, PutnamBench 같은 formal proving/premise-selection 능력을 평가해왔으며, PaperQA, OpenScholar 등 문헌 기반 citation-backed QA 시스템과 NaturalProofs, TheoremQA 같은 theorem-conditioned reasoning 자료도 존재한다.
• Gap: 기존 benchmark들은 self-contained 문제에 대한 최종 답 산출이나 고정된 formal library 내 premise 검색에 집중되어 있어, open-world 문헌에서 partial research proof의 특정 gap을 해결할 수 있는 source-tool pair를 찾아내고 그 적용 가능성을 검증하는 능력은 다루지 않는다.
• Why: 실제 연구 보조 AI는 단순히 정리를 기억해서 말하는 것이 아니라 출처(provenance)를 밝히고 그 가정이 현재 증명 맥락과 부합하는지 검증해야 하므로, 이러한 tool-grounded retrieval 능력을 별도로 정밀 평가하는 것은 신뢰할 수 있는 수학 연구 보조 시스템 개발에 필수적이다.
• Approach: 주요 정리(main theorem) 증명 내 instrumental citation을 자동으로 마이닝하여 hierarchical proof context(global setup + local proof window)와 optional leakage-controlled anchor hint를 제공하고, 에이전트가 shared release-frozen retrieval artifact를 통해 검색 쿼리를 생성해 admissible source와 이를 뒷받침하는 theorem-like statement를 반환하도록 하는 citation-invariant 평가 방식을 사용한다.

Achievement

Figure 3. Dataset statistics. Overview of the curated benchmark and the Eval-200 subset. The full curated dataset contai

1. Task formulation: partial research proof에서의 tool-grounded retrieval을 hierarchical context, raw/assisted track, citation-invariant 성공 기준으로 형식화했다. 2. Living benchmark 구축: published-first, arXiv-backed 자동 파이프라인으로 instrumental proof citation 기반의 versioned benchmark를 구축하여 새 인스턴스를 지속적으로 통합하되 논문 평가는 frozen held-out release로 고정했다. 3. 진단적 평가체계 제공: ToolAcc를 주요 지표로 citation-side retrieval, source grounding, proof-gap sufficiency, oracle-source behavior, alternative-source success를 분리 측정하는 shared-backend protocol을 제시했다. 4. 실증 결과: Eval-200 test set에서 최고 성능 모델도 ToolAcc 7.0%에 그쳐, source grounding 비율은 상대적으로 높음에도 불구하고 현재 시스템들이 유효한 statement는 찾아내지만 local proof step에 대한 적용 가능성 확립에는 실패함을 보였다.

How

Figure 2. Overview of tool-grounded retrieval. Given hierarchical proof context (global + local) and an optional anchor,

• Instrumental citation 식별: main theorem 증명 내에서 외부 도구(정리, 부등식, compactness criterion 등)를 제공하는 것으로 보이는 citation을 자동 파이프라인으로 마이닝
• 각 인스턴스에 global setup과 citation 직전 local proof window로 구성된 hierarchical context 제공, assisted track에는 sanitized anchor hint 추가
• 에이전트는 shared release-frozen retrieval artifact(모델 자체 web-search/browser/deep-research 모드 아님)를 통해서만 검색 쿼리 실행 가능, 검색 인터페이스는 고정하여 mathematical source-tool policy 자체를 평가
• 성공 기준은 citation-invariant: 원저자가 인용한 source와 다르더라도 gap을 닫는 admissible source-grounded statement면 credit 부여
• ToolAcc를 주요 metric으로, citation recall/grounding/proof-gap sufficiency/oracle-source/alternative-source success를 분리하여 진단
• Appendix B에서 instrumentality 및 anchor sanitization의 구성 신호와 잔여 위험을 감사(audit)

Originality

• 기존 benchmark들이 self-contained 문제 해결이나 고정 formal library 내 premise selection에 그친 것과 달리, open-world 문헌에서 partial research proof의 특정 gap을 해결하는 source-tool pair 검색이라는 새로운 task를 제안
• citation-invariant(원저자 인용과 무관하게 admissible한 대안 source도 인정)하면서 source-grounded(반드시 실제 출처에 근거)한 이중 기준을 결합한 평가 설계가 독창적
• published-first, arXiv-backed 자동 파이프라인으로 instrumental citation을 마이닝하여 living benchmark를 구성하되, 논문 평가는 frozen release로 고정함으로써 재현성과 지속적 확장성을 동시에 확보하는 구조
• citation recall, grounding, proof-gap sufficiency를 분리하여 진단하는 세분화된 평가 프레임워크 제시

Limitation & Further Study

• instrumental citation 식별 및 anchor sanitization 과정이 완전히 자동화되어 있어 오분류(예: 실제로는 instrumental하지 않은 citation을 오인)나 leakage 위험이 존재할 수 있으며, 이는 Appendix B에서 일부 감사되었지만 근본적 해소는 아님
• 현재 모델들의 ToolAcc가 7.0%로 매우 낮아 벤치마크의 난이도가 과도하게 높거나, judge(평가자) 자체의 신뢰성(judge 모델의 판단 정확도)에 대한 추가 검증이 더 필요할 수 있음
• release-frozen retrieval artifact를 사용함으로써 모델 고유의 최신 web-search나 deep-research 능력을 온전히 반영하지 못해 실제 배포 환경에서의 성능과는 괴리가 있을 수 있음
• 후속 연구로는 benchmark 규모 확장, 다양한 수학 분야로의 일반화, judge의 편향성 감소, 그리고 실제 연구자 워크플로우와의 정합성 검증 등이 필요

Evaluation

총평: research-level 수학 연구 보조에 필수적이지만 그동안 간과되었던 tool-grounded literature retrieval 능력을 정밀하게 분해하여 진단하는 benchmark로, 낮은 ToolAcc 결과가 현재 LLM의 한계를 명확히 드러내는 의미 있는 기여이다. 다만 자동 파이프라인의 신뢰성과 judge 평가의 견고성에 대한 추가 검증이 향후 필요하다.