Axiom의 Verified AI: 수학적 증명으로 AI 학습의 한계 돌파

섹션별 상세

기존 LLM은 통계적 추론에 의존하여 복잡한 논리 문제에서 오류를 범하는 한계를 가짐.

Axiom은 Lean 언어를 활용해 AI가 생성한 증명을 형식 검증하여 논리적 무결성을 확보함.

Axiom은 Putnam 수학 시험에서 12/12점을 기록하고, Verina 벤치마크에서 99%의 성공률을 달성하며 기존 모델 대비 압도적 성능을 보임.

형식 검증은 강화학습(RL) 과정에서 명확한 보상 신호를 제공하여 모델의 학습 효율과 성능을 극대화함.

형식 검증(Formal Verification): — 시스템이나 소프트웨어가 사양을 정확히 준수하는지 수학적으로 증명하는 기법. AI 모델의 추론 과정에서 논리적 오류를 방지하고 결과의 정확성을 보장하는 데 사용됨.
Lean: — 수학적 증명을 컴퓨터가 검증 가능한 형태로 작성하는 형식 검증 언어. AI가 생성한 증명의 논리적 무결성을 확인하는 도구로 활용됨.
퍼트넘 수학 시험(Putnam Exam): — 학부생 대상의 최고 난이도 수학 경시대회. AI 모델의 고차원적 논리 추론 능력과 문제 해결력을 평가하는 벤치마크로 활용됨.