|잡돌쌤•2026-03-23•2분 소요

기존 LLM 기반 접근과 단독 Sledgehammer를 크게 넘은 결과거든요

💡 한줄 요약|기존 LLM 기반 접근과 단독 Sledgehammer를 크게 넘은 결과거든요.

Stepwise가 시스템 검증 자동화에서 seL4 정리의 최대 77.6%를 증명했어요. 기존 LLM 기반 접근과 단독 Sledgehammer를 크게 넘은 결과거든요.

이 프레임워크는 신경망+기호 추론을 결합한 방식이에요. 증명 상태 트리를 best-first로 탐색하면서 LLM이 다음 증명 스텝 후보를 내고, 거절된 스텝은 ITP 도구로 복구해요.

또 proof state-step 데이터로 LLM을 파인튜닝하고, Isabelle REPL에서 세밀한 증명 상태를 노출해 필터링·랭킹·서브골 자동 해결까지 붙였어요. seL4뿐 아니라 추가 Isabelle 벤치마크에서도 일반화 성능을 보였어요.

의미는 분명해요. 대규모 소프트웨어 검증이 수작업 중심에서 자동 탐색 중심으로 넘어갈 현실적인 경로가 열리고 있다는 점이에요.

이 글이 어땠나요?

관련 글

논문은 두 축을 제안했어요

논문은 두 축을 제안했어요.

잡돌쌤2분 소요

연구팀은 지도 미세조정(SFT) 뒤에 멀티턴 프로세스-리워드 강화학습을 붙여, 멀티모달 LLM 에이전트를 학습시켰거든요

연구팀은 지도 미세조정(SFT) 뒤에 멀티턴 프로세스-리워드 강화학습을 붙여, 멀티모달 LLM 에이전트를 학습시켰거든요.

잡돌쌤2분 소요

arXiv 2603.19514(2026년 3월 19일 공개) 논문은 LLM을 미세조정해 반례를 만들고, 그 반례가 맞는지 Lean 4에서 자동 검증 가능한 형식 증명까지 함께 내게 했거든요

arXiv 2603.19514(2026년 3월 19일 공개) 논문은 LLM을 미세조정해 반례를 만들고, 그 반례가 맞는지 Lean 4에서 자동 검증 가능한 형식 증명까지 함께 내게 했거든요.

잡돌쌤2분 소요