발견하고 증명하다: Lean 4 환경에서 어려운 자동 정리 증명 작업을 위한 오픈 소스 에이전트 기반 프레임워크

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4

대부분의 자동 정리 증명(ATP) 벤치마크는 정답을 형식적인 명제 안에 포함하고 있는데, 우리는 이를 "쉬운 모드"라고 부릅니다. 이러한 설계는 인간 경쟁자가 직면하는 작업보다 단순하며, 모델의 능력을 지나치게 낙관적으로 평가할 수 있습니다. 우리는 더욱 엄격하고 현실적인 환경을 "어려운 모드"라고 정의합니다. 이 모드에서는 시스템이 정답을 독립적으로 발견한 후에 형식적인 증명을 구성해야 합니다. 어려운 모드 연구를 지원하기 위해, 우리는 다음과 같은 두 가지 기여를 합니다. 첫째, 널리 사용되는 두 가지 ATP 벤치마크의 어려운 모드 변형인 MiniF2F-Hard 및 FIMO-Hard를 공개합니다. 둘째, LLM의 자연어 추론과 명시적인 자기 성찰을 사용하여 정답을 발견하고, 기존의 ATP 증명기가 처리할 수 있도록 어려운 모드 명제를 쉬운 모드 명제로 변환하는 에이전트 기반 프레임워크인 Discover And Prove (DAP)를 소개합니다. DAP는 현재 최고 수준의 성능을 보입니다. CombiBench에서는 해결된 문제의 수를 7개(이전 최고 성능, Pass@16)에서 10개로 증가시켰습니다. PutnamBench에서는 처음으로 36개의 정리를 어려운 모드에서 형식적으로 증명했습니다. 동시에, 최첨단 LLM이 동일한 문제에서 80% 이상의 정확도를 보이는 반면, 형식적 증명기는 10% 미만의 성능을 보이는 것을 보여주며, 어려운 모드 벤치마크가 이러한 격차를 측정하는 데 독특하게 적합하다는 것을 드러냅니다.

Most ATP benchmarks embed the final answer within the formal statement -- a convention we call "Easy Mode" -- a design that simplifies the task relative to what human competitors face and may lead to optimistic estimates of model capability. We call the stricter, more realistic setting "Hard Mode": the system must independently discover the answer before constructing a formal proof. To enable Hard Mode research, we make two contributions. First, we release MiniF2F-Hard and FIMO-Hard, expert-reannotated Hard Mode variants of two widely-used ATP benchmarks. Second, we introduce Discover And Prove (DAP), an agentic framework that uses LLM natural-language reasoning with explicit self-reflection to discover answers, then rewrites Hard Mode statements into Easy Mode ones for existing ATP provers. DAP sets the state of the art: on CombiBench it raises solved problems from 7 (previous SOTA, Pass@16) to 10; on PutnamBench it is the first system to formally prove 36 theorems in Hard Mode -- while simultaneously revealing that state-of-the-art LLMs exceed 80% answer accuracy on the same problems where formal provers manage under 10%, exposing a substantial gap that Hard Mode benchmarks are uniquely suited to measure.