4B小模型通过符号推理实现可解释的教育问答,物理题拿满分。
CoTu at EXACT 2026: Neuro-Symbolic Reasoning for Transparent Educational QA
- 用40亿参数模型生成可验证的程序代码,代替直接回答
- 物理题获满分,推理深度获专家最高分13.44/15
- 适合关注可解释AI与小模型推理能力的研究者
透明教育问答要求答案不仅正确,还需可解释。在EXACT 2026竞赛中,参赛系统需使用不超过80亿参数的开源语言模型,自托管,并对每个答案提供自然语言解释。任务包括大学规章逻辑推理和多步物理问题求解。我们提出的CoTu系统采用神经符号式“思维程序”流程:40亿参数主干模型生成程序而非直接作答——规章类查询输出Z3编码以证明推论有效性,物理题生成数值型Python代码,二者均经统一自纠错循环与结构化解释输出。通过答案类型路由、基于蒸馏的任务微调及延迟感知服务架构(SGLang + 推测解码),系统在单次查询60秒内完成。该系统在物理任务中两次自动筛选轮次均获满分,并在最终技术评分中以13.44/15位列所有队伍第一;综合自动化评测与专家评判的推理深度得分,总分位列第三。将答案锚定于符号求解器,可在40亿参数规模实现正确且可验证的推导,真正难点在于前提选择而非推导过程本身。
原文摘要 · Abstract (English)
Transparent educational question answering asks for answers that are not only correct but explainable, and doing so with small models rules out the reasoning power of the largest proprietary systems. The EXACT 2026 competition poses this problem concretely: open-weight language models of at most 8B parameters, self-hosted, with a natural-language explanation for every answer. It pairs two tasks: logical reasoning over university regulations, and multi-step physics problem solving. We describe the system that team \cotu{} developed to address both, a neuro-symbolic Program-of-Thought pipeline in which a 4B backbone writes a program rather than stating an answer directly: for regulation queries it emits a Z3 encoding whose entailment verdict grounds the deduction, and for physics it emits numerical Python, both wrapped in a shared self-correction loop and a unified explained-JSON output. Answer-type routing, distillation-based task fine-tuning, and a latency-aware serving stack -- SGLang with speculative decoding -- keep the system within the 60-second per-query limit. The system achieved a \textbf{perfect score} on the physics task in both automated selection rounds and obtained the \textbf{highest final-round technical score} of any team -- $13.44/15$, combining automated answer evaluation with expert-judged reasoning depth -- with the equally weighted presentation score included, \cotu{} placed 3rd overall. Grounding answers in a symbolic solver yields correct, verifiable deductions at the 4B scale, and the residual difficulty lies in premise selection rather than the deduction itself.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。