Agentified Assessment of Logical Reasoning Agents

이 논문은 실행 재현성, 감사 가능성, 그리고 실패 견고성을 보장하는 '에이전트화된 평가 (Agentified Assessment)' 프레임워크를 제시하고, 이를 적용하여 FOLIO 데이터셋에서 자동 형식화 에이전트가 체인 오브 씽킹 (Chain-of-Thought) 기반선보다 높은 정확도 (86.70% 대 73.89%) 를 달성함을 입증했습니다.

핵심

🎓 1. 문제: 기존 시험 방식의 한계

기존에 AI 를 평가할 때는 마치 선생님이 직접 채점지를 들고 학생의 답안을 일일이 확인하는 방식이었습니다.

• 문제점: 학생이 답을 쓰다가 펜이 고장 나거나 (실행 오류), 시간이 부족하거나 (타임아웃), 글씨를 못 읽게 썼을 때 (파싱 오류), 이를 '논리 실수'와 구별하지 못해 점수를 깎거나 아예 시험을 무효 처리했습니다. 또한, 시험 문제마다 채점 방식을 다시 짜야 해서 매우 번거로웠습니다.

🕵️ 2. 해결책: "심사위원 AI"를 도입하다 (Agentified Assessment)

이 논문은 **"심사위원 AI (Assessor Agent)"**라는 새로운 캐릭터를 등장시킵니다.

• 비유: 이제 시험은 **학생 (테스트받는 AI)**과 심사위원 AI가 서로 대화하며 진행됩니다.
  • 학생 AI: 문제만 받고 답을 냅니다. (내부 방식은 자유!)
  • 심사위원 AI: 학생에게 문제를 주고, "시간은 60 초만 줘!", "답이 안 보이면 '오류'로 기록해!", "논리적으로 맞는지 확인해!"라고 지시합니다.
• 장점: 학생 AI 는 심사위원 AI 와만 대화하는 규칙 (표준 인터페이스) 하나만 지키면 됩니다. 시험 문제가 바뀌어도 학생은 그대로고, 심사위원만 바뀌면 되므로 훨씬 효율적입니다.

🧹 3. 데이터 청소: "오류가 있는 문제지"를 고치기

연구팀은 논리 추론 테스트용 데이터 (FOLIO) 를 사용했는데, 원래 데이터에 오타나 논리적 모순이 섞여 있었습니다.

• 비유: 마치 수학 문제집에 답이 틀린 문제나 문제 자체가 모호한 문제가 섞여 있는 상황입니다.
• 해결: 연구팀은 **수학 선생님 (Vampire 증명기)**과 수정 전문가 AI를 투입해 문제집을 꼼꼼히 검수했습니다.
  • 논리적으로 말이 안 되는 문제는 고치고, 답이 명확하지 않은 문제는 '불확실 (Uncertain)'로 분류했습니다.
  • 이렇게 깨끗하게 다듬어진 문제집을 만들어서 시험을 치르게 했습니다.

🤖 4. 실험: 두 명의 학생 대결

깨끗해진 문제집으로 두 명의 AI 학생을 시험시켰습니다.

1. 학생 A (기존 방식, Chain-of-Thought):

   • 방식: "생각해 봐, A 라면 B 고, B 라면 C 지... 그러니까 답은 C 야!"라고 글로 써가며 추론합니다.
   • 결과: 73.89% 점수. (논리적으로 헷갈리면 틀리기 쉬움)

2. 학생 B (새로운 방식, Auto-formalization):

   • 방식: 문제를 **수학 공식 (Z3Py 코드)**으로 번역한 뒤, 컴퓨터가 직접 계산하게 합니다. "A+B=C 인가? 컴퓨터가 계산해!"
   • 결과: 86.70% 점수. (특히 '거짓'인 경우를 찾아내는 능력이 월등히 뛰어남)

💡 5. 핵심 결론

