为探索人工智能与数学推理的交叉前沿，12月1日14:30，三亚学院信息与智能工程学院“信智讲座”系列活动在书新4A04会议室顺利举行。本次讲座特邀杨涛教授担任主讲，主题为“大型语言模型在不等式证明中的应用研究”，学院师生代表参与了此次学术交流。
讲座伊始，杨涛教授围绕“如何验证模型推理的严谨性”展开背景介绍：当前，形式化数学系统（如Lean、Coq）虽能精准验证证明过程，但存在门槛高、自动化程度低的问题，面对奥数级不等式时难以规模化处理；而大型语言模型依托自然语言训练，在“非正式推理”领域更贴近人类思考模式，具备低门槛、易处理的优势，因此探索其在不等式证明中的应用具有重要价值。
随后，杨涛教授重点讲解了研究团队开发的“AI数学裁判系统”：该系统不仅能判断最终答案的正确性，还可从“特例验证”、“逻辑漏洞检测”、“数值近似识别”、“代数运算验证”四个维度，自动评估模型推理步骤的合理性，避免模型仅靠“蒙对”结果而被“欺骗”。现场演示中，系统对“a^2+b^2 \geq 2ab”等不等式的推理验证过程，让师生直观感受到技术的实用性。
讲座尾声，师生围绕“模型推理的容错边界”、“数据集的拓展方向”等问题与杨涛教授展开互动，现场氛围热烈。参与师生表示，此次讲座不仅展现了大型语言模型在数学领域的创新应用，也为交叉学科研究提供了新的思路。
一审一校 | 申玮帆
二审二校 | 杨涛
三审三校 | 李成名 尹娜
