Meta AI가 2026년 10월 13일, AI 에이전트가 Lean 4에서 고급 수학을 형식화할 수 있는지 평가하는 벤치마크 AutoformBench를 공개했습니다. 벤치마크에는 고급 수학 자료 24곳에서 가져온 과제 341개가 포함됐습니다. Lean 사용 경험이 있는 수학자들이 각 목표 명제를 형식화하고 검토했으며, 평가 대상 에이전트는 Lean 증명을 작성하도록 했습니다.

각 AutoformBench 문제는 개별 정리 증명 시험과 달리 더 넓은 수학적 전개 안에 놓입니다. 에이전트는 비형식 증명을 받은 뒤 이를 Lean으로 옮기고, 결과를 형식화된 수학 라이브러리에 연결하는 데 필요한 정의와 중간 보조정리, 지원 구조를 만들어야 합니다. 연구진은 기존 평가에서 정리의 명제가 이미 Mathlib에 상당한 이론적 기반이 마련된 환경에 주어지는 경우가 많다고 설명했습니다.

연구진은 여러 최첨단 모델을 비교한 결과, 수학 분야 전반에서 대체로 공통된 성능 한계가 나타났다고 밝혔습니다. 성능은 주제 영역보다 모델이 누락된 형식 기반 구조를 구축하는 능력에 더 크게 좌우됐습니다. 데이터셋과 코드는 GitHub에서 이용할 수 있습니다.

Meta AI가 2026년 10월 13일, AI 에이전트가 Lean 4에서 고급 수학을 형식화할 수 있는지 평가하는 벤치마크 AutoformBench를 공개했습니다. 벤치마크에는 고급 수학 자료 24곳에서 가져온 과제 341개가 포함됐습니다. Lean 사용 경험이 있는 수학자들이 각 목표 명제를 형식화하고 검토했으며, 평가 대상 에이전트는 Lean 증명을 작성하도록 했습니다.

각 AutoformBench 문제는 개별 정리 증명 시험과 달리 더 넓은 수학적 전개 안에 놓입니다. 에이전트는 비형식 증명을 받은 뒤 이를 Lean으로 옮기고, 결과를 형식화된 수학 라이브러리에 연결하는 데 필요한 정의와 중간 보조정리, 지원 구조를 만들어야 합니다. 연구진은 기존 평가에서 정리의 명제가 이미 Mathlib에 상당한 이론적 기반이 마련된 환경에 주어지는 경우가 많다고 설명했습니다.

연구진은 여러 최첨단 모델을 비교한 결과, 수학 분야 전반에서 대체로 공통된 성능 한계가 나타났다고 밝혔습니다. 성능은 주제 영역보다 모델이 누락된 형식 기반 구조를 구축하는 능력에 더 크게 좌우됐습니다. 데이터셋과 코드는 GitHub에서 이용할 수 있습니다.