당신이 복잡한 수학 문제를 풀려고 노력하고 있다고 상상해 보세요. 하지만 천재적이지만 때때로 과신하는 천재에게 묻는 대신, 매우 조직적이고 약간은 경직되어 있지만 믿을 수 없을 정도로 정직한 사서에게 묻는 것입니다.

이것이 바로 AXIOM의 핵심 아이디어입니다. AXIOM은 "신뢰 우선"의 사고방식을 가진 수학적 추론을 수행하도록 설계된 새로운 시스템입니다. 이 시스템이 어떻게 작동하는지 간단한 개념과 비유를 통해 설명하겠습니다.

문제점: "자신만만한 오답"을 내놓는 천재

현재의 AI 모델들(당신이 대화하는 것과 같은 모델들)은 정답을 추측하기를 좋아하는 똑똑한 학생과 같습니다. 답을 모를 때도 그들은 그냥 답을 지어내어 완전한 자신감을 가지고 제시할 수 있습니다. 수학에서 이것은 위험합니다. 왜냐하면 틀린 답이 맞는 답과 똑같이 보이기 때문입니다. 사용자는 AI가 거짓말을 하고 있는지, 아니면 단순히 환각(hallucination)을 일으키고 있는지 알 방법이 없습니다.

AXIOM의 솔루션: "특화된 조립 라인"

AXIOM은 처음부터 모든 것을 해결하려는 천재가 되려고 노력하지 않습니다. 대신, AXIOM은 네 가지 엄격한 규칙을 가진 매우 효율적인 공장 조립 라인처럼 작동합니다.

1. 분류기 (정규 표현식 라우터 - The Sorter)

질문이 들어오면 질문은 곧바로 AI에게 전달되지 않습니다. 먼저 **분류기(Sorter)**를 거칩니다. 이것은 봉투의 모양을 살피는 우편물 분류원과 같습니다.

만약 편지가 "단순 산술" 형태라면, **급행 차선(Fast Lane)**으로 보내집 most니다.
만약 "대수학" 형태의 편지라면, **대수학 스테이션(Algebra Station)**으로 보내집니다.
만약 모양이 알려진 카테로리에 맞지 않는다면, 분류원은 즉시 "알 수 없음(Unknown)" 도장을 찍고 멈춥니다. 결코 추측하지 않습니다.

2. 번역기 (번역가로서의 AI - The Translator)

편지가 특정 스테이션에 도달했다면, AI에게 문제를 풀라고 요청하지 않습니다. 대신 AI는 번역가 역할을 합니다.

기존 방식: "여기 문장제 문제가 있습니다. 풀어주세요." (AI가 단계를 추측함).
AXIOM 방식: "여기 문장제 문제가 있습니다. 이를 우리 계산기가 이해할 수 있는 특정한 좁은 형식으로 다시 작성해 주세요."
AI는 스스로 수학 문제를 푸는 것이 엄격히 금지됩니다. AI의 역할은 다음 단계에서 완벽하게 읽을 수 있도록 문장을 정리하는 것뿐입니다.

3. 계산기 (결정론적 엔진 - The Calculator)

AI가 문제를 재작성하면, 이는 계산기(컴퓨터 대수 시스템)로 전달됩니다. 이 로봇은 절대 추측하지 않고, 지치지도 않으며, 환각을 일으키지도 않습니다.

이 로봇은 재작성된 문제를 받아 숫자를 계산합니다.
문제를 풀 수 있다면, 답을 내놓습니다.
만약 풀 수 없다면(예를 들어 수학이 너무 기괴하거나 입력값이 약간 잘못된 경우), 계산기는 멈추고 다음과 같이 말합니다: "이것을 검증할 수 없습니다."

4. "정직함" 규칙 (기권 - The "Honesty" Rule)

이것이 가장 중요한 부분입니다. 대부분의 시스템에서는 계산기가 실패하더라도 시스템이 어떻게든 추측을 시도할 수 있습니다. 하지만 AXIOM에서는 "모른다"라고 말하는 것도 하나의 유효하고 구조화된 답변입니다.
라인의 어느 부분에서든 실패가 발생하면(분류기가 모양을 인식하지 못했거나, 번역기가 재작성에 실패했거나, 계산기가 풀지 못한 경우), 시스템은 명확한 메시지를 출력합니다: "나는 기권합니다(I am abstaining)." 시스템은 결코 자신만만한 오답을 내놓지 않습니다.

