OpenAI News·· 2022-02-02AI 评分38
OpenAI 构建 Lean 神经定理证明器解决部分数学奥赛题
Solving (some) formal math olympiad problems
AI 导读
OpenAI 构建了用于 Lean 的神经定理证明器，成功解决了包括 AMC12、AIME 及两道改编 IMO 题目在内的高中奥赛难题。该模型通过机器学习掌握了处理高难度形式化数学问题的能力。
原文
We built a neural theorem prover for Lean that learned to solve a variety of challenging high-school olympiad problems, including problems from the AMC12 and AIME competitions, as well as two problems adapted from the IMO.
来源：OpenAI News · openai.com