칭화대 동문팀이 AI의 도움으로 놀라운 수학적 성과를 달성했습니다! 그들이 개발한 평생 학습 기능을 갖춘 AI 보조자인 LeanAgent는 이전에 풀리지 않았던 162개의 수학 정리를 성공적으로 증명했으며 Terence Tao가 제안한 다항식 Freiman-Ruzsa 추측의 형식 문제까지 해결했습니다. 이는 기초 과학 연구에서 AI의 엄청난 잠재력을 보여줄 뿐만 아니라 수학적 연구 방법의 혁신을 의미합니다. 다운코드 편집자는 이 흥미로운 개발과 LeanAgent의 기술 혁신에 대한 심층적인 이해를 제공할 것입니다.
최근 수학계에 화제가 된 뉴스에서는 칭화대학교 동문 그룹이 AI의 힘을 이용해 이전에 누구도 풀 수 없었던 162개의 수학 정리를 성공적으로 증명했습니다. 더욱 놀라운 점은 LeanAgent라는 에이전트가 Terence Tero의 다항식 Freiman-Ruzsa 추측의 형식화 문제를 실제로 극복했다는 것입니다. 이는 기초 과학의 연구 방법이 AI에 의해 완전히 변형되었다는 사실을 한탄하게 만듭니다.
우리 모두 알고 있듯이 현재 언어 모델(LLM)은 훌륭하지만 대부분은 여전히 정적이며 온라인에서 새로운 지식을 배울 수 없습니다. 고급 수학 정리를 증명하는 것은 훨씬 더 어렵습니다. 하지만 칼텍, 스탠포드대, 워싱턴대 연구팀이 공동 개발한 린에이전트(LeanAgent)는 정리를 지속적으로 학습하고 증명할 수 있는 평생학습 능력을 갖춘 AI 보조자다.
LeanAgent는 신중하게 설계된 학습 경로를 통해 다양한 수학적 어려움에 대응하고, 동적 데이터베이스를 사용하여 지속적인 수학적 지식 흐름을 관리함으로써 새로운 지식을 학습할 때 이미 습득한 기술을 잊지 않도록 합니다. 실험에 따르면 이전에는 누구도 풀 수 없었던 162개의 수학 정리를 23개의 서로 다른 Lean 코드 라이브러리에서 성공적으로 입증했으며 그 성능은 기존 대형 모델보다 11배 더 높습니다. 정말 놀랍습니다!
이러한 정리는 추상 대수학 및 대수 위상수학과 같은 어려운 문제를 포함하여 고등 수학의 다양한 영역을 다룹니다. LeanAgent는 단순한 개념으로 시작하여 점차적으로 복잡한 주제를 다룰 수 있을 뿐만 아니라 안정성과 역이주 측면에서도 뛰어난 성능을 보여줍니다.
하지만 테렌스 타오의 도전은 여전히 AI를 무기력하게 만든다. Lean과 같은 대화형 정리 증명기(ITP)가 수학적 증명을 형식화하고 검증하는 데 중요한 역할을 하지만 이러한 증명을 구축하는 프로세스는 종종 복잡하고 시간이 많이 걸리며 세심한 단계와 광범위한 수학 코드 라이브러리가 필요합니다. o1 및 Claude와 같은 고급 대형 모델은 비공식 증명에 직면할 때 오류가 발생하기 쉬우며 이는 수학적 증명의 정확성과 신뢰성 측면에서 LLM의 단점을 강조합니다.
과거 연구에서는 LLM을 사용하여 특정 데이터 세트에 대한 대규모 모델을 훈련하여 생성된 정리 증명인 LeanDojo와 같은 완전한 증명 단계를 생성하려고 시도했습니다. 그러나 형식적인 정리 증명을 위한 데이터가 극히 부족하여 이 접근 방식의 광범위한 적용 가능성이 제한됩니다. 또 다른 프로젝트인 ReProver는 Lean 정리 증명 코드 라이브러리 mathlib4에 최적화된 모델입니다. 100,000개 이상의 정형 수학 정리 및 정의를 다루고 있지만 학부 수학 범위에 국한되어 더 복잡한 문제에 직면하면 제대로 수행되지 않습니다. 문제.
수학적 연구의 역동적인 특성이 AI에 더 큰 도전을 가져온다는 점은 주목할 가치가 있습니다. 수학자들은 일반적으로 동시에 또는 교대로 여러 프로젝트를 진행합니다. 예를 들어 Terence Tao는 PFR 추측 및 실수 대칭 평균을 포함하여 여러 연구 분야를 동시에 발전시키고 있습니다. 이러한 예는 현재 AI 정리 증명 방법의 주요 단점, 즉 특히 린 데이터가 제한적인 경우 다양한 수학 분야에서 적응적으로 학습하고 개선할 수 있는 AI 시스템이 부족함을 보여줍니다.
이것이 바로 LeanDojo 팀이 위의 문제를 해결하기 위해 설계된 새로운 평생 학습 프레임워크인 LeanAgent를 만든 이유입니다. LeanAgent의 워크플로에는 학습 과정을 공식화하기 위한 정리 복잡성 도출, 점진적인 훈련을 통한 학습 프로세스의 안정성과 유연성 균형 유지, 아직 입증되지 않은 정리를 찾기 위한 최선의 트리 검색 활용이 포함됩니다.
LeanAgent는 모든 대규모 모델과 함께 작동하여 "검색"을 통해 일반화 기능을 향상시킵니다. 그 혁신은 끊임없이 확장되는 수학적 지식을 관리하기 위한 맞춤형 동적 데이터베이스와 보다 복잡한 수학적 콘텐츠를 학습하는 데 도움이 되는 린 증명 구조를 기반으로 하는 강좌 학습 전략을 사용하는 데 있습니다.
AI의 치명적인 망각 문제를 해결하기 위해 연구원들은 LeanAgent가 이전 학습을 잊지 않고 새로운 수학적 지식에 지속적으로 적응할 수 있도록 점진적인 훈련 방법을 채택했습니다. 이 프로세스에는 각각의 새로운 데이터 세트에 대한 점진적인 교육이 포함되어 안정성과 유연성의 최적 균형을 보장합니다.
이러한 종류의 점진적인 훈련을 통해 LeanAgent는 정리 증명에 탁월한 성능을 발휘하며, 특히 추상 대수 및 대수 위상학의 까다로운 정리에서 인간이 풀지 못한 162개의 어려운 문제를 성공적으로 증명했습니다. 새로운 정리를 증명하는 능력은 알려진 정리를 증명하는 능력을 유지하면서 정적 ReProver보다 11배 더 높습니다.
LeanAgent는 정리 증명 과정에서 점진적인 학습의 특징을 보여주며, 단순한 정리에서 복잡한 정리로 점진적으로 전환하여 수학적 지식 습득의 깊이를 입증합니다. 예를 들어 군론, 고리 이론과 관련된 기본적인 대수 구조 정리를 증명함으로써 수학에 대한 깊은 이해를 보여줍니다. 전반적으로 LeanAgent는 강력하고 지속적인 학습 및 개선 기능을 통해 수학 커뮤니티에 흥미로운 전망을 제공합니다!
논문 주소: https://arxiv.org/pdf/2410.06209
LeanAgent의 등장은 AI가 수학 연구 분야에서 점점 더 중요한 역할을 하게 될 것이며, 미래에는 복잡한 수학 문제를 해결하기 위해 AI의 힘을 활용하는 사례가 더 많아질 수 있음을 나타냅니다. 이는 의심할 여지없이 수학적 연구에 새로운 방향을 제시하고 다른 과학 분야의 탐구를 위한 새로운 아이디어와 방법을 제공합니다. 앞으로도 더욱 놀라운 결과를 기대합니다!