사람의 풀이 개요가 자동 증명기의 길잡이가 될 수 있을까?
Jiang 등은 488개 miniF2F 문제에서 비형식 풀이→형식 스케치→자동 증명의 세 단계를 결합해 Isabelle 검증 성공률을 높였습니다.
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
연구와 학습, 시험과 도서를 한곳에서 찾습니다.
검색 결과마다 자료의 코너와 성격을 표시합니다. 제목을 먼저 살펴보고 그림 카드와 기존 본문으로 이어 가세요.

관심 주제로 찾아보기
Jiang 등은 488개 miniF2F 문제에서 비형식 풀이→형식 스케치→자동 증명의 세 단계를 결합해 Isabelle 검증 성공률을 높였습니다.
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
Kimina-Prover Preview v1의 강화학습과 miniF2F pass@8192 결과를 살펴보며 대규모 후보 탐색 성과와 단일 시도 능력, 형식 검증 비용을 구분한다.
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
자기일관성 방법은 다양한 풀이 경로에서 최종 답을 모읍니다. 정답률 개선과 답의 논리적 보증을 구별하고, 반복 답변의 독립성도 따져 봅니다.
Self-Consistency Improves Chain of Thought Reasoning in Language Models
생각의 나무는 중간 풀이를 여러 갈래로 만들고 평가하여 탐색합니다. 유망하다는 판단과 실제 정답 검사는 따로 보아야 합니다.
Tree of Thoughts: Deliberate Problem Solving with Large Language Models
RobustLR는 최소 논리 편집과 동치 변환으로 연역 모델의 일관성을 검사했고, 학습된 모델들이 특히 부정에서 흔들림을 보였습니다.
RobustLR: A Diagnostic Benchmark for Evaluating Logical Robustness of Deductive Reasoners
26–30 / 67편