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

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

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

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

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