• 왜 학생 B 가 이겼을까?
  • 학생 A 는 글로 생각하다 보면 헷갈릴 수 있지만, 학생 B 는 컴퓨터가 직접 계산하므로 실수가 거의 없습니다. 특히 "이 말은 거짓이다"라는 것을 증명할 때 훨씬 강력했습니다.
• 이 연구의 의미:
  • AI 를 평가할 때 실행 오류와 논리 오류를 명확히 구분할 수 있는 시스템을 만들었습니다.
  • 앞으로는 AI 가 복잡한 도구를 사용할 때도, 심사위원 AI가 규칙만 지키면 누구든 공평하게 시험을 볼 수 있는 길이 열렸습니다.

🌟 한 줄 요약

"AI 의 논리력을 시험할 때, '심사위원 AI'가 실행 오류와 논리 실수를 구분해 주고, '컴퓨터 계산'을 활용한 학생이 글로만 생각한 학생보다 훨씬 잘한다는 것을 증명했습니다."

기술 요약

1. 연구 배경 및 문제 제기 (Problem)

기존의 논리적 추론 에이전트 평가 방식은 다음과 같은 한계를 가지고 있습니다:

• 실패 모드의 혼재: 모델의 추론 오류와 도구의 실행 오류 (타임아웃, 런타임 에러, 출력 파싱 실패 등) 를 구분하지 못해 단일 정확도 수치 뒤에 숨겨져 있습니다.
• 평가 인프라의 결합도 (Coupling): 기존 벤치마크는 특정 에이전트 구현과 평가 로직이 강하게 결합되어 있어, 새로운 벤치마크를 추가할 때마다 통합 비용이 기하급수적으로 증가합니다.
• 재현성 부족: 평가 과정이 재현 가능하고 감사 가능하며, 실행 실패에 강건하지 못합니다.

이러한 문제를 해결하기 위해 저자들은 에이전트 기반 평가 (Agentified Assessment) 프레임워크를 제안하며, 평가 자체를 하나의 '에이전트'로 모델링합니다.

2. 방법론 (Methodology)

가. 에이전트 기반 평가 프레임워크 (Agentified Assessment)

• 핵심 개념: 정적인 평가 스크립트 대신 평가자 에이전트 (Assessor Agent) 를 도입합니다.
• 구조:
  • 평가 대상 에이전트 (Agent under Test): 추론을 수행하며 표준화된 에이전트 간 (A2A) 인터페이스만 노출하면 됩니다.
  • 평가자 에이전트 (Assessor Agent): 작업 발행, 실행 예산 (타임아웃 등) 강제, 출력 파싱, 구조화된 실패 유형 기록, 점수 부여를 담당합니다.
• 장점: 에이전트가 A2A 인터페이스를 한 번만 구현하면 다양한 평가자 에이전트와 호환될 수 있어 (O(1) 통합 비용), 플러그 앤 플레이 평가와 아키텍처의 자유도를 보장합니다.

나. 데이터 정제 파이프라인 (Data Cleaning Pipeline)

• 대상 데이터셋: FOLIO (자연어 전제와 결론, 그리고 형식 논리 (FOL) 주석이 포함된 1 차 논리 추론 벤치마크).
• 문제점: 원본 데이터셋은 의미 분석의 복잡성으로 인해 자연어와 형식 주석 간의 불일치 및 레이블 오류가 존재합니다.
• 정제 과정:
  1. 형식 검증: Vampire 정리 증명기를 사용하여 전제와 결론 간의 함의 관계를 검증합니다.
  2. 불일치 식별 및 수정: 검증 결과가 기대 레이블과 다를 경우, 두 개의 LLM 기반 에이전트 (비판 에이전트와 수정 에이전트) 를 통해 번역 오류 (괄호 불균형, 오타 등) 를 식별하고 수정합니다.
  3. 수동 검토: 자동 수정이 실패하는 경우 인간 전문가가 검토합니다.
• 결과: 검증된 데이터셋 (Cleaned FOLIO) 을 구축하여 평가의 신뢰성을 높였습니다.

다. 평가 대상 에이전트 (Reasoning Agents)

