기술 요약: 오류에서 증명으로: 신경-기호적 제약 충족 해결을 위한 최소 핵심 유도형 수리(Minimal-Core-Guided Repair)

문제 정의

언어 모델(LM)은 점점 더 이산적인 추론 문제(예: 스케줄링, 좌석 배치, 패킹)를 해결하는 과업을 맡고 있습니다. LM은 유창한 텍너스트를 생성할 수는 있지만, 전역적인 조합 제약(global combinatorial constraints)을 강제하는 메커니 mechanism이 부족하여, 명시된 규칙을 위반하는 답을 내놓는 경우가 빈번합니다. 표준적인 해결책은 "오프로딩(offloading)"을 통해 탐색 과정을 신뢰할 수 있는 솔버(solver)로 넘기는 것입니다. 즉, LM이 자연어 문제를 정식 명세(formal specification)로 변환(자동 형식화, autoformalization)하면, 솔버(예: Answer Set Programming 솔버)가 추론을 수행하는 방식입니다.

그러나 이 파이프라인의 신뢰도는 번역의 품질에 달려 있습니다. LM은 두 가지 방식으로 실패합니다:

1. 잘못된 형식의 번역(Malformed Translations): 코드가 구문 오류(syntax errors)나 그라운딩 이슈를 포함하여 솔버를 충돌(crash)하게 만듭니다.
2. 불충실한 번ानों(Unfaithful Translations): 코드는 구문적으로는 유효하지만 의미론적으로는 틀린 경우입니다. LM은 명시되지 않은 제약을 추가하여(해결 가능한 문제를 불가능하게 만듦) 또는 명시된 제약을 누락하여(유효하지 않은 솔루션을 허용함) 문제를 일으킬 수 있습니다.

기존의 자기 수정(self-correction) 파이프라인(예: Logic-LM)은 첫 번째 실패 모드에 반응하여 솔버의 에러 메시지를 반환합니다. 하지만 두 번째 실패 모드(프로그램은 실행되지만 논리적으로 틀린 경우)가 발생하면, 솔버는 단순히 "해를 찾을 수 없음(no solution)"이라는 침묵된 판정을 내립니다. 이때 LM은 문제가 실제로 불가능한 것인지 아니면 자신의 과잉 제약된 번역 때문인지 구분하지 못하며, 종종 불가능한 문제에 대해 억지로 해를 만들어내기 위해 제약을 계속 수정하는 오류를 범합니다.

방법론

저자는 일반적인 에러 메시지 대신 **증명 아티팩트(proof artifact)**인 **최소 불만족 핵심(Minimal Unsatisfiable Core, MUC)**을 사용하는 수리 루프를 제안합니다.

시스템 아키텍처

시스템은 4단계 루프로 작동합니다:

1. 형식화(Formalization): LM이 ASP 인코딩을 생성합니다. 일관성을 보장하기 위해, 저자는 모든 결정이 단일 관계인 assign(Var, Value)를 통해 표현되도록 하는 "결정 계약(decision contract)"을 강제합니다. 인코딩은 다음으로 구성됩니다:
   • Facts: 문제 데이터.
   • Choice Rules: 후보 결정 생성.
   • Integrity Constraints: 요구 사항을 강제하는 부분(LM 오류가 가장 발생하기 쉬운 부분).
2. 솔빙(Solving): 인코딩이 컴파일되고 clingo를 사용하여 해결됩니다.
3. 분류 및 진단(Classification & Diagnosis): 솔버 결과는 네 가지 범주로 분류됩니다:
   • OK: 유효한 answer set 발견.
   • SYNTAX ERROR: 파싱 또는 그라운딩 실패.
   • EMPTY: 프로그램은 만족 가능하지만 결정이 없음(예: choice rule 누락).
   • UNSAT: 프로그램은 잘 구성되었으나 해가 없음.
4. 수리(Repair):
   • SYNTAX ERROR 및 EMPTY의 경우, 표준 에러 메시지나 프롬프트가 사용됩니다.
   • UNSAT의 경우, 모델 자체의 무결 제약 조건(integrity constraints)에 대해 **최소 불만족 핵심(Minimal Unsatisfiable Core)**을 계산합니다. 삭제 필터링 알고리즘(QuickXplain 계열의 일원)을 사용하여, 기본 프로그램과 결합했을 때 불만족을 야기하는 가장 작은 제약 집합($C^*$)을 식별합니다.

수리 신호(The Repair Signal)

시스템은 LM에게 "해를 찾을 수 없다"고 말하는 대신, 특정 충돌 제약 집합($C^*$)을 반환하고 원래의 문제 텍스트와 이를 어떻게 조화시킬 것인지 LM에게 요청합니다. LM은 다음 중 하나를 수행하도록 유도됩니다:

• 제약 중 하나가 문제를 잘못 형식화했음을 식별하고 이를 수정하거나 제거함.
• 제약이 텍스트를 충실하게 인코딩했음을 확인하여, 문제가 실제로 불가능함을 인정함.

결정적으로, 이 과정은 누출이 없습니다(leakage-free). 핵심(core)은 정답(ground truth)이나 오라클을 참조하지 않고 오직 LM이 생성한 프로그램만을 바탕으로 계산됩니다.

주요 기여

