SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas
Created by
Haebom
저자
Anjiang Wei, Yuheng Wu, Yingjia Wan, Tarun Suresh, Huanmi Tan, Zhanke Zhou, Sanmi Koyejo, Ke Wang, Alex Aiken
개요
본 논문은 대규모 언어 모델(LLM)의 논리적 추론 능력을 평가하기 위한 새로운 벤치마크인 SATBench를 소개합니다. SATBench는 부울 만족도(SAT) 문제에서 파생된 논리 퍼즐을 사용하여 LLM의 능력을 평가합니다. 기존 연구들이 주로 전제 조건으로부터 결론을 도출하는 추론 규칙 기반 추론에 집중한 것과 달리, SATBench는 특정 논리적 제약 조건을 충족하는 해결책을 찾는 것을 목표로 하는 SAT 문제의 탐색 기반 특성을 활용합니다. 각 SATBench 인스턴스는 SAT 수식에서 생성된 후 LLM을 사용하여 이야기 맥락과 조건으로 변환됩니다. 생성 과정은 완전 자동화되어 있으며 절의 수를 변경하여 난이도를 조절할 수 있습니다. 총 2100개의 퍼즐은 LLM 지원 및 솔버 기반 일관성 검사를 통해 검증되었으며, 일부는 사람에 의해 검증되었습니다. 실험 결과, 가장 강력한 모델인 o4-mini조차도 어려운 UNSAT 문제에서 65.0%의 정확도만 달성하여 50%의 무작위 기준선에 가까웠습니다. SATBench는 현재 LLM의 탐색 기반 논리적 추론 능력의 근본적인 한계를 보여주고 향후 논리적 추론 연구를 위한 확장 가능한 테스트베드를 제공합니다.
시사점, 한계점
•
시사점:
◦
LLM의 탐색 기반 논리 추론 능력의 한계를 명확하게 제시합니다.
◦
LLM의 논리적 추론 능력 평가를 위한 새로운 벤치마크를 제공합니다.
◦
SAT 문제를 활용하여 난이도 조절이 가능한 확장성 있는 테스트베드를 제공합니다.
◦
향후 LLM의 논리적 추론 능력 향상 연구에 중요한 기여를 할 수 있습니다.
•
한계점:
◦
현재 벤치마크의 규모(2100개 퍼즐)가 향후 더욱 다양하고 방대한 데이터셋을 필요로 할 수 있습니다.
◦
LLM을 이용한 문제 생성 및 변환 과정에서 LLM의 편향이나 한계가 결과에 영향을 미칠 수 있습니다.
◦
인간 검증이 일부 퍼즐에만 적용되어 전체 데이터셋의 신뢰성에 대한 추가적인 검증이 필요할 수 있습니다.
