Tacit Verification Apprenticeship for Self-Evolving Scientific Agents

Motivation

• Known: Lean/Lean 4와 같은 formal substrate, retrieval-augmented proving, LLM 기반 autoformalization, semantic-alignment 검사, proof repair, 그리고 cognitive apprenticeship 이론 등 각각의 요소 기술들은 이미 개별적으로 연구되어 있다.
• Gap: 기존 연구들은 formal artifact 생성이나 검증 도구 호출에 초점을 맞추고 있지만, 이 도구들을 실제로 능숙하게 다루는 데 필요한 암묵적(tacit) 전문가 노하우—정의 선택, 증명 의무 분할, 실패 진단 및 수리, 형식적으로는 맞지만 의미적으로 틀린 결과를 감지하는 능력—을 학습 대상으로 삼는 agent 아키텍처는 부재하다.
• Why: 형식적으로 accept된 artifact가 과학적으로 misaligned될 수 있다는 문제는 단순 hallucination보다 더 근본적인 신뢰성 위험이며, self-evolving scientific agent가 여러 cycle에 걸쳐 검증 가능하고(auditable) 의미적으로 충실한(semantically faithful) 방식으로 개선되도록 하는 것은 AI4Math 및 과학적 AI agent 분야의 핵심 과제이다.
• Approach: 저자들은 Tacit Verification Bottleneck을 개념적으로 정의하고, 5개 구성요소(Formalization Apprenticeship Agent, Proof/Validation Repair Memory, Tacit Skill Compiler, Semantic Alignment Sentinel, Domain Verification Apprentice)로 이루어진 TVA 아키텍처와 utility model, failure taxonomy, benchmark 설계를 제시한 뒤 1,406개의 curated record로 세 가지 corpus probe와 실행 가능한 semantic-alignment demo를 통해 이를 검증한다.

Achievement

Figure 3. Experiment 1: mean craft-similarity profiles for the dedu-

1. Tacit Verification Bottleneck 정의: formal artifact와 이를 만들고 진단·수리·전이하는 데 필요한 craft 사이의 간극을 공식적으로 개념화했다.
2. TVA 아키텍처 제안: 다섯 개 모듈로 구성된 apprenticeship 기반 architecture와 typed memory schema, skill utility 함수(수식 1-3), failure diagnosis, repair selection, transfer gating 알고리즘을 제시했다.
3. ApprenticeshipBench-SESA 벤치마크 설계: formal math, semantic alignment, proof repair, executable scientific spec, domain validation을 아우르는 평가 체계를 제안했다.
4. 경험적 probe 결과: craft 차원이 corpus에서 recoverable함을 보였고, apprenticeship retrieval이 process annotation으로 개선되며, repair-memory transfer는 명시적 gate가 필요하고, sentinel이 semantic disagreement를 repair나 abstention으로 전환할 수 있음을 세 가지 corpus probe와 semantic-sentinel demo로 입증했다.

How

Figure 2. Deduplicated top-cluster corpus used for the experiments.

• Tacit Verification Bottleneck을 정의하고, 손실되는 정보(설계 근거, 기각된 정의, 실패한 tactic, 암묵적 side condition, 라이브러리 탐색 경로, alignment 의심, counterexample, domain-risk 판단)를 명세
• 각 skill si를 precondition, postcondition, failure signature, repair operator, provenance, transfer boundary와 함께 저장
• utility 함수 U(si; Gt, Dt, Kt)를 psucc, rrepair, fsem, vreuse, τtransfer, cverify, bbrittle, risk(Dt)의 가중합으로 정의하고 hard transfer gate 적용
• Table 1에 정리된 10가지 tacit craft type(statement design, definition choice, lemma decomposition, library navigation, tactic selection, proof repair, semantic alignment, executable spec, domain formalization, failure distillation)마다 observable trace와 feedback signal을 매핑
• 5개 아키텍처 컴포넌트(Formalization Apprenticeship Agent, Proof/Validation Repair Memory, Tacit Skill Compiler, Semantic Alignment Sentinel, Domain Verification Apprentice)를 설계
• 1,406개 curated record의 deduplicated corpus(Fig 2)에 대해 craft-similarity profile 분석(Experiment 1), retrieval ablation(Experiment 2), repair-memory ablation(Experiment 3)을 수행하고 executable semantic-alignment demo로 sentinel 동작을 시연

Originality

• 기존 formal verification/autoformalization 연구가 명시적 artifact 생성에 집중한 것과 달리, 검증 과정의 "암묵적" 전문가 craft를 학습 대상으로 명시적으로 정식화했다는 점이 독창적이다.
• cognitive apprenticeship 이론(Collins et al.)을 형식 증명·과학적 검증 workflow에 적용하여, 실패를 noise가 아닌 1차 학습 신호(negative evidence)로 취급하는 관점을 제시한다.
• 형식적으로 accepted되었으나 과학적으로 misaligned된 artifact를 탐지하는 Semantic Alignment Sentinel이라는 별도 모듈을 통해 syntactic success와 semantic success를 명시적으로 분리한 설계가 새롭다.
• transfer boundary를 명시적으로 gate하는 utility 함수 설계는 skill 재사용의 무분별한 일반화를 방지하는 실용적 장치이다.

Limitation & Further Study

• 제시된 것은 architecture와 evaluation agenda 수준의 blueprint이며, 실제 대규모 LLM agent에 통합되어 end-to-end로 검증된 시스템 성능(SOTA 대비 정량적 개선)은 제한적으로만 보고된다(1,406개 record 규모의 corpus probe 수준).
• utility 함수의 각 계수(α, β, γ, δ, η, λ, µ, ρ)를 어떻게 학습·튜닝하는지에 대한 구체적 방법론이 충분히 제시되지 않아 재현성에 의문이 남는다.
• 세 가지 corpus probe가 formal math 도메인에 편중되어 있어 causal, finance, bioinformatics 등 다양한 domain으로의 실제 일반화 가능성은 추가 검증이 필요하다.
• 후속 연구로 대규모 실제 self-evolving agent 배포 환경에서의 장기적 craft 축적 및 catastrophic forgetting 방지 메커니즘에 대한 실증 연구가 필요하다.

Evaluation

총평: Formal verification 도구를 다루는 데 필요한 암묵적 전문가 craft를 학습 대상으로 정식화한 개념적 기여가 인상적이지만, 이를 뒷받침하는 실증 결과는 소규모 corpus probe 수준에 머물러 있어 실제 대규모 self-evolving scientific agent 시스템으로서의 완성도는 향후 연구를 통해 더 검증되어야 한다.