HF 해커톤 제출물

Build Small 해커톤을 위해 LLM 기반 형식 검증 (Formal Verification) 에이전트인 Q.E.D를 방금 출시했습니다.

작동 방식: Lean 4로 작성된 정리를 입력하면, 27B LLM을 사용하여 증명 전략 (Proof Tactics)을 제안합니다. 그 후 각 전략을 Lean의 형식 커널 (Formal Kernel)을 통해 검증하고, 커널의 오류를 다음 프롬프트에 다시 입력하는 과정을 정리를 증명하거나 증명 불가능하다고 결론 내릴 때까지 반복합니다.

핵심 사항: 커널은 속일 수 없습니다. "네, 그것은 참입니다"라고 말하는 챗봇과 달리, Lean은 증명을 수락하거나 거부합니다. 환각 (Hallucination)이 없습니다. 기계가 검증한 수학 (Machine-checked mathematics)입니다.

흥미로운 점:

• UI에서 실시간으로 확인 가능한 제안→검증→학습 (propose→verify→learn) 루프
• 모든 실패한 분기와 수락된 경로를 보여주는 커스텀 SVG 증명 트리 (Proof Tree)
• 정체 상태 탐지기 (Stuck-state detector) — 동일한 목표가 진전 없이 반복될 때, 무한 루프에 빠지는 대신 깔끔하게 "증명 불가능" 결론을 내림
• Modal 기반 구동 (지속적인 Lean REPL + LLM을 위한 온디맨드 GPU)

직접 시도해 보세요: https://huggingface.co/spaces/build-small-hackathon/QED
/u/hustla17 님이 제출함
[link] [comments]