Sign In

Neuro-Symbolic Proof Generation for Scaling Systems Software Verification

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

μ €μž

Baoding He, Zenan Li, Wei Sun, Yuan Yao, Taolue Chen, Xiaoxing Ma, Zhendong Su

πŸ’‘ κ°œμš”

λ³Έ 논문은 μ‹œμŠ€ν…œ μ†Œν”„νŠΈμ›¨μ–΄ κ²€μ¦μ—μ„œ λ³΅μž‘ν•˜κ³  μˆ˜λ™μ μΈ 증λͺ… 슀크립트 μž‘μ„±μ„ μžλ™ν™”ν•˜κΈ° μœ„ν•œ μ‹ κ²½-기호 증λͺ… 생성 ν”„λ ˆμž„μ›Œν¬λ₯Ό μ œμ•ˆν•©λ‹ˆλ‹€. μ œμ•ˆλœ ν”„λ ˆμž„μ›Œν¬λŠ” 증λͺ… μƒνƒœμ— λŒ€ν•œ μ΅œμ„  μš°μ„  트리 탐색을 μˆ˜ν–‰ν•˜λ©°, 각 λ‹¨κ³„μ—μ„œ LLM을 ν™œμš©ν•˜μ—¬ λ‹€μŒ 증λͺ… 후보λ₯Ό μƒμ„±ν•©λ‹ˆλ‹€. 신경망 μΈ‘λ©΄μ—μ„œλŠ” 증λͺ… μƒνƒœ-단계 쌍 λ°μ΄ν„°μ…‹μœΌλ‘œ LLM을 νŒŒμΈνŠœλ‹ν•˜κ³ , 기호 μΈ‘λ©΄μ—μ„œλŠ” ITP(Interactive Theorem Proving) 도ꡬλ₯Ό ν†΅ν•©ν•˜μ—¬ 증λͺ… μ‹€νŒ¨ 단계 μˆ˜μ •, μƒνƒœ 필터링 및 μˆœμœ„ 지정, μžλ™ ν•˜μœ„ λͺ©ν‘œ 해결을 μˆ˜ν–‰ν•©λ‹ˆλ‹€.

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

β€’
데이터 효율적인 LLM 적응 및 의미둠적 μ œμ•½ 기반 탐색 곡간 κ°€μ§€μΉ˜κΈ°: 신경망과 기호 μ ‘κ·Ό λ°©μ‹μ˜ μ‹œλ„ˆμ§€λ₯Ό 톡해 LLM을 데이터 효율적으둜 μ μ‘μ‹œν‚€κ³ , 의미둠적 정보λ₯Ό ν™œμš©ν•˜μ—¬ 증λͺ… 탐색 곡간을 효과적으둜 쀄일 수 μžˆμŠ΅λ‹ˆλ‹€.
β€’
κΈ°μ‘΄ LLM 기반 및 Sledgehammer μ ‘κ·Ό λ°©μ‹μ˜ μ„±λŠ₯ μ΄ˆμ›”: seL4 λ²€μΉ˜λ§ˆν¬μ—μ„œ μ œμ•ˆλœ μ‹œμŠ€ν…œμ΄ 이전 LLM 기반 μ ‘κ·Ό 방식과 독립적인 Sledgehammer보닀 훨씬 λ›°μ–΄λ‚œ μ„±λŠ₯을 보이며, 특히 닀단계 증λͺ…μ—μ„œ 더 λ§Žμ€ 수의 정리λ₯Ό 증λͺ…ν•˜λŠ” 것을 μž…μ¦ν–ˆμŠ΅λ‹ˆλ‹€.
β€’
ν™•μž₯ κ°€λŠ₯ν•œ μžλ™ν™”λœ μ†Œν”„νŠΈμ›¨μ–΄ 검증을 μœ„ν•œ μ‹€ν˜„ κ°€λŠ₯ν•œ 경둜 μ œμ‹œ: λ‹€μ–‘ν•œ Isabelle λ²€μΉ˜λ§ˆν¬μ— λŒ€ν•œ κ°•λ ₯ν•œ μΌλ°˜ν™” μ„±λŠ₯을 보여주며, λŒ€κ·œλͺ¨ μ‹œμŠ€ν…œ μ†Œν”„νŠΈμ›¨μ–΄ 검증을 μžλ™ν™”ν•˜κΈ° μœ„ν•œ μœ λ§ν•œ μ ‘κ·Ό 방식을 μ œμ‹œν•©λ‹ˆλ‹€.
β€’
κ³ ν’ˆμ§ˆ 증λͺ… μƒνƒœ 정보 μ œκ³΅μ„ μœ„ν•œ Isabelle REPL의 ν•„μš”μ„±: ν”„λ ˆμž„μ›Œν¬μ˜ 성곡적인 κ΅¬ν˜„μ΄ λ―Έμ„Έν•œ 증λͺ… μƒνƒœμ™€ μžλ™ν™” 도ꡬλ₯Ό λ…ΈμΆœν•˜λŠ” μƒˆλ‘œμš΄ Isabelle REPL에 μ˜μ‘΄ν•˜λ―€λ‘œ, μ΄λŸ¬ν•œ ν™˜κ²½ μ—†μ΄λŠ” 적용이 μ œν•œλ  수 μžˆμŠ΅λ‹ˆλ‹€.
πŸ‘
Made with Slashpage