두 가지 에이전트를 동일한 평가자 하에서 비교했습니다:

1. Chain-of-Thought (CoT) Baseline: 단계별 추론을 수행한 후 최종 답을 출력하는 프롬프트 기반 에이전트.
2. Auto-formalization Agent (제안 모델):
   • 1 단계 (코드 생성): 자연어 전제와 결론을 실행 가능한 Z3Py(SMT 솔버용 Python 라이브러리) 코드로 변환합니다.
   • 2 단계 (실행 및 검증): 생성된 코드를 샌드박스 환경에서 실행하여 만족도 (Satisfiability) 를 확인합니다.
     • 전제 $\land$ $\neg$결론이 불만족 (Unsatisfiable) 이면 TRUE.
     • 전제 $\land$ 결론이 불만족이면 FALSE.
     • 그 외는 UNCERTAIN.
   • 자기 수정 루프: 실행 중 구문 오류 등이 발생하면 에러 메시지를 분석하여 코드를 수정하고 재시도합니다 (최대 3 회).

3. 주요 기여 (Key Contributions)

1. 에이전트 기반 평가 (AAA) 프레임워크 도입: 평가 로직을 에이전트화하여 실행 오류와 추론 오류를 분리하고, 구조화된 실패 데이터를 기록하는 재현 가능한 평가 시스템을 제시했습니다.
2. 신뢰할 수 있는 FOL 벤치마크 구축: FOLIO 데이터셋에 대한 체계적인 검증 및 수정 파이프라인을 적용하여, 레이블 오류를 보정하고 자연어 - 형식 논리 정렬을 개선한 데이터셋을 공개했습니다.
3. 솔버 기반 추론의 유효성 입증: 자동 형식화 (Auto-formalization) 에이전트가 CoT 기반 접근법보다 논리적 추론, 특히 모순 (FALSE) 과 불확실성 (UNCERTAIN) 처리에서 우수한 성능을 보임을 실증했습니다.

4. 실험 결과 (Results)

데이터셋: 정제된 FOLIO 검증 세트 (203 개 예시)
모델: Gemini 2.5 Flash 기반 (두 에이전트 모두 동일)

카테고리	CoT Baseline 정확도	Auto-formalization 정확도	비고
TRUE	89.04%	90.41%	유사한 성능
FALSE (모순)	44.26%	77.05%	가장 큰 개선 (약 33%p)
UNCERTAIN (불확실)	84.06%	91.30%	유의미한 개선
전체 정확도	73.89%	86.70%	약 12.8%p 향상

• 분석: CoT 는 모순 (FALSE) 판별에 취약했으나, Z3 솔버를 활용한 자동 형식화 에이전트는 논리적 불일치를 정확하게 식별하여 성능을 크게 향상시켰습니다. 또한, 불확실한 경우 (UNCERTAIN) 에도 솔버 기반 추론이 유리함을 보였습니다.

5. 의의 및 결론 (Significance)

• 평가 패러다임의 전환: 단순한 정답률 측정을 넘어, 에이전트의 실행 과정, 오류 유형, 그리고 재현성을 체계적으로 관리하는 '에이전트 기반 평가'의 중요성을 강조했습니다.
• 도구 사용 에이전트의 신뢰성: 논리적 추론과 같은 복잡한 작업에서 LLM 의 직접적인 추론 (CoT) 보다, 외부 도구 (SMT 솔버) 를 활용한 형식적 검증이 훨씬 강력하고 견고함을 입증했습니다.
• 미래 전망: 이 프레임워크는 다양한 도구 사용 에이전트 환경으로 확장 가능하며, 평가자 에이전트의 정책을 개선함으로써 더 복잡한 에이전트 시스템의 벤치마킹에 기여할 수 있습니다.

이 논문은 ICLR 2026 Agents in the Wild (AIWILD) 워크숍에 채택되었으며, 에이전트 평가의 표준화와 신뢰성 있는 벤치마킹을 위한 중요한 발걸음으로 평가됩니다.