형식적 검증을 이용한 자동 추론 해결

Automated Conjecture Resolution with Formal Verification

최근 대규모 언어 모델의 발전은 수학적 추론 능력을 크게 향상시켜, 초등 문제 해결에서부터 연구 수준의 문제 해결 능력까지 확장되었습니다. 그러나 자연어 추론의 고유한 모호성으로 인해, 이러한 문제들을 신뢰성 있게 해결하고 검증하는 것은 여전히 어려운 과제입니다. 본 논문에서는 자연어 추론과 형식적 검증을 통합하여 연구 수준의 수학 문제를 해결하는 자동화된 프레임워크를 제안합니다. 이 프레임워크는 최소한의 인간 개입으로 문제 해결을 가능하게 합니다. 제안하는 프레임워크는 두 가지 구성 요소로 이루어집니다. 첫 번째는 비형식적 추론 에이전트인 Rethlas이며, 두 번째는 형식적 검증 에이전트인 Archon입니다. Rethlas는 인간 수학자의 작업 흐름을 모방하며, 우리의 정리 검색 엔진인 Matlas를 활용하여 해결 전략을 탐색하고 후보 증명을 구성합니다. Archon은 우리의 형식적 정리 검색 엔진인 LeanSearch를 탑재하여, 구조화된 작업 분해, 반복적인 개선, 그리고 자동 증명 생성 과정을 통해 비형식적 논증을 형식화된 Lean 4 프로젝트로 변환하여, 기계가 검증할 수 있는 정확성을 보장합니다. 우리는 이 프레임워크를 사용하여 교환 대수학 분야의 미해결 문제를 자동으로 해결하고, 생성된 증명을 Lean 4에서 형식적으로 검증했습니다. 실험 결과는 강력한 정리 검색 도구가 다양한 분야의 수학적 기법을 발견하고 적용하는 데 기여하며, 형식적 에이전트는 비형식적 논증의 중요한 부분을 자율적으로 채울 수 있음을 보여줍니다. 더 넓은 의미에서, 우리의 연구는 정리 검색 도구를 갖춘 비형식적 및 형식적 추론 시스템이 상호 작용하여 검증 가능한 결과를 생성하고, 인간의 노력을 크게 줄이며, 인간-AI 협력 수학 연구의 구체적인 사례를 제공하는 유망한 패러다임을 보여줍니다.

Recent advances in large language models have significantly improved their ability to perform mathematical reasoning, extending from elementary problem solving to increasingly capable performance on research-level problems. However, reliably solving and verifying such problems remains challenging due to the inherent ambiguity of natural language reasoning. In this paper, we propose an automated framework for tackling research-level mathematical problems that integrates natural language reasoning with formal verification, enabling end-to-end problem solving with minimal human intervention. Our framework consists of two components: an informal reasoning agent, Rethlas, and a formal verification agent, Archon. Rethlas mimics the workflow of human mathematicians by combining reasoning primitives with our theorem search engine, Matlas, to explore solution strategies and construct candidate proofs. Archon, equipped with our formal theorem search engine LeanSearch, translates informal arguments into formalized Lean 4 projects through structured task decomposition, iterative refinement, and automated proof synthesis, ensuring machine-checkable correctness. Using this framework, we automatically resolve an open problem in commutative algebra and formally verify the resulting proof in Lean 4 with essentially no human involvement. Our experiments demonstrate that strong theorem retrieval tools enable the discovery and application of cross-domain mathematical techniques, while the formal agent is capable of autonomously filling nontrivial gaps in informal arguments. More broadly, our work illustrates a promising paradigm for mathematical research in which informal and formal reasoning systems, equipped with theorem retrieval tools, operate in tandem to produce verifiable results, substantially reduce human effort, and offer a concrete instantiation of human-AI collaborative mathematical research.