1. 최소 핵심 유도형 수리(Minimal-Core-Guided Repair): 본 논문은 LM의 자기 수정을 위한 피드백 신호로 최소 불만족 핵심을 사용하는 수리 메커니즘을 도입합니다. 일반적인 에러 메시지와 달리, 핵심은 왜 제약들이 충돌하는지에 대한 구조적 증명을 제공하여, 정답을 노출하지 않으면서도 결함을 국소화합니다.
2. 자동 형식화 충실도 진단(Diagnosis of Autoformalization Fidelity): 7개 영역에 걸친 77개 문제의 새로운 벤치마크를 통해, 저자는 LM의 ASP 번역이 6개 영역(예: 그래프 채색, 배낭 문제)에서는 매우 충실(정확도 100%)하지만, **집계-범위 스케줄링(aggregate-coverage scheduling)**에서는 무너진다는 것을 보여줍니다. 이러한 실패는 모델의 일반적인 능력 부족이 아니라, 전역 카운팅 제약(global counting constraints)을 인코딩하는 어려움 때문인 것으로 분석되었습니다.
3. 기호적 오프로딩 가치의 재조정(Recalibration of Symbolic Offloading Value): 연구 결과, 강력한 Chain-of-Thought(CoT) 베이스라인이 기호적 파이프라인의 정확도와 유사한 수준에 도달할 수 있음에도 불구하고, 기호적 경로는 다음과 같은 뚜렷한 장점을 가집니다:
   • 조작 제로(Zero Fabrication): 파이프라인은 불가능한 문제에 대해 해를 조작(fabricate)하는 일이 전혀 없습니다(0%의 조작률). 반면 직접 프롬프팅은 21%의 확률로 조작을 수행합니다.
   • 인증서(Certificates): 프롬프팅은 보장할 수 없는 최적성(optimality) 및 불가능성(infeasibility)에 대한 인증서를 제공합니다.

실험 결과

저자는 gemma4:31b와 deepseek-v3.2 두 가지 오픈 웨이트 모델을 사용하여 직접 프롬프팅, Chain-of-Thought, 표준 에러 메시지 수리 등의 베이스라인과 함께 77개 인스턴스에 대해 접근 방식을 평가했습니다.

• 정확도: 기본 모델(gemma4:31b)에서 최소 핵심 수리가 적용된 기호적 파이프라인은 **89.6%**의 실행 가능성 정확도를 달성하여, 직접 프롬프팅(74.0%)을 능가하고 대부분의 영역에서 CoT(98.7%)와 대등하거나 이를 상회했습니다. 파이프라인의 정확도는 주로 집계 제약(aggregate constraints) 처리에 어려움을 겪는 스케줄링 영역에서 제한되었습니다.
• 조작 감소(Fabrication Reduction): 가장 중요한 발견은 조작된 실행 가능성(fabricated feasibility)(불가능한 문제에 대해 해가 있다고 주장하는 것)에 관한 것입니다.
  • 더 약한 모델인 deepseek-v3.2의 경우, 일반적인 에러 메시지 수리는 불가능한 인스턴스에 대해 **79%**의 조작률을 보였습니다.
  • 최소 핵심 수리는 이를 **7%**로 낮추었습니다.
  • 핵심(core)은 모델이 실제 제약을 임의로 삭제하여 충돌을 해소하려는 시도를 방지함으로써, 모델이 진정한 불가능성을 인식하도록 강제합니다.
• 모델 강도 의존성(Model Strength Dependency): 핵심의 이점은 조건부적입니다. 거짓 불만족을 거의 생성하지 않는 강력한 모델(gemma4:31b)의 경우, 핵심이 일반 수리에 비해 미미한 개선만을 제공했습니다. 핵심은 조작성이 높은 약한 모델에서 가장 결정적인 역할을 합니다.

의의 및 주장

본 논문은 강력한 LM 시대에 기호적 오프로딩의 가치가 반드시 더 높은 정확도에 있는 것이 아니라, **강건성(robustness)과 인증(certification)**에 있다고 주장합니다.

• 에러 메시지보다 증명(Proof over Error): 저자는 에러 메시지를 증명 아티팩트(최소 핵심)로 교체하는 것이 LM 수리를 위한 더 우수한 피드백 메커니즘이라고 주장합니다. 이는 결함을 구조적으로 국소화하고 모델이 불가능한 문제에 대해 환각(hallucination)을 일으키는 것을 방지합니다.
• 구조적 충실도(Structured Fidelity): 자동 형식화에 대한 신뢰는 세밀해야 함을 시사합니다. 모델은 로컬 제약에는 신뢰할 수 있으나 전역 카운팅에는 취약하며, 이는 "신뢰의 단위"가 모델 자체가 아니라 형식화 패턴이어야 함을 나타냅니다.
• 피드백으로서의 솔버 아티팩트: 본 연구는 솔버 측의 아티팩트(핵심 등)가 단순한 판정을 넘어, LM이 더 신뢰할 수 있는 신경-기호적 추론을 수행할 수 있도록 하는 일급 피드백(first-class feedback)으로 취급되어야 한다고 제안합니다.

저자는 기호적 경로가 정확도 면에서 강력한 CoT를 항상 압도하지는 않더라도, 잘못된 답이 치명적인 비용을 초래하는 애플리케이션에서 불가능성을 인증하고 조작을 거부하는 능력 덕분에 필수적이라고 결론짓습니다.