Sign In

CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean

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

์ €์ž

Wentao Long, Yunfei Zhang, Chenyi Li, Li Zhou, Chumin Sun, Zaiwen Wen

๐Ÿ’ก ๊ฐœ์š”

๋ณธ ๋…ผ๋ฌธ์€ ๊ณ„์‚ฐ ๋ฐ ์‘์šฉ ์ˆ˜ํ•™ ๋ถ„์•ผ์˜ ์–ธ์–ด ๋ชจ๋ธ ๊ธฐ๋ฐ˜ ์ž๋™ ์ •๋ฆฌ ์ฆ๋ช… ์„ฑ๋Šฅ์„ ํ‰๊ฐ€ํ•˜๊ธฐ ์œ„ํ•œ 1,000๊ฐœ์˜ Lean ์ฆ๋ช… ๋ชฉํ‘œ๋กœ ๊ตฌ์„ฑ๋œ CAM-Bench๋ฅผ ์ œ์•ˆํ•œ๋‹ค. ๊ธฐ์กด ๋ฒค์น˜๋งˆํฌ๊ฐ€ ์˜ฌ๋ฆผํ”ผ์•„๋“œ ์Šคํƒ€์ผ ๋ฐ ๋Œ€์ˆ˜ํ•™ ๋ฌธ์ œ์— ์ง‘์ค‘๋œ ๊ฒƒ๊ณผ ๋‹ฌ๋ฆฌ, CAM-Bench๋Š” ์ตœ์ ํ™”, ์ˆ˜์น˜ ์„ ํ˜•๋Œ€์ˆ˜, ์ˆ˜์น˜ ํ•ด์„ ๋“ฑ ์‘์šฉ ์ˆ˜ํ•™ ๋ถ„์•ผ๋ฅผ ํฌ๊ด„ํ•œ๋‹ค. ํ…์ŠคํŠธ๋ถ ์—ฐ์Šต ๋ฌธ์ œ๋ฅผ ๊ธฐ๋ฐ˜์œผ๋กœ ์ง€์—ญ์  ์ •์˜์™€ ๊ฐœ๋…์„ ๋ณต์›ํ•˜๋Š” ํŒŒ์ดํ”„๋ผ์ธ์„ ํ†ตํ•ด ๋ฌธ์ œ์˜ ๊ณต์‹ํ™”์™€ Lean์œผ๋กœ์˜ ๋ณ€ํ™˜์„ ์ˆ˜ํ–‰ํ–ˆ์œผ๋ฉฐ, ๋ชจ๋ธ๋“ค์˜ ์ฆ๋ช… ์‹คํŒจ ํŒจํ„ด์„ ๋ถ„์„ํ•˜์—ฌ ํ–ฅํ›„ ์—ฐ๊ตฌ ๋ฐฉํ–ฅ์„ ์ œ์‹œํ•œ๋‹ค.

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

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