Recurrence: An Evolving Research-State Copilot for Mathematics

Motivation

• Known: 최근 AI-for-math 연구(Aletheia, QED, Rethlas/Archon, Aristotle, AlphaGeometry, FormalProofBench 등)는 statement가 주어지면 proof를 generate-check-revise하는 단일 proof obligation 문제로 theorem proving을 프레이밍하며, prover/formalizer layer에서 빠른 진전을 보이고 있다.
• Gap: 기존 시스템들은 최종 proof text 생성에 집중할 뿐, 정확한 statement 고정, 반례 탐색, 실패한 경로의 기억, 재사용 가능한 lemma 추출, 다음 공략 대상 결정 등 실제 수학 연구를 지탱하는 주변 상태(research state)를 다루지 않는다는 연구 공백이 존재한다.
• Why: 수학 연구의 실질적 병목은 단일 proof 생성이 아니라 관련 문제들 사이에서 안정적인 상태(statement, counterexample, failed route, verifier judgment, next step)를 유지하는 것이므로, 이 layer를 다루는 것은 AI-assisted mathematical research의 장기적 생산성에 직접적으로 기여할 수 있다.
• Approach: Recurrence는 proof-and-verification pipeline에 pre-proof layer를 추가하여 target statement를 잠그고(lock), exploratory mapping과 direct attack을 분리하며, proof-side/disproof-side route를 동시에 유지하고, adversarial verification으로 claim에 라벨을 부여하며, 이후 run을 안내하는 memory item을 저장하는 방식으로 동작한다.

Achievement

1. Locked-statement 연구 하니스 제안: statement drift를 방지하고 fragile mathematical target을 안정적으로 유지하는 locked-statement discipline을 도입했다.
2. Explore/Attack 이원 모드: 문제를 공략하기 전 인접한 positive/negative conjecture를 탐색하는 explore mode와 proof/disproof method를 동시에 열거하는 attack mode를 분리하여 proof-side와 disproof-side 압력을 모두 가시화했다.
3. Artifact contract 정의: target card, branch ledger, no-output note, drift check, claim map, memory item, return map 등 6종의 artifact를 통해 hallucinated success, opaque proof blob, statement drift 등을 방지하는 계약(Table 1)을 제시했다.
4. Non-parametric self-evolution 프레임 제시: 모델 가중치 업데이트 없이 research state, prompt, memory만 진화시키는 proto-evolutionary scientific agent 개념을 구체화했다.
5. Gompf 문제 목록 기반 cluster-benchmark 파일럿: 22개 target으로 구성된 Gompf problem list를 이용해 topology 캠페인 및 클러스터 벤치마크 프로토콜을 시범 적용하고 obstruction 보존, 허위 해 주장 회피, human-checkable next step 산출을 정성적으로 제시했다.

How

• Pre-proof 단계에서 문제를 의미 변경 없이 재서술(rephrase)하고 hypothesis와 conclusion을 분리, quantifier와 성공 기준(success criteria)을 명시
• Explore mode와 Attack mode 중 선택: Explore는 인접한 conjecture 지형을 매핑, Attack은 proof/disproof method를 동시에 enumerate
• 모든 branch를 direct progress, reduction, obstruction, finite evidence, side result, dead end 중 하나로 분류하고 항상 원래 target으로 "recur"하도록 강제
• Whole-proof verification과 statement-drift check를 통해 artifact honesty와 theorem truth를 구분
• 실패한 route를 failure ledger, no-output decision, warning으로 변환하여 memory item으로 저장, 이후 run이 이를 상속
• Verifier가 각 claimed lemma에 Yes/No/Uncertain 라벨을 부여하며 Uncertain은 최종 결과로 승격되지 않음
• topology 중심 파일럿 run과 22-target Gompf problem list 기반 cluster-benchmark 프로토콜로 평가

Originality

• 기존 연구가 거의 전적으로 prover/formalizer layer(최종 proof 생성 및 검증)에 집중한 반면, 본 논문은 그 이전 단계인 pre-proof/research-state layer를 명시적 대상으로 삼은 점이 독창적이다.
• Reflexion, Voyager 등 일반 에이전트의 memory/lesson 축적 패턴을 conjecture, reduction, obstruction, claim map, return map 등 수학 연구 특유의 객체로 특화(specialize)한 점이 새롭다.
• "self-evolving"을 model weight 업데이트가 아닌 non-parametric, process-level(state, prompt, memory) 진화로 재정의하여 proto-evolutionary scientific agent라는 개념적 위치를 제시한 점이 흥미롭다.
• Poincaré, Tao의 수학적 직관과 formalism에 관한 철학적 논의를 AI 에이전트 설계 원칙(locked-statement, explore/attack)으로 구체화한 접근이 독창적이다.

Limitation & Further Study

• 발췌된 본문에서 정량적 평가 지표나 baseline 대비 성능 비교가 명확히 제시되지 않아 "false solution claim 회피", "human-checkable next step 산출"과 같은 주장이 파일럿 수준의 정성적 증거에 머무를 가능성이 크다.
• 22-target Gompf problem list라는 특정 도메인(topology)에 국한된 평가로, 다른 수학 분야(대수, 해석학 등)로의 일반화 가능성이 검증되지 않았다.
• Memory item과 verifier label의 정확성 자체가 결국 LLM의 신뢰도에 의존하므로, adversarial verification이 실제로 얼마나 견고한지에 대한 정량적 검증이 부족해 보인다.
• 후속 연구로는 다양한 수학 분야에 대한 확장 평가, 인간 수학자 평가자와의 inter-rater reliability 측정, memory 축적에 따른 장기적 성능 향상 곡선 제시가 필요하다.

Evaluation

총평: Proof 생성이라는 좁은 목표를 넘어 수학 연구의 상태 관리라는 실질적이지만 저평가된 문제를 다룬 시의적절하고 개념적으로 흥미로운 워크숍 논문이나, 제시된 평가는 파일럿 수준에 머물러 있어 정량적 검증과 다양한 도메인으로의 확장이 향후 설득력을 좌우할 것으로 보인다.