ProofGrid: LLM 추론 평가를 위한 기계 검증 가능 증명 벤치마크 — 15개 태스크, 난이도 분화

Konstantine Arkoudas가 LLM 추론 능력을 최종 답변이 아닌 기계 검증 가능한 증명으로 평가하는 ProofGrid 벤치마크를 공개했습니다. 15개 태스크는 증명 작성, 검증, 마스킹, 간격 채우기로 구성되며, 간결한 자연연역 언어 NDL을 사용해 정밀하고 재현 가능한 평가가 가능합니다. 프론티어 모델들이 기초 태스크에서는 좋은 성능을 보이나, 전역 조합 추론이나 저수준 증명 합성이 필요한 어려운 태스크에서는 여전히 한계를 드러냈고, 모델이 결함 있는 증명을 생성하면서도 개별 추론은 올바르게 거절하는 인식적 불안정성도 확인되었습니다.

• #llm
• #reasoning
• #benchmark
• #proof-checking
• #ndl