Sign In

RocqSmith: Can Automatic Optimization Forge Better Proof Agents?

Created by
  • Haebom
Category
Empty

μ €μž

Andrei Kozyrev, Nikita Khramov, Denis Lochmelis, Valerio Morelli, Gleb Solovev, Anton Podkopaev

πŸ’‘ κ°œμš”

λ³Έ μ—°κ΅¬λŠ” μžλ™ν™”λœ AI μ—μ΄μ „νŠΈ μ΅œμ ν™” 방법둠이 ν˜•μ‹ 검증 ν™˜κ²½μ˜ μ‹€μ œ μ—μ΄μ „νŠΈμ— 적용될 수 μžˆλŠ”μ§€ νƒκ΅¬ν•˜λ©°, λ³΅μž‘ν•œ 뢄야인 Rocq의 μžλ™ 정리 증λͺ…에 μ΄ˆμ μ„ 맞μΆ₯λ‹ˆλ‹€. λ‹€μ–‘ν•œ μžλ™ μ—μ΄μ „νŠΈ μ΅œμ ν™”κΈ°λ“€μ΄ Rocq 증λͺ… 생성 μ—μ΄μ „νŠΈ μ΅œμ ν™” μž‘μ—…μ—μ„œ μ–΄λ–»κ²Œ μ„±λŠ₯을 λ°œνœ˜ν•˜λŠ”μ§€ ν‰κ°€ν•˜κ³ , ν”„λ‘¬ν”„νŠΈ λ””μžμΈ, λ§₯락 지식, μ œμ–΄ μ „λž΅κ³Ό 같은 μ—μ΄μ „νŠΈ μ‹œμŠ€ν…œμ˜ λ―Έμ„Έ μ‘°μ • 뢀뢄을 μžλ™ν™”ν•  수 μžˆλŠ”μ§€ λΆ„μ„ν•©λ‹ˆλ‹€.

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

β€’
μžλ™ν™”λœ μ΅œμ ν™” 방법둠이 Rocq의 증λͺ… μ—μ΄μ „νŠΈ μ„±λŠ₯을 ν–₯μƒμ‹œν‚¬ 수 μžˆμŒμ„ λ³΄μ—¬μ€λ‹ˆλ‹€.
β€’
κ°„λ‹¨ν•œ few-shot bootstrapping 방식이 κ°€μž₯ 일관성 있게 효과적인 μ΅œμ ν™” λ°©λ²•μœΌλ‘œ ν™•μΈλ˜μ—ˆμŠ΅λ‹ˆλ‹€.
β€’
ν˜„μž¬ μ—°κ΅¬λœ μ΅œμ ν™” λ°©λ²•μœΌλ‘œλŠ” μˆ˜μž‘μ—…μœΌλ‘œ μ •κ΅ν•˜κ²Œ μ„€κ³„λœ μ΅œμ‹  증λͺ… μ—μ΄μ „νŠΈμ˜ μ„±λŠ₯에 λ―ΈμΉ˜μ§€ λͺ»ν•˜λŠ” ν•œκ³„κ°€ μžˆμŠ΅λ‹ˆλ‹€.
πŸ‘
Made with Slashpage