Sign In

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

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

์ €์ž

Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

๐Ÿ’ก ๊ฐœ์š”

๋ณธ ๋…ผ๋ฌธ์€ ์ž๋™ํ™”๋œ ๋Œ€์ˆ˜์  ์ถ”๋ก ์˜ ๊ทผ๋ณธ์ ์ธ ๋ฌธ์ œ์ธ ๋‹คํ•ญ์‹ ๋ถ€๋“ฑ์‹ ์ฆ๋ช…์„ ์œ„ํ•œ ์‹ ๊ฒฝ-๊ธฐํ˜ธ ํ†ตํ•ฉ ํ”„๋ ˆ์ž„์›Œํฌ NSPI๋ฅผ ์ œ์•ˆํ•œ๋‹ค. LLM์ด ๊ทผ์‚ฌ์ ์ธ ์ œ๊ณฑํ•ฉ(SOS) ๋ถ„ํ•ด๋ฅผ ์ถ”์ธก์œผ๋กœ ์ œ์‹œํ•˜๋ฉด, ์ด๋ฅผ ๊ธฐํ˜ธ ๊ณ„์‚ฐ์œผ๋กœ ์ •์ œํ•˜์—ฌ ์ •ํ™•ํ•œ SOS ํ‘œํ˜„์„ ์–ป๊ณ , ์ด๋ฅผ ํ†ตํ•ด ๋ถ€๋“ฑ์‹์„ ์ฆ๋ช…ํ•œ๋‹ค. ์ตœ์ข…์ ์œผ๋กœ Lean ์ฆ๋ช… ๋ณด์กฐ๊ธฐ๋ฅผ ์‚ฌ์šฉํ•˜์—ฌ ์ฆ๋ช…์„ ๊ฒ€์ฆํ•จ์œผ๋กœ์จ, ๋ฐœ๊ฒฌ๋ถ€ํ„ฐ ๊ธฐ๊ณ„ ๊ฒ€์ฆ๊นŒ์ง€์˜ ์ „์ฒด ํŒŒ์ดํ”„๋ผ์ธ์„ ๊ตฌ์ถ•ํ•œ๋‹ค.

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

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