MECA: 메커니즘 중심 에이전트를 활용한 잘 정의되고 가치 있는 수학적 추론 생성

MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures

잘 정의되고 가치 있는 수학적 추론을 자동으로 생성하는 것은 인공지능 기반의 수학적 발견 분야에서 핵심적인 과제입니다. 많은 기존 문제와 추론은 종종 너무 광범위하거나, 명확하게 정의되지 않았거나, 합리적인 증명 또는 반증 전략과 연결하기 어렵습니다. 본 연구에서는 수학적 메커니즘을 후보 문제의 가정과 목표 결론(예: 부등식, 불변량, 분해, 중간 주장에 대한 환원)을 연결하는 구조 또는 추론 원칙으로 간주합니다. MECA (MEchanism-centered Conjecture Agent)는 후보 명제와 이를 뒷받침하는 메커니즘을 공동으로 개발하여 추론을 생성하는 다중 에이전트 프레임워크입니다. 탐색 에이전트는 메커니즘을 제안하고, 그 적용 가능성을 테스트하며, 이에 따라 후보 추론을 수정합니다. 반면, 비평 에이전트는 해당 추론의 수학적 타당성과 연구 가치를 평가합니다. 이러한 피드백은 가정, 범위 및 결론에 대한 변경 사항을 안내합니다. 이 과정을 통해 MECA는 광범위한 연구 방향을 명확하고 실질적인 수학적 근거를 갖춘 정확한 추론으로 변환하면서도 여전히 해결되지 않은 핵심 내용을 유지합니다. 본 연구에서는 두 가지 상호 보완적인 환경에서 MECA를 평가했습니다. 첫째, MECA를 기존의 생성-수정 방식과 비교하여, 목표 논문의 결론을 재구성하는 성능을 평가했습니다(단, 논문 내용은 숨겨진 상태). 둘째, 문헌 기반의 초기 정보와 기존 미해결 문제로부터 100개의 준미결 문제를 구성하고, 자동 증명기를 사용하여 독립적인 증명 및 반증 시도를 통해 그 타당성을 평가했습니다. 연구 결과는 메커니즘 중심의 정제가 잘 정의되고 가치 있는 추론을 생성하며, 이러한 추론은 현재의 자동 증명기로는 해결하기 어렵다는 것을 보여줍니다.

Automatically constructing well-specified and valuable mathematical conjectures remains a central challenge in AI-assisted mathematical discovery. Many existing open problems and conjectures are often too broad, underspecified, or difficult to connect to plausible proof or refutation strategies. We view a mathematical mechanism as a structure or reasoning principle that connects the assumptions of a candidate problem to its target conclusion, such as an inequality, invariant, decomposition, or reduction to an intermediate claim. We present MECA (MEchanism-centered Conjecture Agent), a multi-agent framework that constructs conjectures by jointly developing candidate statements and their supporting mechanisms. Explorer agents propose mechanisms, test how they apply, and revise the candidate conjecture accordingly, while critic agents assess their mathematical validity and research value. Their feedback guides changes to the assumptions, scope, and conclusion. Through this process, MECA transforms broad research directions into precise conjectures with substantive mathematical support while retaining a clearly identified unresolved core. We evaluate MECA in two complementary settings. First, we compare it with a generate-and-revise baseline on reconstructing preselected target-paper conclusions from target-conditioned but article-blind source materials. Second, we construct 100 semi-open problems from literature-derived seeds and existing open problems and evaluate them through independent proof and refutation attempts by automated provers. Our results indicate that mechanism-centered refinement produces well-specified and research-worthy conjectures that remain challenging for current automated provers.