Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability

기술 요약: 선호도 기반 최대 만족도 문제를 통한 대규모 언어 모델을 활용한 신뢰할 수 있는 추론

문제 정의

대규모 언어 모델 (LLM) 은 자연어 이해 및 코드 생성 분야에서 뛰어난 능력을 보여주지만, 여러 제약 조건과 사용자 정의 선호도가 포함된 복잡한 최적화 문제를 처리할 때는 상당한 신뢰성 부족을 보입니다. 정확성과 증명 가능한 최적성이 필수적인 로봇 공학 및 물류와 같은 분야에서 LLM 은 내부 추론 (예: 사고의 사슬, Chain-of-Thought) 만이나 직접적인 답변 생성에 의존할 때, 종종 경직된 제약 조건을 충족시키지 못하거나 목적 함수를 최소화하지 못합니다. 이러한 실패는 최적화의 조합적 특성과 LLM 의 정밀한 추론 수행 불가에서 비롯되며, 검증하기 어려운 실행 불가능하거나 비최적의 해를 초래합니다. 또한, 기존 최대 만족도 (MaxSAT) 와 같은 형식적 방법은 사용자가 선호도를 PDDL 과 같은 특수하고 경직된 언어로 표현해야 하므로 비전문가에게는 진입 장벽이 됩니다.

방법론

본 논문은 LLM 의 추론을 형식적 솔버로 외부화하는 하이브리드 신경 - 심볼릭 접근법을 제안합니다. 핵심 패러다임인 "바이브 코딩 (vibe coding)"은 LLM 이 자연어 문제 설명을 실행 가능한 파이썬 코드로 변환하고, 이를 정밀한 MaxSAT 솔버가 해결하는 과정을 포함합니다.

제안된 파이프라인은 다음 단계로 구성됩니다:

1. 중간 계획 수립: 코드 생성 전에 LLM 에게 의사 결정 변수, 경직된 제약 조건, 그리고 부드러운 선호도에 대한 구조화된 심볼릭 설명을 생성하도록 프롬프트를 제공합니다. 이 단계는 문제를 체계적으로 분해하도록 강제하여 모델링 정확도를 높이는 것을 목표로 합니다.
2. 코드 생성: LLM 은 PySAT API 를 사용하여 문제를 가중치 부분 MaxSAT 인스턴스로 인코딩하는 파이썬 코드를 생성합니다. 경직된 제약 조건은 경직된 절 (hard clauses) 로 인코딩되고, 사용자 선호도는 가중치 부드러운 절 (weighted soft clauses) 로 인코딩됩니다.
3. MaxSAT 해결: 생성된 코드를 실행하여 MaxSAT 솔버 (구체적으로 PySAT 의 RC2) 를 호출합니다. 솔버는 반환된 할당이 실행 가능 (모든 경직된 절을 만족) 하고 최적 (인코딩된 문제에 대해 만족되지 않은 부드러운 절의 총 가중치를 최소화) 임을 보장합니다.
4. 검증: LLM 의 내부 추론에 의존하지 않고 시스템을 평가하기 위해, 저자들은 각 문제 인스턴스에 대한 "표준 (canonical)" MaxSAT 인코딩을 구성합니다. 이 표준 인코딩은 검증만을 위한 기준 진실 (ground truth) 로 작용합니다. LLM 이 생성한 코드가 산출한 해를 이 표준 인코딩과 비교하여 다음을 확인합니다:
   • 실행 가능성: 해가 모든 경직된 제약 조건을 만족하는가?
   • 최적성: 해가 표준 최적 해와 동일한 목적 함수 값을 달성하는가?
   • 참고: 이 검증은 참조 의미론 하에서 정확하다면 대안적인 인코딩과 여러 최적 해를 허용합니다.
5. 피드백 루프: 코드가 실행되지 않거나 오류를 발생시키면, 오류 메시지가 LLM 에게 반환되어 정교화됩니다. 중요하게도, 기준 검증 결과 (실행 가능성/최적성 확인) 는 데이터 누출이나 참조에 대한 과적합을 방지하기 위해 생성 과정에서 모델에 대한 피드백으로 사용되지 않습니다.

주요 기여

