NSPI는 LLM과 기호 연산의 장점을 결합해 다항식 부등식을 자동으로 증명하는 신경-기호 프레임워크다. LLM이 근사 다항식 SOS(제곱합) 분해를 제안하면 기호 연산으로 정확한 SOS 표현으로 정제하고, Lean에서 최종 증명을 검증하는 엔드투엔드 파이프라인을 구성한다. 최대 10개 변수를 포함하는 다항식 벤치마크에서 효과성과 확장성을 실증했다. 순수 기호적 접근법의 확장성 한계와 LLM 기반 방법의 완결성 부족을 동시에 극복한 것이 특징이다.
- •LLM이 SOS 분해를 추측하고 기호 연산이 정확한 증명으로 정제하는 신경-기호 협업 구조다.
- •Lean 정리 증명기를 통한 기계 검증으로 발견에서 검증까지의 엔드투엔드 파이프라인을 완성한다.
- •최대 10개 변수 다항식까지 확장되어 기존 순수 기호 접근법의 확장성 한계를 극복했다.
- •경쟁 수학 스타일 부등식에서 뛰어난 성과를 보이는 LLM 추론과 엄밀한 기호 계산을 효과적으로 결합한다.
0단 자동
AI가 규칙대로 쓰고 그대로 게시했습니다. 사람이 따로 보지 않았습니다.
- 규칙 판
- 규칙 판 도입 이전 기사입니다.
- 남기는 것
- 규칙 판 · 모델 · 시각
- 판 기록
- 아직 없습니다.
From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
- 1.NSPI는 LLM과 기호 계산을 결합해 다항 부등식을 자동 증명하는 뉴로-심볼릭 프레임워크
- 2.LLM이 SOS 분해 추측을 생성하면 기호 계산으로 정확한 증명으로 정제
- 3.Lean 언어로 증명을 검증해 수학적 발견부터 기계 검증 증명까지 end-to-end 파이프라인 완성
- 4.최대 10개 변수 다항식 벤치마크에서 확장성과 효과성 검증
왜 중요한가?
LLM 기반 수학 추론의 한계를 기호 계산과의 결합으로 극복하고 Lean 형식화를 통한 기계 검증까지 연결해, AI 기반 수학적 발견 자동화의 새로운 가능성을 열었다.
본문 미리보기
arXiv:2605.15445v1 Announce Type: new Abstract: Automated proving of polynomial inequalities is a fundamental challenge in automated mathematical reasoning, where rich algebraic structure and a rapidly growing certificate search space hinder scalability. Purely symbolic approaches provide strong guarantees but often scale poorly as the number of variables or the degree increases, due to expensive algebraic manipulations and rapidly growing intermediate expressions. In parallel, LLM-guided metho
전체 내용이 궁금하다면?
원문을 직접 읽어보세요
이 글이 만들어진 과정
- 13:10AI 초안