결과: 속도와 안전성

이 논문은 이 시스템을 테스트한 결과 놀라운 통계치를 보고합니다:

자신만만한 실수 제로: 수천 번의 테스트 동안, 시스템은 맞는 답처럼 보이는 틀린 답을 단 한 번도 내놓지 않았습니다. 답을 냈다면, 그것은 검증된 것입니다.
높은 정확도: 표준 수학 테스트에서 약 94%의 정답률을 기록했습니다.
속도: 단순한 수학(예: "2 + 2")의 경우, AI 번역기를 거치지 않고 1밀리초 만에 해결합니다 (당신이 눈을 깜빡이는 것보다 빠릅니다). 더 어려운 문제의 경우에도, 일반적인 AI에게 "단계별로 생각하라"고 요청하는 것보다 훨씬 빠릅니다.
비용: AI에게 긴 에세이를 쓰거나 추측하게 하지 않기 때문에 실행 비용이 거의 들지 않습니다.

"전방 역동성": 망가지지 않고 발전하기 (The "Forward Dynamic")

저자들은 이 시스템이 성장하도록 설계되었음을 강조합니다.

시스템이 모르는 새로운 유형의 수학 문제를 접한다고 가정해 봅시다. 침묵하며 실패하거나 추측하는 대신, 시스템은 다음과 같이 기록합니다: "이런 모양을 보았지만, 이를 위한 스테이션이 없습니다."
그러면 개발자는 그 모양에 특화된 새로운 "스테이션(새로운 규칙)"을 구축할 수 있습니다.
모든 스테이션은 격리되어 있기 때문에, 새로운 스테이션을 추가하는 것이 기존의 것들을 절대 망가뜨리지 않습니다. 이는 고속도로에 새로운 차선을 추가하는 것과 같습니다. 기존 차선의 교통 흐름을 방해하지 않습니다.

요약 비유

표준 AI를 모자 속에서 답을 꺼내는 마술사라고 생각해보세요. 때로는 토끼가 있고, 때로는 양말이 나오기도 하지만, 마술사는 그것이 토끼인 것처럼 행동합니다.

AXIOM은 품질 관리 검사관입니다.

제품이 상자에 맞는지 확인합니다.
항목에 명확한 라벨을 붙입니다.
제품을 측정 기계에 통과시킵니다.
기계가 측정할 수 없다면, "불합격(Rejected)" 태그를 붙입니다.

이 시스템은 마술사보다 더 많은 제품을 탈락시킬 수도 있지만, "통과(Pass)" 태그와 함께 공장을 나가는 모든 제품은 반드시 정확함이 보장됩니다.

기술 요약: AXIOM – 신뢰 우선형 신경-기호 실행 아키텍처 (A Trust-First Neuro-Symbolic Execution Architecture)

1. 문제 정의

본 논문은 최첨단 대규모 언어 모델(LLM)의 수학적 추론에서 발생하는 근본적인 검증 가능성 결여 문제를 다룬다. LLM은 벤치마크에서 높은 정확도를 달성하지만, "프롬프트 입력-텍스트 출력" 인터페이스를 통해 작동하며, 이 과정에서 확신에 찬 오답(confident-wrong)은 구조적으로 정답과 구분이 불가능하다. 기존의 대안들은 상당한 트레이드오프를 수반한다:

**Lean 기반 증명기(Prover)**는 자연어 질의를 위한 병목 현상을 생성하는 특정 구문(예: Lean)으로 문제를 사전 형식화해야 한다.
폐쇄형 전문가 시스템(예: Wolfram Alpha)은 기호적 백엔드를 제공하지만, 입력 경계에서의 LLM 증강이 부족하며 조사 가능한 유도 흔적(derivation traces)을 제공하지 않는다.

저자들은 "확신에 찬 오답"이 수학적 추론에서 가장 최악의 실패 모드라고 주장한다. 이들은 설계 목표를 "정확도 우선(accuracy-first)"에서 "신뢰 우선(trust-first)"으로 전환할 것을 제안하며, 여기서 신뢰를 $1 - \frac{\text{wrong}}{\text{attempted}}$ 로 정의한다 (여기서 'wrong'은 시스템이 명시적으로 답변을 거부(abstain)한 기록은 제외한다).

