Cheng Wen Xi'an University of Electronic Science and Technology, Hu Junjie, YiKun Hu, Jie Su Xi'an University of Electronic Science and Technology, Bin Yu, Dugang Liu Shenzhen University, Zhiwu Xu Shenzhen University, Weidi Sun Peking University 等 10 位作者
Formal verification can provide strong mathematical guarantees about software correctness, but it typically requires developers to write detailed formal specifications (e.g., contracts and loop invariants), which is costly and error-prone. We introduce AutoSpec+, an LLM-driven neuro-symbolic demonstration system that reframes specification writing as constrained structured synthesis: large language models generate candidate specifications at the granularity of proof-relevant program components, while a symbolic verifier acts as a deterministic critic that checks legality, satisfiability, and proof adequacy, rejecting or repairing candidates in an iterative loop. This design turns unconstrained text generation into constrained structured synthesis, substantially reducing hallucinations and producing proof-ready annotations. We evaluate AutoSpec+ on seven benchmark suites, showing strong effectiveness. We release an open-source, Dockerized system with ensemble LLM backends and inter-modular verification support for reproducible demonstration and deployment
尚无 AI 解读，展示原文摘要
cs.CL
Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 3: System Demonstrations) · 2026 · 正式发表
Zexu Sun, Yongcheng Zeng, Erxue Min, Heyang Gao Renmin University of China, Bokai Ji, Dugang Liu Shenzhen University, Xing Tang Shenzhen Technology University, Xiuqiang He 等 9 位作者
Contemporary progress in Large Language Models (LLMs) has revealed notable inferential capacities via reinforcement learning (RL) employing verifiable rewards. However, “zero-RL” approaches relying on fixed prompt templates introduce substantial sampling inefficiencies for weak LLMs, as most problems generate invalid outputs during accuracy-driven filtration. To solve this, we propose Cog-Rethinker, a novel hierarchical metacognitive RL framework. Cog-Rethinker enhances the rollout procedure by improving sample utilization through a two-stage framework leveraging human cognition. First, it prompts the policy to decompose zero-accuracy problems into subproblems. Second, it prompts the policy to refine answers by referencing previous wrong solutions. Moreover, to enable cold-starts and maintain train-test consistency, Cog-Rethinker applies supervised fine-tuning using correct samples from these stages. Experimental results demonstrate Cog-Rethinker’s superior performance on mathematical reasoning benchmarks and its improved sample efficiency that accelerates convergence compared to baselines.
尚无 AI 解读，展示原文摘要
cs.CL
Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) · 2026 · 正式发表