AI初创企业webAI于近期正式推出轻量形式逻辑大模型系列TwIL-LM，包含17亿（1.7B）、30亿（3B）两个参数版本，主打自动形式化、逻辑蕴涵检查能力，原生支持Lean交互式定理证明器，可完全脱离云端在普通消费级本地硬件上运行，为科研、工业领域的研发人员提供了低门槛的数理逻辑推理工具。
数理逻辑推理能力一直是大模型向硬核科研、工业场景落地的核心瓶颈，而此前能支撑自动形式化、定理验证等任务的大模型普遍参数超过百亿，仅能在云端或专业超算设备运行，不仅调用成本高，还存在核心研发数据泄露的风险。
不论是数学界的定理证明、芯片行业的形式化验证还是软件行业的代码合规审计，都需要把自然语言描述的规则、命题转换为机器可识别的形式化代码，这个过程此前高度依赖人工，效率极低。引入AI工具后，行业又普遍面临大模型部署成本高、数据安全难以保障的痛点，中小企业和独立开发者几乎没有低成本的可用工具。
登录后解锁全文，体验收藏、点赞、评论等完整功能
立即登录
滇公网安备 53252802528133号