๋กœ๊ทธ์ธ

MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries

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

์ €์ž

Zixuan Xie, Xinyu Liu, Shangtong Zhang

๐Ÿ’ก ๊ฐœ์š”

LLM(๋Œ€๊ทœ๋ชจ ์–ธ์–ด ๋ชจ๋ธ)์€ ์ตœ๊ทผ ๊ณต์‹ ์ˆ˜ํ•™ ๋ผ์ด๋ธŒ๋Ÿฌ๋ฆฌ์ธ Mathlib ์ƒํƒœ๊ณ„์—์„œ ๋†€๋ผ์šด ์„ฑ๊ณต์„ ๊ฑฐ๋‘์—ˆ์ง€๋งŒ, Mathlib ์ž์ฒด์— ์ง์ ‘์ ์œผ๋กœ ๊ธฐ์—ฌํ•˜๋Š” ๋ฐฉ์‹์œผ๋กœ๋Š” ํ™œ์šฉ๋˜์ง€ ๋ชปํ–ˆ์Šต๋‹ˆ๋‹ค. ๋ณธ ๋…ผ๋ฌธ์€ Mathlib PR(Pull Request) ๋ฆฌ๋ทฐ์— LLM์ด ๊ธฐ์—ฌํ•  ์ˆ˜ ์žˆ๋Š”์ง€ ํƒ๊ตฌํ•˜๊ธฐ ์œ„ํ•ด ์‹ค์ œ Mathlib4 PR ๊ธฐ๋ก์„ ๊ธฐ๋ฐ˜์œผ๋กœ ํ•œ ๋ฒค์น˜๋งˆํฌ์ธ MathlibPR์„ ์†Œ๊ฐœํ•ฉ๋‹ˆ๋‹ค. ํ‰๊ฐ€ ๊ฒฐ๊ณผ, LLM ๋ชจ๋ธ ๋ฐ ์—์ด์ „ํŠธ ๋ชจ๋‘ ๋ณ‘ํ•ฉ ๊ฐ€๋Šฅํ•œ PR๊ณผ ๋‹จ์ˆœํžˆ ๋นŒ๋“œ๋ฅผ ํ†ต๊ณผํ–ˆ์œผ๋‚˜ ๋ณ‘ํ•ฉ๋˜์ง€ ์•Š๊ฑฐ๋‚˜ ์ˆ˜์ •๋œ PR์„ ๊ตฌ๋ถ„ํ•˜๋Š” ๋ฐ ์–ด๋ ค์›€์„ ๊ฒช์—ˆ์Šต๋‹ˆ๋‹ค.

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

โ€ข
MathlibPR ๋ฒค์น˜๋งˆํฌ๋Š” LLM์„ ํ™œ์šฉํ•˜์—ฌ ๊ณต์‹ ์ˆ˜ํ•™ ๋ผ์ด๋ธŒ๋Ÿฌ๋ฆฌ์˜ PR ๋ฆฌ๋ทฐ ๊ณผ์ •์„ ์ž๋™ํ™”ํ•˜๊ฑฐ๋‚˜ ์ง€์›ํ•˜๋Š” ์—ฐ๊ตฌ์˜ ์ค‘์š”ํ•œ ๋ฐœํŒ์„ ๋งˆ๋ จํ•ฉ๋‹ˆ๋‹ค.
โ€ข
LLM์ด ๋‹จ์ˆœํžˆ ์ฝ”๋“œ๋ฅผ ์ƒ์„ฑํ•˜๋Š” ๊ฒƒ์„ ๋„˜์–ด, ๋ณต์žกํ•œ ๋ผ์ด๋ธŒ๋Ÿฌ๋ฆฌ์˜ ๊ทœ์•ฝ์„ ์ค€์ˆ˜ํ•˜๊ณ  ์‹ค์ œ ๋ณ‘ํ•ฉ์— ์ ํ•ฉํ•œ ๊ธฐ์—ฌ๋ฅผ ์ƒ์„ฑํ•˜๋„๋ก ํ›ˆ๋ จ์‹œํ‚ค๋Š” ๋ฐ ํ•„์š”ํ•œ ์‹ ํ˜ธ์™€ ํ‰๊ฐ€ ํ”„๋กœํ† ์ฝœ์„ ์ œ๊ณตํ•ฉ๋‹ˆ๋‹ค.
โ€ข
ํ˜„์žฌ LLM์€ ๋ณ‘ํ•ฉ ๊ฐ€๋Šฅํ•œ PR๊ณผ ๋‹จ์ˆœํžˆ ๋นŒ๋“œ๋ฅผ ํ†ต๊ณผํ•œ PR์„ ๊ตฌ๋ถ„ํ•˜๋Š” ๋ฐ ํ•œ๊ณ„๊ฐ€ ์žˆ์œผ๋ฉฐ, ์ด๋Š” ํ–ฅํ›„ LLM์˜ ์ถ”๋ก  ๋Šฅ๋ ฅ ๋ฐ ๊ทœ์•ฝ ์ค€์ˆ˜ ๋Šฅ๋ ฅ์„ ํ–ฅ์ƒ์‹œํ‚ค๋Š” ์—ฐ๊ตฌ๊ฐ€ ํ•„์š”ํ•จ์„ ์‹œ์‚ฌํ•ฉ๋‹ˆ๋‹ค.
๐Ÿ‘
Slashpage๋กœ ์ œ์ž‘๋จ