#数学奥林匹克
相关项目
alphageometry
AlphaGeometry是一个创新的几何定理证明系统,能够解决奥林匹克级别的几何问题,无需人类示范。它结合了演绎-归纳推理和大型语言模型,自动构建辅助线并生成严格证明。在IMO-AG-30和JGEX-AG-231测试集上,AlphaGeometry分别解决了25和228个问题,大幅超越传统DDAR方法。项目开源了核心代码,包括DDAR求解器和语言模型推理模块,为几何定理自动证明开辟新路径。
MathBlackBox
MathBlackBox项目采用蒙特卡罗树搜索(MCTS)方法提升大语言模型的数学问题解决能力。项目使用VLLM或其他OpenAI兼容方法构建服务器,客户端则基于Hugging Face工具包和OpenAI进行推理。支持GSM8K、OlympiadBench和MATH等多个数学数据集。研究显示,该方法可使LLaMa-3 8B模型在数学奥林匹克解题方面达到接近GPT-4的水平。目前项目处于早期阶段,仍需进一步测试和优化。