Sign In

Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations

Created by
  • Haebom
Category
Empty

μ €μž

Hita Kambhamettu, Will Crichton, Sean Welleck, Harrison Goldstein, Andrew Head

πŸ’‘ κ°œμš”

λ³Έ μ—°κ΅¬λŠ” LLM이 μƒμ„±ν•œ 정적인 ν…μŠ€νŠΈ μ„€λͺ…μ˜ ν•œκ³„λ₯Ό κ·Ήλ³΅ν•˜κΈ° μœ„ν•΄, μˆ˜ν•™ 정리와 증λͺ…을 Leanμ΄λΌλŠ” 기계 검증 증λͺ… ν”„λ‘œκ·Έλž˜λ° μ–Έμ–΄λ‘œ λ³€ν™˜ν•˜λŠ” "탐색 κ°€λŠ₯ν•œ 정리(explorable theorems)" μ‹œμŠ€ν…œμ„ μ œμ•ˆν•©λ‹ˆλ‹€. 이 μ‹œμŠ€ν…œμ€ λ…μžλ“€μ΄ 증λͺ…μ˜ 각 단계λ₯Ό λ‹¨κ³„λ³„λ‘œ νƒμƒ‰ν•˜κ³ , μ‚¬μš©μž μ •μ˜ μ˜ˆμ œλ‚˜ λ°˜λ‘€λ₯Ό ν…ŒμŠ€νŠΈν•˜λ©°, 논리적 μ˜μ‘΄μ„±μ„ 좔적할 수 μžˆλ„λ‘ μ§€μ›ν•©λ‹ˆλ‹€. μ‚¬μš©μž 연ꡬ κ²°κ³Ό, 탐색 κΈ°λŠ₯을 μ΄μš©ν•œ μ°Έκ°€μžλ“€μ΄ 증λͺ…에 λŒ€ν•œ 이해도가 높아지고 더 μ •ν™•ν•˜κ³  μƒμ„Έν•œ 닡변을 μ œκ³΅ν•˜λŠ” λ“± 긍정적인 효과λ₯Ό λ³΄μ˜€μŠ΅λ‹ˆλ‹€.

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

β€’
μˆ˜ν•™μ  λ‚΄μš©μ„ LLM의 ν…μŠ€νŠΈ μ„€λͺ…을 λ„˜μ–΄, μ‹€ν–‰ κ°€λŠ₯ν•œ ν˜•μ‹μœΌλ‘œ ν‘œν˜„ν•¨μœΌλ‘œμ¨ 심측적인 ν•™μŠ΅ 및 μƒν˜Έμž‘μš©μ„ κ°€λŠ₯ν•˜κ²Œ ν•©λ‹ˆλ‹€.
β€’
λ³΅μž‘ν•œ μˆ˜ν•™μ  증λͺ…에 λŒ€ν•œ 접근성을 높이고, μ‚¬μš©μžκ°€ λŠ₯λ™μ μœΌλ‘œ ν•™μŠ΅μ— μ°Έμ—¬ν•˜λ„λ‘ μœ λ„ν•˜λŠ” μƒˆλ‘œμš΄ λ°©μ•ˆμ„ μ œμ‹œν•©λ‹ˆλ‹€.
β€’
μ œμ•ˆλœ 방법둠은 Leanκ³Ό 같은 νŠΉμ • ν˜•μ‹ 언어에 μ˜μ‘΄ν•˜λ©°, λͺ¨λ“  μˆ˜ν•™μ  정리와 증λͺ…에 λŒ€ν•œ μžλ™ λ³€ν™˜ 및 탐색 κΈ°λŠ₯ κ΅¬ν˜„μ— λŒ€ν•œ μΌλ°˜ν™” κ°€λŠ₯μ„± 탐ꡬ가 ν•„μš”ν•©λ‹ˆλ‹€.
πŸ‘
Made with Slashpage