CertJudge: Evaluating Lean Formal-Code With Falsifiable Properties

Motivation

• Known: LLM-as-a-Judge는 코드, 테스트, 정리, 형식 명세 등 AI 생성물 평가에 광범위하게 사용되며, 신뢰도는 보통 human agreement(G-EVAL, MT-Bench, Judge-Bench 등)로 검증된다. 또한 position/verbosity bias, prompt phrasing 민감성 등 judge의 한계가 알려져 있고, ChatEval이나 구조화된 prompting(G-Eval) 같은 완화 기법이 존재한다.
• Gap: 새로운 judge, prompt, model, threshold가 등장할 때마다 human rating으로 재검증하는 것은 비용이 크고 확장성이 없으며, Lean 4 같은 agentic 정형 검증 환경에서는 Lean kernel의 type-checking만으로는 후보 theorem/specification이 완전한지, 의미적으로 gold와 일치하는지, 혹은 단순히 약한 statement인지 판단할 수 없다는 근본적 한계가 있다.
• Why: agent가 인간이 검사할 수 있는 속도보다 훨씬 빠르게 후보 형식 산출물을 생성하는 상황에서, judge의 신뢰도를 매번 human labeling 없이 확장 가능하게(scalable) 측정하는 방법은 scalable oversight 문제의 핵심이며, AI for math 및 formal verification 분야에서 agentic 시스템 평가의 병목을 해소할 수 있다.
• Approach: 고정된 human-labeled calibration panel(n=75)을 한 번만 사용해 네 가지 falsifiable behavioral property(식별성, 버그 단조성, 명세 단조성, 안정성)를 검증하는 controlled perturbation 기반 진단을 설계하고, 이를 geometric aggregation으로 결합한 TI_var라는 judge 신뢰도 요약 지표를 제안한다.

Achievement

Figure 3. TIvar vs. judge-level human alignment. Each point is one judge configuration; the x-axis is TIvar, and the y-a

1. amortized trust-validation protocol 제안: 고정된 Lean artifact panel에 대한 perturbation 기반 property certification을 일회성 calibration으로 정식화하여, 이후 새로운 judge 구성은 human labeling 없이 네 가지 falsifiable property만 계산해 스크리닝할 수 있게 했다.
2. n=75 규모의 proof-of-concept calibration 수행: TI_var가 진단들의 geometric aggregation으로서 human agreement를 잘 추적함을 검증셋에서 Spearman correlation 0.833(avg labels), 0.905(pass1), 0.738(pass2)로 보여주었다.
3. VeriBench에서의 end-to-end 활용: calibrated judge로 theorem-generation 방법들을 순위화하여(예: DSPy ReAct 0.615 vs baseline prompting 0.470, normalized specs 기준) benchmark 기대치와 일치하는 결과를 도출, 소규모 human calibration set이 scalable judge selection을 지원할 수 있음을 실증했다.

How

Figure 4. (P3) Monotonicity w.r.t. missing specifications. Candidate scores decrease as more theorems/tests are withheld

• 각 benchmark item은 자연어 문제 설명, gold Lean 4 artifact g, AI agent가 생성한 candidate artifact x로 구성되며, judge는 Jθ(x,g)∈[0,1] 점수를 산출한다(θ = model, prompt, nrepeats, aggregation로 파라미터화).
• n=75개의 aligned candidate-gold pair를 한 명의 annotator가 두 가지 rubric strictness level(pass1, pass2, avg labels 등)로 라벨링하여 고정 reference panel 구축.
• 새로운 judge 구성마다 인간 라벨을 다시 모으지 않고, Lean artifact에 대한 scripted perturbation을 적용해 네 가지 property score(P1 identity/consistency, P2 bug monotonicity, P3 specification monotonicity, P4 stability)를 계산.
• judge는 discrete score s∈{0,...,10}을 반환하며 [0,1]로 정규화되고, 네 property score를 결합해 variance-aware trust index TI_var를 산출.
• 8개의 judge configuration으로 구성된 panel에서 TI_var와 human-labeled judge-level alignment 간 Spearman correlation을 측정해 calibration 효과를 검증.
• VeriBench에서 calibrated judge를 사용해 theorem-generation 방법(DSPy ReAct, baseline prompting 등)의 순위를 매김.

Originality

• human agreement를 유일한 검증 신호로 삼는 기존 LLM-as-a-Judge 검증 관행과 달리, identity, bug monotonicity, specification monotonicity, stability라는 falsifiable behavioral property를 통해 human calibration을 일회성으로 amortize하는 프로토콜을 제안.
• metamorphic testing과 유사한 개념을 Lean 4 형식 코드/정리/명세 평가라는 새로운 도메인(agentic formal verification)에 적용.
• 단일 보편적 "evaluator constant"가 아니라, 판단 신뢰도를 도메인·judge별로 요약하는 variance-aware trust index(TI_var)라는 개념을 도입.

Limitation & Further Study

• calibration set이 n=75, 단일 annotator에 의한 라벨링으로 규모가 매우 작고, 통계적 유의성 및 annotator bias에 대한 우려가 있음.
• held-out human rater, 새로운 benchmark, 새로운 judge family로의 generalization은 저자들도 명시했듯 아직 검증되지 않은 future work임.
• TI_var의 geometric aggregation weighting이 고정된 최종 해법이 아니라 proof-of-concept 수준이며, 도메인이나 태스크가 바뀌면 재보정이 필요할 가능성이 있음.
• 8개 judge configuration만을 대상으로 한 panel 크기가 작아 상관계수의 robust성에 제한이 있을 수 있음.
• 후속 연구로는 더 큰 규모의 multi-annotator calibration, 다양한 도메인(코드, 자연어 등)으로의 확장, TI_var 가중치의 이론적 정당화 등이 필요함.

Evaluation

총평: scalable oversight라는 중요한 문제에 대해 falsifiable property 기반의 실용적이고 창의적인 접근을 제시했으나, calibration 규모가 작고 generalization 검증이 부족해 proof-of-concept 단계에 머무른다는 점에서 추가 검증이 필요한 초기 연구이다.