무작위로 생성한 SAT/UNSAT CNF 인스턴스를 여러 LLM에 입력하고, z3로 결과를 검증해 추론 능력을 평가한 실험과 그 결론.
URL: https://blog.aiono.dev/posts/can-llms-sat.html
Title: Can LLMs SAT?
최근 몇 년 사이 LLM은 전반적인 성능에서 눈에 띄는 개선을 보여 왔습니다. 몇 년 전 처음 대중화되었을 때도 사람처럼 대화하는 능력은 이미 인상적이었지만, 추론 능력은 늘 부족했습니다. 예를 들어 좋아하는 작가 문체로 어떤 정렬 알고리즘이든 설명할 수는 있었지만, 덧셈조차 일관되게 수행하지 못하곤 했습니다. 하지만 이후 크게 발전했고, 이제는 “추론에 실패하는 사례”를 찾기가 점점 더 어려워졌습니다. 그 결과 충분히 스케일링하면 LLM이 일반적인 추론을 학습할 수 있을 것이라는 믿음이 생겼습니다.
저는 이 주장을 SAT 문제로 시험해 보고 싶었습니다. 왜 SAT일까요? SAT 문제를 푸는 데에는 극히 소수의 규칙을 일관되게 적용하는 능력이 필요합니다. 변수가 수백만 개든 몇 개뿐이든 원리는 같습니다. 즉, 제대로 추론할 줄만 안다면 시간이 충분하다는 가정하에 어떤 SAT 인스턴스든 풀 수 있습니다. 또한 완전히 무작위 SAT 문제를 쉽게 생성할 수 있기 때문에, LLM이 순수한 패턴 인식만으로 맞히기 어려워집니다. 따라서 SAT는 LLM이 학습 데이터 너머로 기본 규칙을 일반화할 수 있는지 시험하기에 좋은 문제 유형이라고 생각합니다.
SAT(“satisfiability”, 만족 가능성의 약자)는 논리 문제로, 어떤 불리언(참/거짓) 공식이 주어졌을 때 그 공식을 true로 만드는 변수 대입이 존재하는지 묻습니다. 예시 불리언 공식은 다음과 같습니다.
(a || b) && !a
이 공식은 만족 가능합니다. b를 true, a를 false로 두면 전체 공식이 true가 되기 때문입니다. 다른 모든 대입은 공식을 false로 만들지만, 적어도 하나의 대입이라도 공식을 true로 만들 수 있다면 그 공식은 만족 가능하다는 사실은 변하지 않습니다.
만족 불가능(UNSAT)한 공식 예시는 다음과 같습니다.
b && !b
b에 무엇을 대입하든, && 연산자의 왼쪽 또는 오른쪽 중 하나는 항상 false이므로 결과는 false입니다.
불리언 공식에는 “Conjunctive Normal Form”(CNF, 연언 표준형)이라는 특수한 형태가 있습니다. 이 형태의 문제는 AND 연산자로 연결된 절(clause)들의 합으로 이루어지며, 각 절은 OR 연산자로 연결된 변수들로만 구성됩니다. 변수는 부정된 형태로 나타날 수 있지만, 부정은 변수에만 직접 적용될 수 있고 !(a && b) 같은 형태는 허용되지 않습니다. CNF 형태의 예시는 다음과 같습니다.
(a || b || c) &&
(!a || d || e) &&
(e || g || x)
SAT 솔버는 보통 이 형태의 공식을 입력으로 기대합니다. CNF에 최적화되어 효율적으로 풀 수 있도록 특화되어 있기 때문입니다. 저는 LLM 출력 결과를 SAT 솔버로 검증하기 위해 CNF 형태를 사용하기로 했습니다.
제 접근법은 매우 단순합니다.
LLM에게 공정한 테스트가 되려면 SAT 인스턴스는 적당히 커야 하지만 너무 크면 안 됩니다. 변수가 수천 개인 SAT 문제를 그대로 줄 수는 없습니다. 하지만 너무 쉬워서도 안 됩니다.
4-SAT의 경우, 절(clause) 대 변수(variable) 비율이 10보다 크면 생성된 문제가 풀기 어려워지고, 공식이 SAT일 확률과 UNSAT일 확률이 50%에 가까워진다는 점을 알게 되었습니다. 그래서 저는 3가지 유형의 공식을 생성했습니다.
다음 명령으로 cnfgen을 사용해 SAT 인스턴스를 생성했습니다.
cnfgen -q randkcnf 4 $VARIABLES $CLAUSES
이 명령은 dimacs format으로 공식을 출력합니다. dimacs는 모든 SAT 솔버가 지원하는 CNF 표준 형식이기 때문에, LLM의 판단을 다른 프로그램으로 검증할 수 있습니다.
여러 LLM 제공업체에 각각 가입하지 않고도 다양한 모델을 시험하기 위해 https://openrouter.ai 를 사용했습니다.
테스트한 모델은 다음과 같습니다.
각 모델은 reasoning을 활성화했고, reasoning effort는 high로 설정했습니다. GPT 5.2를 포함한 이유는 mini보다 더 잘 추론할 수 있다고 주장할 여지가 있기 때문입니다. 다만 GPT 5.2는 비용이 너무 비싸 다른 모델만큼 많이 테스트하지 못했습니다. Gemini 3 Pro도 비용이 들긴 했지만, 제 경험상 GPT 5.2만큼 추론 과정에서 시간을 쓰지는 않아서 상대적으로 부담이 덜했습니다.
각 모델에는 동일한 시스템 프롬프트를 사용했습니다.
The user will give a CNF in dimacs format.
Determine if it's satisfiable or not WITHOUT USING ANY EXTERNAL TOOLS.
Use your own reasoning. Don't stop even if the formula is too large just try to solve it manually.
After determining the result output a JSON with two fields:
- satisfiable: Boolean. True if the formula is satisfiable
- assignment: Array of booleans. If the formula is satisfiable provide an assignment for each variable from 1 to N. If the formula is not satisfiable this field is null.
EXAMPLE INPUT:
p cnf 10 10
-7 9 10 0
7 8 9 0
-7 -9 10 0
-2 3 5 0
-4 -6 -8 0
-1 3 -5 0
1 -3 -8 0
4 -5 -10 0
4 -7 -8 0
-2 -5 8 0
EXAMPLE JSON OUTPUT:
{
"satisfiable": true,
"assignment": [false, false, false, false, false, false, false, false, false, false]
}
LLM 출력은 꽤 괜찮은 SAT 솔버인 z3 정리 증명기를 사용해 평가했습니다. LLM 출력이 성공적이라고 판단하는 기준은 다음과 같습니다.
대입 검증은 쉽습니다. 어떤 대입이 주어지면, 그 대입을 강제하는 단일 변수 절들을 공식에 추가할 수 있습니다. 그 결과 공식이 여전히 SAT라면 그 대입은 유효하며, UNSAT가 된다면 그 대입이 공식과 모순되므로 유효하지 않습니다.
처음에는 각 모델에 대해 SAT/UNSAT 각각 최소 10개 공식으로 테스트하려 했지만, 생각보다 비용이 많이 들어서 케이스/모델당 약 5개 정도만 테스트했습니다. 처음에는 openrouter API로 과정을 자동화했지만, 추론 과정이 길어 응답이 중간에 끊기는 경험을 했고(모델 제공업체 문제인지 openrouter 문제인지는 모르겠습니다), 결국 채팅 인터페이스로 되돌아갔습니다. 이 때문에 각 테스트에 대한 표준화된 출력은 없지만, 결과에서 언급한 각 케이스는 링크로 남겼습니다.
이번 테스트에 사용한 모든 공식은 여기에서 확인할 수 있습니다.
프론티어급 플래그십 모델이라는 점을 고려하면 실망스러웠습니다. 성공 사례가 하나도 없었습니다. 추론 기능을 켜고 수준도 high로 설정했음에도 충분히 철저하게 추론하지 않는 것처럼 보였습니다.
변수 10개, 절 200개인 SAT 문제에서는 기대대로 SAT라고 출력하는 경우가 많았지만, 대입은 한 번도 유효하지 않았습니다(예: 첫 번째, 두 번째). 한 번은 SAT 공식을 UNSAT라고 주장하기도 했습니다. 이 때문에 SAT 케이스에서 더 많은 변수를 대상으로 테스트하는 수고는 하지 않았습니다.
변수 10개, 절 200개인 UNSAT 문제에서는 항상 공식이 SAT라고 주장하며 대입을 지어냈습니다(이 예시 참고).
놀랍게도 더 작은 모델임에도 Gemini 3 Pro보다 성능이 좋았습니다. SAT 공식에 대해서는 유효한 대입을 몇 번 찾았지만, UNSAT 공식에 대해서는 대입을 지어내는 동일한 문제가 있었습니다.
변수 10개, 절 200개인 SAT 문제에서는 만족하는 대입을 찾지 못하면 UNSAT을 출력하기도 했고, 더 오랜 시간이 필요하다는 식이었습니다. 이는 논리적으로는 타당합니다. 저는 이를 “추론이 나쁘다”고 보진 않았고, 성능(시간/탐색) 문제로 보았습니다. 그래서 절을 100개로 줄여 보았고, 그 경우에는 성공적으로 유효한 대입을 찾았습니다.
변수 10개, 절 200개인 UNSAT 문제에서는 Gemini 3 Pro와 동일하게 대입을 지어내는 문제가 있었습니다.
이 모델은 다른 모델들보다 훨씬 나았습니다. 변수 10개, 절 200개인 모든 SAT 문제에 대해 유효한만족대입을 찾아냈습니다. 그래서 변수 14개, 절 100개로 난이도를 올려 테스트했더니 4개 인스턴스 중 절반만 맞혔습니다(여기에서 formula14_ 접두사의 파일 참조). 절반 정답은 겉보기엔 괜찮아 보이지만, 무작위 추측과 동등합니다.
변수 10개, 절 200개인 UNSAT 문제에서는 다른 모델들과 동일하게 대입을 지어내는 문제가 있었습니다.
SAT로 LLM의 추론 능력을 시험하는 것은 새로운 아이디어가 아닙니다. 최근 연구에서는 GPT-4o 같은 모델을 포함해 철저히 테스트했고, 충분히 어려운 문제에서는 어떤 모델이든 결국 무작위 추측 수준으로 성능이 떨어진다는 결과를 보였습니다. 하지만 제가 사용한 것처럼 더 새로운 모델들을 대상으로 한 연구는 찾지 못했습니다. 더 새로운 모델들로 다시 한 번 철저한 테스트가 이루어지면 좋겠습니다.
비록 제 데이터셋은 매우 작지만, LLM이 일관되게 추론할 수 없다는 결론을 내리기에는 충분하다고 생각합니다. 또한 SAT 인스턴스가 커질수록 추론 성능이 악화되는데, 이는 추론이 진행되면서 컨텍스트 윈도우가 너무 커지고, 컨텍스트 상단의 원래 절들을 기억하기 어려워지기 때문일 수 있습니다. 제 친구는 복잡한 SAT 인스턴스가 대규모 코드베이스에서 많은 규칙을 다루는 것과 유사하다는 관찰을 했습니다. 규칙을 더 많이 추가할수록 LLM이 그중 일부를 잊을 가능성이 커지고, 이는 교묘하고 위험할 수 있습니다.
물론 그렇다고 해서 LLM이 쓸모없다는 뜻은 아닙니다. 추론을 못하더라도 분명 유용할 수 있습니다. 하지만 추론이 부족하다는 점 때문에, 규칙을 적어 놓기만 하면 LLM이 언제나 그것을 따를 것이라고 기대할 수는 없습니다. 중요한 요구사항이 있다면, 그것이 충족되도록 보장하기 위한 다른 프로세스가 필요합니다.