Essence
Figure 1. COVCAL treats Lean as a partial-observation judge: accept a Lean-backed answer only when the formal trace has
Lean 기반 증명 신호가 자연어 수학 답 선택에서 부분적(partial)이고 coverage에 크게 의존한다는 것을 보이고, 이를 반영해 accepted 답에 대해 finite-sample selective-risk 인증서를 제공하는 selector인 COVCAL을 제안한다.
Evaluation
Novelty: 4/5 Technical Soundness: 4/5 Significance: 3/5 Clarity: 4/5 Overall: 4/5
총평: Lean 증명 신호의 신뢰성이 coverage에 크게 좌우된다는 현상을 실증적으로 밝히고 이를 통계적으로 인증하는 selective-risk 프레임워크를 제안한 점에서 개념적으로 참신하고 시의적절한 워크숍 논문이나, 실용적 성능 우위보다는 진단적·분석적 기여에 초점이 맞춰져 있어 추가 검증과 확장이 필요하다.
같이 보면 좋은 논문
기반 연구SPECTER2 유사도 0.94로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Fimo: A challenge formal dataset for automated theorem proving'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
기반 연구SPECTER2 유사도 0.93로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Lean-star: Learning to interleave thinking and proving'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
기반 연구SPECTER2 유사도 0.93로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Grammars of formal uncertainty: When to trust llms in automated reasoning tasks'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
기반 연구counterfactual 검증을 형식 증명 탐색에 확장 적용
기반 연구Lean 검증 가능한 반례 생성 기법을 다른 도메인으로 확장한 연구이다.
기반 연구Isabelle 환경에서의 실제 증명 성능 향상에 적용된 사례이다.
기반 연구informal reasoning과 formal proof 결합 방법을 확장한 연구이다.
기반 연구Lean 4/Mathlib 기반 평가 벤치마크를 확장하는 연구로 판단됨.
기반 연구grind 검색 알고리즘의 개입 시점을 확장하여 다룬다.
기반 연구재사용 가능한 계산 구조 발견을 확장한 관련 연구이다.
다른 접근formal proof 신호를 활용한 답 선택 문제의 다른 접근이다.
다른 접근자연어 수학 답 선택에서 형식적 증명 신호를 활용하는 대안적 검증 방법을 제시한다.
다른 접근형식 검증 가능한 반례 생성이라는 유사한 목표를 가진 접근이다.
다른 접근수학적 증명 기반 답변 선택 문제와 관련된 유사 연구이다.
후속 연구선택적 위험(selective risk) 제어 프레임워크를 수학적 답 선택 문제로 확장한다.
후속 연구axiom dependency tracking을 통한 증명 분석의 이론적 기초를 제공함
응용 사례LLM 기반 수학 추론 검증에 conformal-style risk 인증서를 적용한 사례이다.
