Math-Inference：让大语言模型的数学回答可被形式化验证

Math-Inference是基于Phoenix LiveView的开源项目，结合LLM路由能力与SymPy、Julia、Octave、Lean4等数学证明引擎，通过生成-验证双层架构实现AI数学答案的形式化验证，为数学AI应用提供可靠性保障，解决LLM数学输出的幻觉问题。

LLM在数学推理中存在"幻觉"问题，生成表面正确但实际错误的内容。传统方案（增数据、改架构、微调）无法保证绝对正确性，而数学对正确性零容忍，业界需验证LLM数学输出的技术方案。

Math-Inference采用Phoenix LiveView框架（Elixir开发）构建实时交互应用，核心架构含三层：

1. LLM路由层：智能分配问题，简单题直接返回结果，复杂题触发验证；
2. 多引擎验证层：SymPy（符号计算）、Julia（数值计算）、Octave（工程计算）、Lean4（形式化证明）互补；
3. 协调机制：分层验证策略，优化资源利用。

亮点包括：

1. 实时交互：Phoenix LiveView通过WebSocket推送验证过程，增强用户信任；
2. 反馈循环：验证错误反馈给LLM重新生成，提升答案质量；
3. 可扩展架构：模块化设计，易集成新引擎（如Coq、Isabelle）。

应用场景：

1. 教育辅助：智能助教，经验证答案用于自动批改；
2. 科研验证：快速检查科研计算中间步骤；
3. 定理证明：结合Lean4提供证明建议与验证服务。

局限：验证成本高（复杂证明耗时）、LLM生成Lean代码语法错误多。未来方向：优化验证策略、改进LLM形式化代码生成、探索轻量级验证方法。

Math-Inference代表AI数学应用从生成转向生成与验证并重，为高正确性AI场景提供借鉴，期待更多可靠智能系统出现。