Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness

Motivation

• Known: 기존 수학 증명 벤치마크는 human expert evaluation이나 LLM judge를 활용해 주로 proof correctness에 집중해왔으며, 이는 LLM이 어려운 경시대회 문제를 얼마나 잘 맞히는지를 평가하는 데 초점이 맞춰져 있다.
• Gap: 최근 연구들은 증명의 가치가 formal correctness를 넘어 이해도, 동기 부여, 수학적 맥락까지 포함해야 한다고 지적하지만, 기존 벤치마크는 모든 correct proof를 동등하게 취급하며 간결성, 계산 의존도, 인지적 접근성, 다양성, 특정 기법 적용 능력 같은 proof quality 차원을 체계적으로 측정하지 못한다.
• Why: LLM이 연구 수준의 수학 문제 해결에 실질적 협력자로 활용되기 시작하면서, 단순히 정답을 맞히는 것을 넘어 명확하고 통찰력 있으며 다른 문제로 전이 가능한 증명을 생성하는 능력이 실제 유용성을 결정하기 때문에 이를 정량적으로 측정할 필요가 있다.
• Approach: 고난도 경시대회 final-answer 문제 382개를 curation하고, 각 문제에 대해 모델이 생성한 두 증명을 동일 metric 기준으로 pairwise 비교한 뒤 이를 모델 수준 rating(Elo 등)으로 집계하는 방식을 사용한다.

Achievement

Figure 2. Main results for several models.

1. PROOFRANK 벤치마크 구축: 대수, 기하, 조합론, 미적분, 정수론에 걸친 382개의 고난도 high-school-level final-answer 경시대회 문제로 구성된 최초의 proof quality 평가 벤치마크를 제시했다.
2. 5가지 scalable proxy metric 정의: conciseness, computational ease, cognitive simplicity(이상 proof-level), diversity, adaptivity(이상 problem-level)라는 다섯 가지 측정 가능한 proof quality 지표를 설계했다.
3. Pairwise 비교 및 correctness 필터링 기법: 절대 점수 산정의 어려움을 해결하기 위해 동일 문제 내에서 정답이면서 완전한 증명끼리만 pairwise 비교하여 model-level rating을 산출하는 방법론을 제시했다.
4. 프론티어 LLM 평가를 통한 실증적 발견: GPT-5.4가 accuracy와 다수 품질 지표에서 우수한 반면 GEMINI-3.1-PRO는 conciseness가 매우 낮고(3.5배 장황), QWEN3.5-397B는 낮은 accuracy에도 품질 지표가 좋으며 GLM-5는 준수한 accuracy에도 품질 지표가 낮다는, correctness와 proof quality 간의 trade-off 및 비상관성을 발견했다.

How

Figure 3. Tradeoff between accuracy and conciseness under differ-

• 382개의 challenging final-answer 경시대회 문제(대수, 기하, 조합론, 미적분, 정수론)를 curation
• final-answer 문제 선택을 통해 correctness 평가의 확장성 확보 및 full-proof judgment의 편향 회피
• 각 문제에 대해 여러 모델로부터 증명을 생성한 뒤, 두 proof가 모두 correct(정답 도달 + 완전한 justification)인 경우에만 pairwise 비교 수행
• conciseness, computational ease, cognitive simplicity는 proof-level metric으로 개별 증명 쌍을 비교
• diversity(동일 문제에 대한 여러 시도 간 접근법 다양성), adaptivity(지정된 proof technique를 따르는 능력)는 problem-level metric으로 다중 시도 전체를 평가
• pairwise 비교 결과를 집계해 모델별 rating(Elo 스타일) 산출 후 GPT-5.4, GEMINI-3.1-PRO, GLM-5, KIMI-K2.5, QWEN3.5-397B 등 프론티어 모델 비교

Originality

• correctness 중심이던 기존 수학 증명 평가 패러다임에서 벗어나 proof quality를 다차원적이고 scalable하게 정량화한 최초의 시도
• 주관적일 수밖에 없는 elegance 대신, conciseness·computational ease·cognitive simplicity·diversity·adaptivity라는 concrete하고 measurable한 proxy로 분해한 설계
• 절대 점수 대신 pairwise 비교와 rating 집계를 도입해 문제별 난이도 차이에 따른 캘리브레이션 문제를 우회
• correct proof만을 비교 대상으로 제한해 "단순하지만 틀린 증명"이 부당하게 높은 품질 점수를 받는 것을 방지하는 실용적 장치

Limitation & Further Study

• 발췌된 본문 기준으로 각 metric(특히 cognitive simplicity, diversity, adaptivity)의 구체적 산출 방식(judge 모델, 프롬프트, 신뢰도 검증)에 대한 세부 사항이 충분히 설명되지 않아 재현성과 강건성 검증이 어려움
• final-answer 문제로 한정함으로써 확장성은 얻었지만, 실제 연구 수준 수학이나 서술형 증명이 요구되는 상황에서의 일반화 가능성은 제한적일 수 있음
• LLM judge를 활용한 평가일 가능성이 높은데, 이 경우 judge 자체의 편향(sycophancy, 특정 스타일 선호)이 결과에 영향을 줄 수 있어 human validation과의 일치도 검증이 추가로 필요
• 후속 연구로는 formal proof assistant(Lean 등)와의 결합을 통한 정확성 검증과 proof quality의 동시 평가, 그리고 실제 수학자 대상 human study를 통한 metric의 타당성 검증이 필요해 보임

Evaluation

총평: Correctness 일변도의 수학 증명 평가 관행에 신선한 문제의식을 제기하며 실용적인 다차원 평가 프레임워크를 제시한 의미 있는 연구로, workshop paper로서 향후 본격적인 벤치마크 확장과 human validation이 뒤따른다면 임팩트가 클 것으로 기대된다.