์ ์: Wenhu Chen, Ming Yin, Max Ku, Pan Lu, Yixin Wan, Xueguang Ma, Jianyu Xu, Xinyi Wang, Tony Xia | ๋ ์ง: 2023 | DOI: N/A 📄 PDF
Essence
TheoremQA์ ๊ฐ์ ๋ฐ ์ ์ฉ๋ ํ๋กฌํํ
์ ๋ต
๋ํ ์์ค์ ์ํ, ๋ฌผ๋ฆฌ, ๊ธ์ต, ์ ์ฐ ๋ถ์ผ์์ 350๊ฐ ์ด์์ ์ ๋ฆฌ(theorem)๋ฅผ ํฌํจํ๋ 800๊ฐ์ ๊ณ ํ์ง ์ง๋ฌธ-๋ต๋ณ ์์ผ๋ก ๊ตฌ์ฑ๋ ์ ๋ฆฌ ์ค์ฌ ์ง๋ฌธ ๋ต๋ณ ๋ฐ์ดํฐ์
์ ์ ์ํ๋ค. ์ด๋ LLM์ ๋๋ฉ์ธ ์ง์ ์ ์ฉ ๋ฅ๋ ฅ์ ํ๊ฐํ๋ ์ฒซ ๋ฒ์งธ ๋ฒค์น๋งํฌ์ด๋ค.
Evaluation
์ดํ: TheoremQA๋ LLM์ ๋๋ฉ์ธ ํนํ ์ง์ ํ์ฉ ๋ฅ๋ ฅ์ ์ฒด๊ณ์ ์ผ๋ก ํ๊ฐํ๋ ์ฒซ ๋ฒ์งธ ๋ฒค์น๋งํฌ๋ก์ ์๋ฏธ ์๋ ๊ธฐ์ฌ๋ฅผ ํ๋ฉฐ, ๊ด๋ฒ์ํ ๋ชจ๋ธ ํ๊ฐ๋ฅผ ํตํด ํ์ฌ์ ์ฑ๋ฅ ๊ฒฉ์ฐจ๋ฅผ ๋ช
ํํ ๋๋ฌ๋ธ๋ค. ๋ค๋ง ์คํ์์ค ๋ชจ๋ธ์ ๊ทนํ ๋ฎ์ ์ฑ๋ฅ์ ํ๊ฐ์ ๋ณ๋ณ๋ ฅ์ ์ ํํ๊ณ , ์ ๋ฆฌ ํตํฉ ๋ฐฉ์์ ๊ฐ์ ์ฌ์ง๊ฐ ํฌ๋ค๋ ์ ์ด ์์ฝ๋ค.
๊ฐ์ด ๋ณด๋ฉด ์ข์ ๋
ผ๋ฌธ
๊ธฐ๋ฐ ์ฐ๊ตฌ
379๋ LLM์ ํ์ฉํ ์๋ ์ ๋ฆฌ ์ฆ๋ช
(generative theorem proving)์ ๊ธฐ์ด๋ฅผ ์ ๊ณตํ๋ฉฐ, 808์ ์ ๋ฆฌ ์ค์ฌ QA ๋ฒค์น๋งํฌ ์ค์ ์ ๊ธฐ๋ฐ์ด ๋ฉ๋๋ค.
๊ธฐ๋ฐ ์ฐ๊ตฌ
032๋ ๊ณผํ์ง์ ์ถ๋ก ๋ฐ ํํ์์ ์ง์๊ทธ๋ํ ์ฐ๊ตฌ๋ฅผ ์ฒด๊ณํํ์ฌ, ๋
ผ๋ฆฌ์ ์ ๋ฆฌ ์ถ๋ก ํ๊ฐ์ธ 808์ ์ด๋ก ์ ํ ๋๋ฅผ ๋ค๋ฃน๋๋ค.
๊ธฐ๋ฐ ์ฐ๊ตฌ
์ ๋ฆฌ(์ํ ๋ช
์ ) ๊ธฐ๋ฐ ์ง์์๋ต ๋ฐ์ดํฐ์
์ ํตํด TheoremExplainAgent์ ๋ฉํฐ๋ชจ๋ฌ ์๋ ์ค๋ช
์์ฑ ๋ฐฉ์์ ํ๊ฐ ๋ฐ์ดํฐ๋ก ํ์ฉํ ์ ์๋ค.
๋ค๋ฅธ ์ ๊ทผ
TheoremQA ๋
ผ๋ฌธ์ ์ ๋ฆฌ ๊ตฌ๋ ๋ฌธ์ ํด๊ฒฐ ๋ฐ์ดํฐ๋ฅผ ๋ค๋ฃจ์ด ์๋ฆฌ์ ๋
ผ์ฆ/์ฆ๋ช
ํ์คํฌ์ ๋๋ค๋ฅธ ํ๊ฐ ๋์์ ์ ์ํฉ๋๋ค.
๋ค๋ฅธ ์ ๊ทผ
TheoremQA๋ ์ํ์ ์ ๋ฆฌ์ ์์ฐ์ด ์ง์๋ก ๊ตฌ์ฑ๋ ๋ฐ์ดํฐ์
์ ๋ค๋ฃจ๋ฏ๋ก, FIMO์ ๋ฌ๋ฆฌ ์ง์์๋ต ํํ์ ์ฆ๋ช
๋ฌธ์ ํ๊ฐ์ ๋๋น๋๋ค.
๋ค๋ฅธ ์ ๊ทผ
TheoremQA ๋
ผ๋ฌธ์ ์ฐ์์ ์ฌ๊ณ ๋ฅผ ์๊ตฌํ๋ ์ํ ๋ฌธ์ QA์ ์ง์คํ์ฌ, T-SciQ์ ๋ฉํฐ๋ชจ๋ฌ Chain-of-Thought ๊ต์ก ๋ฐ์ดํฐ ํผํฉ ์ ๊ทผ๊ณผ ๋ฌธ์ ์ ํ์ ์ฐจ์ด๊ฐ ์๋ค.
๋ค๋ฅธ ์ ๊ทผ
TheoremQA ๋
ผ๋ฌธ์ ์ํ์ ์ง๋ฌธ-์ฆ๋ช
์ฐ์์ ์ด์ ์ ๋ง์ถฐ, ์ฆ๋ช
๋๊ธฐ๋ ์ฌ๊ณ ๊ณผ์ ์ด ์๋ ์ต์ข
์ ๋ต๊ณผ ๊ทธ ํด์ค๋ง์ ๋ค๋ฃธ์ผ๋ก์จ ์๋ฐ๋ ํ๊ฐ ๊ธฐ์ค์ ๋ณด์ฌ์ค๋ค.
๋ค๋ฅธ ์ ๊ทผ
TheoremQA ๋
ผ๋ฌธ์ ์ ํ ์ํ ์ฆ๋ช
, ์ ๋ฆฌ ๊ธฐ๋ฐ ๋ฌธ์ ํด๊ฒฐ์ ๋ค๋ฃจ๋ฉฐ, Pelican๊ณผ ๊ฐ์ด ์๋ ์ฆ๋ช
์์ LLM์ ์ ํ์ฑ ๊ฒ์ฆ์ ๊ดํ ์ค์ฆ์ ์ ์ํ๋ค.
๋ค๋ฅธ ์ ๊ทผ
์ํ ๋ฐ ๋ฌผ๋ฆฌ ์ ๋ฆฌ ๊ธฐ๋ฐ์ QA ๋ฐ์ดํฐ์
์ ํตํด LLM์ ๋ฌผ๋ฆฌ ์ถ๋ก ๋ฅ๋ ฅ์ ๋ค๋ฅธ ๋ฐ์ดํฐ์
์ผ๋ก ํ๊ฐํ ์ ์๊ธฐ ๋๋ฌธ์
๋๋ค.
ํ์ ์ฐ๊ตฌ
TheoremQA(808)๋ ๊ณผํ ๋
ผ๋ฌธ ์ฐ๊ธฐ, AI ๋ณด์กฐ ์์คํ
์ peer-review domain์์ LLM/AI์ ์ํฅ์ ๋ณด๋ค ๊ตฌ์ฒด์ ์ด๊ณ ํ๊ฐ์ค์ฌ์ ์ผ๋ก ํ์ฅํฉ๋๋ค.
ํ์ ์ฐ๊ตฌ
808์ด ์ ์ํ๋ ๋ฒค์น๋งํฌ๋ 030์ ๋ฅ๋ฌ๋ ๊ธฐ๋ฐ ์ ๋ฆฌ ์ฆ๋ช
๋ฐฉ๋ฒ ๋
ผ์์ ์ค์ฆ์ ํ๊ฐ ๋๊ตฌ๊ฐ ๋ ์ ์์ต๋๋ค.
ํ์ ์ฐ๊ตฌ
Mustard ๋
ผ๋ฌธ์ ๊ธฐ๊ณ ์์ฑ ์ํ ์ ๋ฆฌยท์ฆ๋ช
๋ฐ์ดํฐ ํ์ฅ ๋ฐ ๋ฒค์น๋งํฌ ๊ฐ๋ฐ๋ก TheoremQA ๋ฐ์ดํฐ์
์ ํ์ฉ์ฑ์ ํ์ฅํฉ๋๋ค.
ํ์ ์ฐ๊ตฌ
DeepSeek-Prover์ ์ ๋ฆฌ ์ฆ๋ช
์ ๊ทผ๋ฒ์ ํ์ฅํ๊ฑฐ๋ ๋ณด์ํ๋ ์ฐ๊ตฌ์ด๋ค.
ํ์ ์ฐ๊ตฌ
504๋ ๊ณผํ ๋ถ์ผ ๋ชจ๋ธ์ด ์์ ํ์ ๋ฐ ๋ฐ๊ฒฌ ๊ณผ์ ๋ฅผ ์ผ๋ง๋ ์ ์ํํ๋์ง๋ฅผ ํ๊ฐํ๋ฉฐ, ์ํ์ reasoning ๋ฒค์น๋งํฌ๋ก 808์ ์ญํ ์ ํ์ฅํฉ๋๋ค.
ํ์ ์ฐ๊ตฌ
AI-๊ธฐ๋ฐ ์ํ ๊ณต์ํ ์ฐ๊ตฌ์์ TheoremQA ๋ฐ์ดํฐ์
ํ์ฉ ๋ฐ ํ์ฅ ์ฌ๋ก๋ฅผ ํ์ธํ ์ ์์ต๋๋ค.
์์ฉ ์ฌ๋ก
TheoremQA ๋
ผ๋ฌธ์ ์ ๋ฆฌ ๊ธฐ๋ฐ ์ง์์๋ต ๋ฐ์ดํฐ์
์ ํตํด ์๋์ ๋ฆฌ์ฆ๋ช
LLM์ ์ค์ ๋ฌธ์ ํ์ด ๋ฅ๋ ฅ์ ํ๊ฐํฉ๋๋ค.
์์ฉ ์ฌ๋ก
TheoremQA ๋
ผ๋ฌธ์ MUSTARD ๋ฑ ์๋ ์์ฐ๋ ๋ฐ์ดํฐ๋ก ๋ฏธ์ธ์กฐ์ ๋ LLM์ ํ์ ์ํ ๋ฌธ์ ํด๊ฒฐ ๋ฅ๋ ฅ์ ์ค์ ํ๊ฐํฉ๋๋ค.
์์ฉ ์ฌ๋ก
์ํยท๋ฌผ๋ฆฌยท์ปดํจํฐ ๋ถ์ผ ์ค์ ์ ๋ฆฌ-๋ฌธ์ -๋ต๋ณ ์๋ฃ๊ฐ ์ฌ๊ท์ ์๋ ์ฆ๋ช
์คํ์ ๋ฒค์น๋งํฌ๋ก ์ฐ์ผ ์ ์์ต๋๋ค.
์์ฉ ์ฌ๋ก
030์์ ์ ๋ฆฌ๋ ์ฆ๋ช
AI ํ๊ฐ ๋ฐฉ๋ฒ๋ค์ 808์ ์ ๋ฆฌ ์ค์ฌ ์ง์์๋ต ๋ฒค์น๋งํฌ์ ์ค์ ์ ์ผ๋ก ์ ์ฉํ์ฌ ์ฌ์ธต ๋น๊ต๊ฐ ๊ฐ๋ฅํฉ๋๋ค.
์์ฉ ์ฌ๋ก
TheoremQA(808)์ LLM ๊ธฐ๋ฐ ์๋ ๋
ผ๋ฌธ ์์ฑ ๋ฐ ๊ฒ์ฆ์ด ๊ฐ๋ฅํ ์ค์ ์์๋ก, 444์ AI ๋
ผ๋ฌธ์์ฑ ์ค๋ฆฌ ๋
ผ์๋ฅผ ํ์ค์ ๊ทผ๊ฑฐํ์ฌ ํ์ฅํ๋ค.
์์ฉ ์ฌ๋ก
์ํ ๊ธฐ๋ฐ ์ง์์๋ต(Automated Theorem-driven QA)์ ์ญ๋์ด ์ค์ ์ฆ๋ช
์๋ํ ํ๋ ์์ํฌ์์ ์ด๋ป๊ฒ ํ๊ฐ๋๋์ง ํ์ธํ ์ ์์ต๋๋ค.