Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics

개방적이고 범용적인 에이전트 추론 시스템 Numina-Lean-Agent는 형식적 수학 추론을 수행하기 위해 범용 코딩 에이전트를 활용한다.

개방적이고 범용적인 에이전트 추론 시스템 Numina-Lean-Agent는 형식적 수학 추론을 수행하기 위해 범용 코딩 에이전트를 활용한다. 이 시스템은 Putnam 2025 벤치마크의 12개 문제를 모두 풀어 최첨단 성능을 달성했으며, 잘못된 형식 진술문을 자율적으로 수정하는 것을 포함해 Brascamp-Lieb 정리를 형식화함으로써 대규모 협업 역량을 입증했다.

핵심 요약

• 기존 에이전트 정리 증명 시스템은 광범위하게 학습된 형식 증명기와 긴밀히 결합된 과제 특화 추론 파이프라인에 종종 의존한다.
• 고성능 자동 정리 증명기 다수가 폐쇄형이어서 투명성, 재현성, 그리고 더 넓은 커뮤니티 발전이 제한된다.
• 기존의 단일 모델 접근법은 Lean과 같은 복잡한 형식 체계에 내재된 장기 시야의 구조적 추론에 어려움을 겪었다.
• 범용 코딩 에이전트, 구체적으로 Claude Code가 형식적 수학 추론의 중앙 오케스트레이터 역할을 하는 패러다임을 제안했다.
• Claude Code를 포괄적인 모델 컨텍스트 프로토콜(Numina-Lean-MCP)과 통합하는 개방적이고 모듈형인 시스템 Numina-Lean-Agent를 개발했다.
• Numina-Lean-MCP는 Lean과의 심층 상호작용(Lean-LSP-MCP), 의미 기반 정리 검색(LeanDex), 반복적 비형식 증명(Gemini Generator/Verifier), 다중 모델 협업(Discussion Partner)을 위한 특화 도구를 포함한다.

논문 링크

외부 연구를 정리한 자료입니다. HDATF가 발표한 논문이나 제품 성능을 측정한 결과는 아닙니다.