2. 방법론: AXIOM 아키텍처

AXIOM은 LLM이 솔버(solver)가 아닌 엄격한 **정규화 도구(canonicalizer)**로서 기능하는 신경-기호 실행 아키텍처이다. 이 시스템은 자연어(NL) 입력을 결정론적인 컴퓨터 대수 시스템(CAS) 파이프라인으로 라우팅한다. 핵심 설계는 네 가지 약속(commitment)에 기반한다:

2.1 1:1:1 태스크 라우팅 정렬

단일한 모놀리식(monolithic) LLM이나 범용 핸들러 대신, AXIOM은 **1:1:1 불변성(invariant)**을 채택한다:

트리거(Trigger): 단 하나의 태스크를 정확히 선택하는 문제 형태(problem-shape) 정규식.
프롬프트(Prompt): 해당 특정 형태에 맞춤화된 퓨샷(few-shot) 예시를 포함한 스키마별 프롬프트.
핸들러(Handler): 오직 해당 특정 스키마만을 소비하는 결정론적 CAS 핸들러.

이러나 정렬은 새로운 태스크( $T_{N+1}$ )를 추가하더라도 기존 태스크( $T_1 \dots T_N$ )를 퇴보시키지 않음을 보장한다. 이는 모놀리식 모델에서 발견되는 "표상 예산(representational budget)" 경쟁을 방지한다.

2.2 일급 객체로서의 답변 거부(Abstain)

시스템은 answer=null을 실패가 아닌 구조적으로 유효한 출력으로 취급한다. 세 가지 독립적인 채널이 답변 거부를 유발할 수 있다:

라우터 미스(Router Miss): 입력에 매칭되는 정규식 트리거가 없음.
번역기 거부(Translator Abstain): LLM이 입력을 스키마로 재작성할 때 추측(guessing) 없이 unknown을 명시적으로 반환함 (퓨샷 예시를 통해 학습됨).
핸들러 거부(Handler Abstain): CAS 파이프라인이 검증된 답을 도출할 수 없는 경우 (예: 인식되지 않는 술어 또는 ConditionSet을 만남).

결정적으로, 시스템은 **화이트리스트 가드(whitelist guard)**를 강제한다: 핸들러가 인식되지 않는 술어를 만날 경우, 특정 값(예: 0)을 기본값으로 설정하는 대신 반드시 답변을 거부해야 하며, 이를 통해 "확신에 찬 오답" 출력을 방지한다.

2.3 복합 태스크 체인 프레임워크(Composed-Task Chain Framework)

다단계 문제(예: 파싱, 분기별 풀이, 집계가 필요한 piecewise 함수)를 위해 AXIOM은 ComposedTask 프레임워크를 사용한다. 이 프레임-워크는 결정론적 연산자(순수 함수)를 체이닝하며, LLM은 오직 시작 단계(InitialExtractor)에서 한 번만 호출된다. 체인은 등록 시점에 의존성을 검증하여, 단계 중 하나라도 실패할 경우 침묵하는 오류(silent error) 대신 깔끔한 답변 거부로 이어지도록 보장한다.

2.4 규칙 전용 경로(Rule-Only Path)

폐쇄형 기본 산술(산술 연산자와 숫자만 있고 산문이 없는 경우)의 경우, LLM 단계를 완전히 건너뛴다. 시스템은 입력을 결정론적 CAS 평가기로 직접 라우팅한다. 이 경로는 실행 간 비트 동등성(bit-equivalence)을 보장하며 추론 비용이 발생하지 않는다.

3. 주요 기여

본 논문은 정적인 정확도 수치보다 아키텍처의 **순방향 역학(forward dynamic)**을 강조한다. 주요 기여는 다음과 같다:

