Sign In

Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4

μž‘μ„±μž
  • Haebom
μΉ΄ν…Œκ³ λ¦¬
Empty

μ €μž

Austin Shen, Yunong Shi

πŸ’‘ κ°œμš”

λ³Έ 논문은 Lean 4 기반 μžλ™ 정리 증λͺ… μ‹œμŠ€ν…œμ—μ„œ 병렬 μ „μˆ  검색 μ‹œ λ°œμƒν•˜λŠ” λΉ„νš¨μœ¨μ μΈ 증λͺ… μƒνƒœ μž¬κ΅¬μ„± 문제λ₯Ό ν•΄κ²°ν•˜κ³ μž ν•©λ‹ˆλ‹€. 이λ₯Ό μœ„ν•΄, ν•œ 번만 증λͺ… μƒνƒœλ₯Ό μΊ‘μ²˜ν•˜μ—¬ μ—¬λŸ¬ 탐색 λΆ„κΈ°μ—μ„œ μž¬μ‚¬μš©ν•˜λŠ” '증λͺ… μƒνƒœ μŠ€λƒ…μƒ·νŒ…' 기법을 μ œμ•ˆν•©λ‹ˆλ‹€. μ œμ•ˆ 기법은 κΈ°μ‘΄ 방식 λŒ€λΉ„ 5.6λ°°μ—μ„œ 50λ°°κΉŒμ§€ μ„±λŠ₯을 ν–₯μƒμ‹œν‚€λ©°, 특히 탐색 λΆ„κΈ° μˆ˜κ°€ λ§Žμ„μˆ˜λ‘ νš¨κ³Όκ°€ μ¦λŒ€λ©λ‹ˆλ‹€.

πŸ”‘ μ‹œμ‚¬μ  및 ν•œκ³„

β€’
Lean 4 기반 μžλ™ 정리 증λͺ… μ‹œμŠ€ν…œμ˜ 병렬 탐색 μ„±λŠ₯을 획기적으둜 κ°œμ„ ν•  수 μžˆμŠ΅λ‹ˆλ‹€.
β€’
증λͺ… μƒνƒœ μž¬κ΅¬μ„± μ˜€λ²„ν—€λ“œλ₯Ό 쀄여 λŒ€κ·œλͺ¨ 포트폴리였 기반 νƒμƒ‰μ˜ μ‹€μš©μ„±μ„ λ†’μž…λ‹ˆλ‹€.
β€’
κΈ°μ‘΄ import 레벨 μΊμ‹±κ³ΌλŠ” μƒν˜Έ 보완적인 관계λ₯Ό κ°€μ§‘λ‹ˆλ‹€.
β€’
μ œμ•ˆλœ μ–Έμ–΄ μ„œλ²„ ν™•μž₯ 및 patched Lean binary 배포가 ν•„μš”ν•˜λ©°, ν–₯ν›„ 더 λ³΅μž‘ν•œ 증λͺ… κ΅¬μ‘°μ—μ„œμ˜ νš¨μœ¨μ„± 검증이 ν•„μš”ν•  수 μžˆμŠ΅λ‹ˆλ‹€.
πŸ‘
Made with Slashpage