Daily Arxiv

전 세계에서 발간되는 인공지능 관련 논문을 정리하는 페이지 입니다.
본 페이지는 Google Gemini를 활용해 요약 정리하며, 비영리로 운영 됩니다.
논문에 대한 저작권은 저자 및 해당 기관에 있으며, 공유 시 출처만 명기하면 됩니다.

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

Created by
  • Haebom

저자

Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang, Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang, Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, Thomas Hanwen Zhu

개요

본 논문은 대규모 언어 모델(LLM)의 수학적 추론 능력 향상을 위한 새로운 모델 Seed-Prover를 제안합니다. Seed-Prover는 Lean이라는 형식 검증 언어를 활용하여 강화 학습을 통해 증명 과정을 반복적으로 개선합니다. IMO 수준의 문제 해결을 위해 세 가지 추론 전략을 설계하였으며, 과거 IMO 문제의 78.1%를 증명하고 MiniF2F 데이터셋에서 최고 성능을 달성하였습니다. 또한 기존의 형식 기하 엔진보다 성능이 우수한 Seed-Geometry 엔진을 개발하여 기하 문제 해결 능력을 향상시켰습니다. Seed-Prover와 Seed-Geometry를 활용하여 IMO 2025에 참가하여 6문제 중 5문제를 완벽히 증명하는 성과를 거두었습니다. 이는 형식 검증과 장기 사고 연쇄 추론의 효과를 보여주는 자동 수학적 추론 분야의 중요한 발전입니다.

시사점, 한계점

•
시사점:
◦
LLM을 이용한 수학적 정리 증명 분야에서 상당한 성능 향상을 달성.
◦
Lean과 같은 형식 언어를 활용한 강화 학습의 효과성을 입증.
◦
Seed-Geometry를 통해 기하 문제 해결 능력 향상.
◦
실제 IMO 참가를 통해 모델의 실용성 검증.
•
한계점:
◦
Lean 언어에 대한 의존성 (Lean 지원하지 않는 문제 유형은 해결 불가능).
◦
Seed-Geometry의 성능 향상에도 불구하고, 기하 문제 해결의 완전성은 여전히 제한적일 수 있음.
◦
IMO 2025에서 1문제는 증명하지 못함. 모든 수학 문제에 대한 완벽한 해결책은 아님.
👍
Made with Slashpage