아키텍처 프레임워크: 규칙 전용 바이패스와 복합 태스크 체인을 갖춘 1:1:1 라우팅 시스템.
운영 규율(Operational Discipline): 신뢰할 수 있는 신경-기호 시스템을 위한 일련의 원칙들:
- 수학 템플릿 버케팅(Math-template bucketing): 표면적인 문구가 아닌 솔버 구조에 기반한 라우팅.
- LOST_CORRECT 스캔: 새로운 태스크가 기존 성능을 저해하지 않는지 확인하기 위해 아카이브된 벤치마크를 재실행하는 사전 커밋 회귀 오라클.
- 술어 미인식 = 답변 거부(Predicate-not-recognized = Abstain): "확신에 찬 오답" 출력을 막기 위한 구조적 방어.
- 파싱 우선 온보딩(Parseable-first onboarding): 새로운 도메인에 대한 신뢰를 최적화하기 전에 파싱 가능한 입력의 비율을 먼저 최적화함.
선형-가법적 수익(Linear-Additive Returns): 로그 함수적 수익(정확도 이득의 감소)을 보이는 모놀리식 LLM과 달리, AXIOM의 커버리지는 태스크들이 서로를 억제하지 않으므로 등록된 태스크 수에 따라 선형적으로 증가한다.

4. 실험 결과

아키텍처는 MATH 벤치마크(4개 카테고리), lm-eval-harness 산술 스위트, 그리고 공공 프로덕션 배포 환경(~30,000 쿼리)에서 평가되었다.

MATH 벤치마크 (4개 카테고리):
- 누적 정답률(Cumulative Correctness): 94.36% (2,592/2,747).
- 파싱 가능 데이터에 대한 신뢰도(Trust on Parseable): 4개 영역(대수학, 정수론, 계수 및 확률, 프리칼큘러스) 전체에서 100.00%. 확신에 찬 오답은 0건이었다.
- 지연 시간(Latency): LLM 기반 태스크의 중앙값 446 ms, 규칙 전용 태스크 1 ms.
lm-eval-harness 산술:
- 정확도: 100.0% (20,000/20,000).
- 비용: LLM API 호출 0회; 일반적인 CPU에서 실행 시간 21.6초.
프로덕션 배포:
- 약 30,000개의 쿼리를 처리하면서 API 경계에서 확신에 찬 오답 사례가 0건 발생함.
- 지연 시간 격차: 규칙 전용 경로(1 ms)와 LLM 기반 경로(446 ms) 사이의 약 400배 차이.
순수 LLM (Qwen 2.5 7B CoT)과의 비교:
- AXIOM은 어려운 도메인(예: 프리칼큘러스에서 +38.2 pp)에서 순수 CoT 베이스라인보다 정확도가 크게 높았으며, CoT 베이스라인이 수백 개의 오답을 내는 동안 AXIOM은 0개의 오답을 기록했다.
- AXIOM은 좁은 범위의 프롬프팅과 반복적 추론 루프의 부재 덕분에 평균적으로 약 24배에서 40배 더 빨랐다.

5. 의의 및 주장

본 논문은 AXIOM이 모놀리식 LLM이나 사전 형식화된 증명기가 제공할 수 없는 **런타임 신뢰 보증(runtime trust guarantee)**을 확립한다고 주장한다. 그 의의는 특정 정확도 점수를 달성하는 것이 아니라, 다음과 같은 **순방향 역학(forward dynamic)**을 가능하게 하는 데 있다:

단조적 개선(Monotonic Improvement): 프로덕션에서 기록된 모든 답변 거부는 다음 배포 사이클에서 정답이 될 수 있는 후보가 된다. 시스템은 타겟팅된 태스크 생성을 통해 '거부'를 '정답'으로 변환할 수 있도록 설계되었다.
검증 가능성(Verifiability): 신뢰는 하위 모델의 속성이 아니라, 검증 경로(결정론적 CAS)로부터 도출되는 아키텍처적 속성이다.
확장성(Scalability): 이 아키텍처는 250회 이상의 커밋 동안 lost_correct 회귀 없이 수천 개의 태스크 트리플(3,100개 이상 배포됨)을 점진적으로 추가할 수 있도록 지원한다.

저자들은 비전 통합의 부재로 인한 시각 고정 기하학 문제와 NLP 고유의 난해한 문장 문제(NLP-irreducible word problems)를 한계점으로 인정하지만, 이를 아키텍처의 점진적 한계가 아닌 레지스트리의 다음 발전 단계로 규정한다. 핵심 기여는 "오늘의 답변 거부"를 규율 있고 검증 가능한 엔지니어링 프로세스를 통해 "내일의 정답"으로 바꿀 수 있는 프레임워크를 제공하는 것이다.

AXIOM: A Trust-First Neuro-Symbolic Execution Architecture for Verifiable Mathematical Reasoning