Sign In

FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models

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

์ €์ž

Zeynel A. Ulu\c{s}an, Burak S. Akbudak, Can S. Erer, Gozde Gul \c{S}ahin

๐Ÿ’ก ๊ฐœ์š”

์ด ๋…ผ๋ฌธ์€ ํ˜•์‹ ์ •๋ฆฌ ์ฆ๋ช…์—์„œ ํ•™์Šต๋œ ๋ณด์ƒ ๋ชจ๋ธ์„ ํ‰๊ฐ€ํ•˜๊ธฐ ์œ„ํ•œ ์ตœ์ดˆ์˜ ๋ฒค์น˜๋งˆํฌ์ธ FormalRewardBench๋ฅผ ์ œ์•ˆํ•ฉ๋‹ˆ๋‹ค. ๊ธฐ์กด์˜ ์ด์ง„(binary) ๋ณด์ƒ ๋ฐฉ์‹์€ ์–ด๋ ค์šด ๋ฌธ์ œ์—์„œ ๋ถ€๋ถ„์ ์ธ ์ง„์ „์„ ๋ณด์ƒํ•˜์ง€ ๋ชปํ•˜๋Š” ํฌ์†Œํ•œ ํฌ๋ ˆ๋”ง ํ• ๋‹น ๋ฌธ์ œ๋ฅผ ๊ฒช์œผ๋ฉฐ, ์ด๋ฅผ ํ•ด๊ฒฐํ•˜๊ธฐ ์œ„ํ•ด ์ฆ๋ช… ํ’ˆ์งˆ์„ ํ‰๊ฐ€ํ•  ์ˆ˜ ์žˆ๋Š” ํ•™์Šต๋œ ๋ณด์ƒ ๋ชจ๋ธ์ด ํ•„์š”ํ•ฉ๋‹ˆ๋‹ค. FormalRewardBench๋Š” 250๊ฐœ์˜ ์„ ํ˜ธ ์Œ์œผ๋กœ ๊ตฌ์„ฑ๋˜๋ฉฐ, ์ตœ์‹  LLM์ด ๊ฐ€์žฅ ๋†’์€ ์„ฑ๋Šฅ์„ ๋ณด์˜€์œผ๋‚˜ ํ˜•์‹ ์ •๋ฆฌ ์ฆ๋ช… ๋Šฅ๋ ฅ์ด ๋ณด์ƒ ๋ชจ๋ธ ํ‰๊ฐ€ ๋Šฅ๋ ฅ์œผ๋กœ ์ „์ด๋˜์ง€ ์•Š๋Š”๋‹ค๋Š” ์ ์„ ๋ฐœ๊ฒฌํ–ˆ์Šต๋‹ˆ๋‹ค.

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

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