LLMEval-Logic: 적대적 강화와 Z3 검증으로 검증된 중국어 논리 추론 벤치마크

대형언어모델의 논리추론은 주어진 전제에서 결론이 반드시 도출되어야 하는 규칙적 추론이다. 기존 벤치마크는 템플릿 의존성이나 불충분한 형식 주석으로 인해 실제 추론 능력을 왜곡할 수 있다. LLMEval-Logic은 현실적 시나리오를 기반으로 forward authoring과 Z3 검증, 전문가 루브릭을 결합하고, 5단계의 adversarial hardening 워크플로우를 통해 frontier 모델의 한계를 보다 명확하게 구분한다.

단계적 접근으로 NL 문제의 의미를 최대한 인간 친화적으로 구성하되, 이를 자동 검증 가능한 형식으로 변환하는 것이 핵심이다. 첫째, forward authoring으로 현실적 시나리오를 직접 작성하고, 둘째, LLM의 NL→FL 변환을 Z3 검증으로 교차 확인한다. 셋째, Rubric를 통해 형식화의 세부 요소를 개별적으로 검사하고, 넷째, Hardening 워크플로우로 아이템의 해결 공간을 의도적으로 확장/변형해 frontier 모델의 한계를 노출한다. 마지막으로 Base와 Hard 두 세트를 통해 단일질문 대비 다중질문 환경에서의 일반화 성능과 변형에 따른 민감도를 비교한다.

1. Forward Authoring, Expert Review, Normalization, Z3 Formal Verification, Rubric Construction의 5단계 파이프라인을 통해 Base 아이템을 산출한다. 2) Hardening 파이프라인에서 Decider/Proposal/Review/Answering/Verification 다섯 역할이 교대로 작동하며 6가지 전략(add_branching, add_distractor_premise, change_question_to_set_output, add_uncertainty_or_multi_answer, add_counterfactual_variant, alias_and_coreference_variation)을 적용해 Hard 아이템을 만든다. 3) 평가 프로토콜에서 LLM-as-Judge가 NL-형식화의 정합성과 아이템의 정답 여부를 판단하고, Z3 실행 결과와 Rubric 합을 함께 고려한다. 4) Base/ Hard의 항목별 평가로 각 모델의 NL 추론 능력과 NL→FL 번역의 충실도를 구분한다.

Bases에서의 Item Acc.은 평균 65.1%; Hard에서의 Item Acc.는 22.9%로 하락하며, Best Hard는 37.5%에 그친다. Z3+Rubric의 합산 성능은 Fix Symbol에서 60.16%에 도달하는 모델이 최댓치였다(Gold 100%). 14개 프런티어 모델군은 Hard 아이템에서 대규모 성능 저하를 보였고, 오류 분석을 통해 Counterfactual 재계산, 후보 공간 유지, 증거 원천 관리 등의 실패 패턴이 확인되었다. 평가 프로토콜은 3회 반복Run과 두 추가 Frontier Judge로 IAA를 확인하였으며, Inter-judge Cohen’s κ는 0.87–0.92 범위의 거의 완벽한 수준으로 재현성과 신뢰성을 확보했다.

2-6단락 구성의 연구 방법론; 4-layer Normalization(L1-L4)과 Z3 기반 형식 검증, Expert Rubrics 설계, 5단계 Hardening 워크플로우, 6가지 Hardening 전략의 구체적 조합 및 작동 원리, 평가 프로토콜의 LLM-as-Judge 운영 원칙, Z3/ Rubric의 보완적 신뢰성 분석을 포함한다.

논문은 중국어 아이템 중심으로 설계되었으며 확장 시나리오, 고차원 논리(고차/모달/확률 논리)로의 일반화가 필요하다. Z3 검증은 형식화의 타당성에 대한 보증을 제공하지만 NL 항목과 formalization의 완전한 동등성은 여전히 전문가 루브릭의 역할에 의존한다.