Sign In

Combining Mechanical and Agentic Specification Inference for Move

์ž‘์„ฑ์ž
  • Haebom
์นดํ…Œ๊ณ ๋ฆฌ
Empty

์ €์ž

Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap

๐Ÿ’ก ๊ฐœ์š”

๋ณธ ๋…ผ๋ฌธ์€ Move ์ฝ”๋“œ์˜ ๋ช…์„ธ๋ฅผ ์ž๋™์œผ๋กœ ์ถ”๋ก ํ•˜๋Š” ๋„๊ตฌ๋ฅผ ์ œ์•ˆํ•ฉ๋‹ˆ๋‹ค. ์ œ์•ˆ๋œ ๋„๊ตฌ๋Š” ๊ธฐ๊ณ„์ ์ธ ์•ฝํ•œ ์ „์ œ ์กฐ๊ฑด(WP) ๋ถ„์„๊ณผ Claude Code์™€ ๊ฐ™์€ ์—์ด์ „ํŠธ ๊ธฐ๋ฐ˜ ์ฝ”๋”ฉ CLI๋ฅผ ๊ฒฐํ•ฉํ•˜์—ฌ, Move ํ”„๋กœ๊ทธ๋ž˜๋ฐ ์–ธ์–ด์—์„œ ๋ณต์žกํ•œ ๊ณ ์ˆ˜์ค€ ์†์„ฑ์„ ๊ฒ€์ฆํ•˜๊ธฐ ์œ„ํ•œ ๋ช…์„ธ๋ฅผ ํšจ์œจ์ ์œผ๋กœ ์ƒ์„ฑํ•ฉ๋‹ˆ๋‹ค. ์ด๋ฅผ ํ†ตํ•ด ๊ฐœ๋ฐœ์ž๊ฐ€ ์ˆ˜์ž‘์—…์œผ๋กœ ์ž‘์„ฑํ•ด์•ผ ํ•˜๋Š” ๋ช…์„ธ ์ž‘์„ฑ์˜ ๋ฒˆ๊ฑฐ๋กœ์›€์„ ์ค„์ด๊ณ , AI๊ฐ€ WP ๋ถ„์„์ด ์•ฝํ•œ ๋ถ€๋ถ„(๋ฃจํ”„ ๋ถˆ๋ณ€๋Ÿ‰, ๋ชจ๋…ธํ† ๋‹ˆ์‹œํ‹ฐ ๋“ฑ)์„ ๋ณด์™„ํ•˜๋„๋ก ํ•ฉ๋‹ˆ๋‹ค.

๐Ÿ”‘ ์‹œ์‚ฌ์  ๋ฐ ํ•œ๊ณ„

โ€ข
Move ์–ธ์–ด์—์„œ ํ”„๋กœ๊ทธ๋ž˜๋ฐ ๋ช…์„ธ ์ถ”๋ก ์˜ ์ž๋™ํ™”๋ฅผ ํ†ตํ•ด ๊ฐœ๋ฐœ ์ƒ์‚ฐ์„ฑ์„ ํฌ๊ฒŒ ํ–ฅ์ƒ์‹œํ‚ฌ ์ˆ˜ ์žˆ์Šต๋‹ˆ๋‹ค.
โ€ข
๊ธฐ๊ณ„์ ์ธ ๋ถ„์„๊ณผ AI์˜ ๊ฐ•์ ์„ ๊ฒฐํ•ฉํ•˜์—ฌ, ๊ธฐ์กด ๋ฐฉ์‹์œผ๋กœ๋Š” ์–ด๋ ต๋˜ ๋ณต์žกํ•œ ๋ช…์„ธ(๋ฃจํ”„ ๋ถˆ๋ณ€๋Ÿ‰, ๊ณ ์ˆ˜์ค€ ๋ถˆ๋ณ€๋Ÿ‰ ๋“ฑ) ์ถ”๋ก ์˜ ๊ฐ€๋Šฅ์„ฑ์„ ๋ณด์—ฌ์ค๋‹ˆ๋‹ค.
โ€ข
AI ๋ชจ๋ธ์ด ์ƒ์„ฑํ•œ ๋ช…์„ธ์˜ ์œ ํšจ์„ฑ์„ Move Prover๋ฅผ ํ†ตํ•ด ๊ฒ€์ฆํ•˜๊ณ , ์—์ด์ „ํŠธ๊ฐ€ ์ด๋ฅผ ๊ฐœ์„ ํ•˜๋Š” ๋ฐ˜๋ณต์  ํ”„๋กœ์„ธ์Šค๋Š” ๊ฒฌ๊ณ ํ•œ ๋ช…์„ธ ์ƒ์„ฑ์„ ๊ฐ€๋Šฅํ•˜๊ฒŒ ํ•ฉ๋‹ˆ๋‹ค.
โ€ข
์•„์ง ์ดˆ๊ธฐ ์—ฐ๊ตฌ ๋‹จ๊ณ„์ด๋ฏ€๋กœ, ๋‹ค์–‘ํ•œ Move ์ฝ”๋“œ์˜ ๋ณต์žก์„ฑ ๋ฐ ์ƒˆ๋กœ์šด ํŒจํ„ด์— ๋Œ€ํ•œ ์ ์šฉ์„ฑ๊ณผ ํ™•์žฅ์„ฑ ๊ฒ€์ฆ์ด ํ•„์š”ํ•ฉ๋‹ˆ๋‹ค.
๐Ÿ‘
Made with Slashpage