3 papers
cs.SE2026
Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs
Ning Zhang, Nongyu Di, Zenan Li +2
As AI-generated code proliferates, formal verification, particularly through interactive theorem provers such as Rocq and Isabelle, becomes increasingly important for ensuring soft…
cs.SE2026
Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
Nongyu Di, Tianyu Chen, Shan Lu +6
Large Language Models (LLMs) are widely used for code generation. However, the correctness of code generated by LLMs remains a concern. A potential remedy to this concern is to hav…
cs.CL2025
MiniMax-M1: Scaling Test-Time Compute Efficiently with Lightning Attention
MiniMax, :, Aili Chen +125
We introduce MiniMax-M1, the world's first open-weight, large-scale hybrid-attention reasoning model. MiniMax-M1 is powered by a hybrid Mixture-of-Experts (MoE) architecture combin…