저자: Austin Letson, Leopoldo Sarra, Auguste Poiroux, Oliver Dressler, Paul Lezeau, Dhyan Aranha, Frederick Pu, Aaron Hill, Miguel Corredera Hidalgo, Julian Berman, George Tsoukalas, Lenny Taelman | 날짜: 2026 | URL: https://openreview.net/forum?id=hcO7EwDTL5 📄 PDF
Essence
Figure 1. Dataset extraction pipeline for SorryDB. We consider 78
SorryDB는 78개의 실제 GitHub Lean 정형화 프로젝트에서 추출한 미해결 sorry를 기반으로 동적으로 업데이트되는 벤치마크로, 경쟁 수학 문제 중심의 기존 정적 벤치마크와 달리 실제 커뮤니티 요구에 부합하는 자동 정리 증명기의 실용성을 평가한다.
Evaluation
Novelty: 4/5 Technical Soundness: 4/5 Significance: 5/5 Clarity: 4/5 Overall: 4/5
총평: 실제 정형화 커뮤니티의 요구를 직접 반영하는 동적 벤치마크를 제안하여 정리 증명 분야의 오염 및 포화 문제를 해결하려는 시의적절하고 실용적인 기여이며, 다양한 접근법의 상호보완성을 밝힌 평가 분석이 향후 연구 방향에 유의미한 시사점을 제공한다.
같이 보면 좋은 논문
기반 연구SPECTER2 유사도 0.95로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Fimo: A challenge formal dataset for automated theorem proving'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
기반 연구SPECTER2 유사도 0.94로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Towards large language models as copilots for theorem proving in lean'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
기반 연구SPECTER2 유사도 0.94로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
기반 연구agentic theorem proving 워크플로우를 확장하거나 개선하는 후속 연구로 판단됨
기반 연구dependency graph 기반 local-global 검증 개념을 확장하는 연구이다.
기반 연구Lean 4 정리증명을 위한 인프라/도구를 실제 agentic training 시나리오에 적용하는 관계이다.
기반 연구AI 기반 수학 정리 증명 인프라를 확장하는 연구이다.
기반 연구동적으로 업데이트되는 벤치마크 설계의 기초를 제공한다.
기반 연구self-improving 전략 메모리 개념을 확장한 연구
기반 연구실제 PR 히스토리 기반 평가라는 점에서 formal verification 시스템에 대한 응용 사례로 볼 수 있다.
기반 연구AI 기반 수학 연구 워크플로우를 확장한다.
다른 접근formal theorem proving을 위한 에이전트 시스템의 대안적 구현을 제시한다.
다른 접근도메인 특화 LLM 에이전트 벤치마크 구축이라는 동일한 문제를 다룸
다른 접근LLM의 장기 추론 능력 평가라는 유사한 목표를 다른 벤치마크로 접근한다.
다른 접근Mizar에서 다른 시스템으로의 증명 이식이라는 구체적 문제를 공유한다.
다른 접근Mathlib 등 실제 수학 라이브러리를 이용한 유사한 벤치마크 구축
다른 접근Lean 기반 정리 증명에서 다른 접근으로 후보 생성 문제를 다룸
후속 연구동적 벤치마크 개념을 확장하여 실제 커뮤니티 요구를 반영한 연구이다.
다른 접근수학 추론 모델 평가를 다른 벤치마크 구조로 접근
다른 접근구조화된 데이터에서 탐색적 통찰 추출 능력을 평가하는 유사한 벤치마크 접근법을 다룬다.
다른 접근LLM을 활용해 연구 문헌을 구조화하는 유사한 접근을 다른 방식으로 시도한 연구로 판단됨
응용 사례LLM 기반 증명 시스템의 실제 적용 사례를 다룬다.
다른 접근Lean proof 최적화를 위한 다른 retrieval-augmented 접근으로 보임
다른 접근자동 정리 증명기의 실용성을 다른 벤치마크로 평가한다.
후속 연구library-grounded proof 평가 방법론의 기반이 되는 연구로 보임
다른 접근Lean 프로젝트 자동 생성의 대안적 방법론을 제시한다.
다른 접근수학 정리 증명 벤치마크를 위한 다른 데이터 구성 방식을 제시한다.
후속 연구언어모델의 논리적 반증 능력에 대한 이론적 기초를 제공한다.
후속 연구correctness 외 다양한 평가 척도의 이론적 기초
후속 연구LLM 기반 증명 검증의 이론적 기반을 제공함
후속 연구LLM 기반 검증 가속화의 이론적 기반
후속 연구agentic prover의 구성요소별 성능 분석의 기초가 되는 연구
후속 연구정리 증명 에이전트의 기반이 되는 형식 증명 방법론을 제공한다.
후속 연구정리 증명 벤치마크 및 형식화 방법론의 기초를 제공한다.
후속 연구ReAct 스타일 에이전트 프레임워크의 방법론적 기반이 되는 연구이다.
후속 연구실제 Lean 프로젝트 기반 sorry 완성 작업을 확장한다.
후속 연구Lean 커널 인증 기반 검증 절차의 방법론적 토대를 제공하는 것으로 보임
