LLM이 생성한 근사 SOS(Sum-of-Squares) 분해 conjecture를 symbolic computation으로 정제하여 정확한 SOS 인증서를 얻고, 이를 Lean으로 형식 검증까지 자동화하는 neuro-symbolic 프레임워크 NSPI를 제안한다.
Motivation
Known: 순수 symbolic 방법(SOS decomposition을 SDP 문제로 변환하는 방식 등)은 다항식 부등식 증명에 강력한 보장을 제공하지만 변수 수나 차수가 증가할수록 조합적 폭발로 확장성이 떨어진다. 최근 LLM 기반 정리 증명(AlphaGeometry, Seed-Prover 등)과 neuro-symbolic 접근(AIPS 등)이 발전했지만, 대부분 소수 변수의 경진대회 스타일 부등식에 국한되고 LLM은 주로 탐색 가이드나 전략 선택 역할에 그친다.
Gap: 기존 neuro-symbolic 방법들은 저차원(3~4변수) 문제에 국한되며 LLM을 검색 안내자로만 활용해왔고, LLM을 직접 symbolic conjecture 생성자로 사용하는 것은 제어와 검증이 어려워 미해결 과제로 남아있었다. 본 논문은 고차원 다변수(최대 10변수) 무제약 다항식 부등식 상황에서 LLM을 주요 conjecture 생성자로 격상시키는 방법의 부재라는 gap을 다룬다.
Why: 다항식 부등식 증명은 최적화, 제어, 조합론 등 다양한 분야의 기초이며, AI의 수학적 추론 한계를 평가하는 중요한 벤치마크로 부상하고 있다. LLM의 발견적 능력과 symbolic computation의 엄밀성, Lean의 기계 검증 가능성을 결합함으로써 신뢰할 수 있는 end-to-end 자동 증명 파이프라인을 고차원 문제로 확장할 수 있다는 점에서 중요하다.
Approach: LLM이 근사적인 다항식 SOS 분해 conjecture를 제안하면, symbolic computation(Newton's method와 rational recovery)을 통해 이를 정확한 SOS 표현으로 정제하고, 최종적으로 Lean 증명 템플릿을 이용해 기계 검증 가능한 형식 증명을 자동 생성한다.
Achievement
Figure 4. Performance of different methods on PolyIneqBench
NSPI 프레임워크 제안: LLM 기반 conjecture 생성, symbolic 정제, Lean 형식 검증을 결합한 end-to-end neuro-symbolic 파이프라인을 최초로 구축.
신뢰성 브릿지(reliability bridge) 개발: 휴리스틱한 신경망 conjecture를 기계 검증 가능한 정확한 증명으로 변환하는 원리적 방법을 제시하여 고차원 다변수 문제로 확장성을 확보.
대규모 벤치마크 실험: 522개의 도전적인 부등식 문제(최대 10변수 포함)에서 기존 symbolic 및 LLM 보조 방법들을 능가하는 성능을 입증.
Neural Conjecture 모듈: computation-driven 및 structure-driven 방식으로 비음수 다항식-SOS 쌍 데이터를 구축하고, 이를 이용해 LLM을 SOS 구조 conjecturer로 학습(2단계 training: Cold Start 후 추가 학습). 학습된 모델은 주어진 비음수 다항식에 대해 SOS 표현 conjecture들을 생성하고 오차 크기에 따라 순위를 매김.
Symbolic Correction 모듈: 상위 순위 SOS conjecture로부터 Newton's method와 rational recovery를 포함한 symbolic computation 과정을 통해 정확한(exact) SOS 표현을 도출.
Formal Verification 모듈: 도출된 정확한 SOS 표현과 사전 정의된 Lean 증명 템플릿(theorem statement, proof template, SOS expression 결합)을 기반으로 완전한 Lean 형식 증명을 자동 생성.
Originality
LLM을 단순 탐색 가이드가 아닌 symbolic conjecture(근사 SOS 분해)의 주요 생성자로 격상시킨 최초의 시도.
근사 SOS conjecture를 Newton's method와 rational recovery를 통해 정확한(exact) 증명 가능한 SOS 표현으로 변환하는 "reliability bridge"라는 원리적 연결 고리를 제시.
기존 neuro-symbolic 부등식 증명이 저차원(3~4변수)에 머물던 것을 최대 10변수 다항식으로 확장하며, Lean 형식 검증까지 통합한 완전한 end-to-end 파이프라인 구축.
Limitation & Further Study
본문 발췌에는 구체적인 실험 세부사항(사용한 LLM 종류, 학습 데이터 규모, 실패 사례 분석)이 충분히 제시되지 않아 방법의 일반화 가능성 평가가 제한적임.
SOS 기반 접근은 원리적으로 SOS로 표현 가능한(즉 SOS-representable) 비음수 다항식에만 적용 가능하며, 모든 비음수 다항식이 SOS는 아니라는 한계(예: Motzkin 다항식류)에 대한 논의가 부족해 보임.
Newton's method 기반 symbolic correction의 수렴 실패 시 대안이나 실패율에 대한 분석이 필요.
후속 연구로 SOS로 표현되지 않는 비음수 다항식에 대한 확장, 제약이 있는(constrained) 부등식으로의 일반화, 더 다양한 형식 증명 보조도구(Isabelle, Coq 등)로의 확장이 고려될 수 있음.
기반 연구SPECTER2 유사도 0.92로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Minif2f: a cross-system benchmark for formal olympiad-level mathematics'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