• 신경 - 심볼릭 프레임워크: 저자들은 LLM 이 가중치 부분 MaxSAT 솔버에 대한 자연어 인터페이스로 작용하여 코드 생성을 통해 사용자 의도를 형식적 MaxSAT 공식으로 변환하는 방법을 제시합니다.
• 독립적 검증: 본 연구는 실행 가능성과 최적성 모두에 대해 LLM 이 생성한 해를 표준 인코딩과 비교하여 검증하는 평가 프로토콜을 도입하여, 해의 유효성을 LLM 의 내부 추론 정확도로부터 분리했습니다.
• 선호도에 대한 실증적 분석: 논문은 다양한 제약 최적화 문제에서 사용자 정의 선호도 구성이 LLM 추론 성능에 미치는 영향을 분석합니다.
• 중간 계획 수립 평가: 이 연구는 중간 계획 수립 단계의 효과를 조사하여, 강력한 모델의 성능은 향상시키지만 약한 모델의 경우 오류 전파를 초래할 수 있음을 발견했습니다.

실험 결과

이 접근법은 최대 독립 집합 (MIS), 스케줄링, 집합 커버라는 세 가지 선호도 기반 추론 작업 계열에서 평가되었습니다. 데이터셋은 4 가지 선호도 변형당 25 개씩 총 300 개의 인스턴스 (4 개 계열 × 4 개 변형) 로 구성되었으며, 네 가지 LLM(GEMINI-3.1-PRO, GPT-5.5, LLAMA3.3, QWEN3-CODER) 에서 테스트되었습니다.

• 기선 성능: 직접 답변 및 사고의 사슬 (CoT) 기선은 성능이 낮아, MIS 및 스케줄링 작업에서 종종 0% 의 승인율을 기록했습니다. 사고의 프로그램 (PoT) 기선은 약간 개선되었으나 MaxSAT 기반 접근법보다 여전히 현저히 낮았습니다.
• MaxSAT 파이프라인 성능: 제안된 MaxSAT 기반 파이프라인은 훨씬 높은 승인율을 달성했습니다. GEMINI-3.1-PRO 및 GPT-5.5 와 같은 강력한 모델의 경우, 중간 계획 수립을 사용할 때 집합 커버 작업에서 승인율이 80% 를 초과했으며, 스케줄링 및 MIS 작업에서는 약 56~59% 에 달했습니다.
• 계획 수립의 영향: 중간 계획 수립은 가장 강력한 모델 (예: GEMINI-3.1-PRO 의 MIS 작업에서 36% 에서 56% 로 향상) 의 성능을 일관되게 향상시켰습니다. 그러나 약한 모델 (LLAMA3.3, QWEN3-CODER) 의 경우 계획 수립이 때로는 성능을 저하시켰는데, 이는 모델이 계획을 실행 가능한 코드로 정확하게 변환하지 못할 때 오류 전파가 발생할 수 있음을 시사합니다.
• 선호도 민감도: 사용자 선호도는 일반적으로 "선호도 없음" 설정에 비해 승인율을 낮추었지만, MaxSAT 기반 접근법은 모든 선호도 변형에서 기선보다 더 강력한 견고성을 보였습니다.

중요성과 주장

본 논문의 주요 기여는 새로운 솔버 아키텍처가 아니라, 선호도 인식 최적화를 위해 LLM 을 형식적 솔버의 인터페이스로 사용하는 실증적 및 방법론적 증명에 있다고 주장합니다. 저자들은 다음과 같이 주장합니다:

1. 외부화가 핵심: LLM 은 내부적으로 최적화 추론을 수행하도록 신뢰해서는 안 되며, 대신 자연어 제약 조건을 실행 가능한 코드로 변환하는 데 매우 효과적입니다.
2. 솔버를 통한 신뢰성: 최적화와 검증을 건전하고 완전한 MaxSAT 솔버에 위임함으로써, 시스템은 순수 LLM 추론이 제공할 수 없는 실행 가능성과 최적성의 형식적 보장을 달성합니다.
3. 견고성: LLM 기반 의미 해석과 MaxSAT 해결의 결합은 특수한 도메인 언어를 요구하지 않고도 사용자 선호도를 수용하는 견고하고 검증 가능한 의사 결정을 가능하게 합니다.

저자들은 의미 해석 (LLM) 과 형식적 최적화 (MaxSAT 솔버) 를 분리하는 것이 정확성이 최우선인 분야에서 특히 신뢰할 수 있는 사용자 중심 의사 결정 시스템을 구축하기 위한 유망한 방향이라고 결론지었습니다. 또한 향후 연구는 이 신경 - 심볼릭 루프의 지원을 받아 사용자가 선호도를 반복적으로 정교화할 수 있는 대화형 환경을 탐구할 것이라고 언급했습니다.