6 papers
Aligning Faithfulness for Theory-Scale Autoformalization
Yuming Feng, Tadd Mao, Dhruva Arekar +4
Autoformalization (AF) requires more than compilation: formal statements must preserve the meaning of their informal sources, a property known as faithfulness. An emerging frontier…
Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs
Tadd Mao, Tianjun Zhong, Dhruva Arekar +5
In formal verification, both the autoformalization of statements and automated proof search have been studied extensively. While automated proof search can produce a formal proof t…
SWE-Spot: Building Small Repo-Experts with Repository-Centric Learning
Jinjun Peng, Magnus Saebo, Tianjun Zhong +6
The deployment of coding agents in privacy-sensitive and resource-constrained environments drives the demand for capable open-weight Small Language Models (SLMs). However, they suf…
LLMs Think with DAGs: Probing the Latent Graph Structure of Reasoning
Tianjun Zhong, Linyang He, Ziyang Li +1
Large language models often externalize reasoning as linear chains, but many reasoning problems can be more naturally modeled as directed acyclic graphs (DAGs), where intermediate…
Far from the Shallow: Brain-Predictive Reasoning Embedding through Residual Disentanglement
Linyang He, Tianjun Zhong, Richard Antonello +3
Understanding how the human brain progresses from processing simple linguistic inputs to performing high-level reasoning is a fundamental challenge in neuroscience. While modern la…
K2-Think: A Parameter-Efficient Reasoning System
Zhoujun Cheng, Richard Fan, Shibo Hao +28
K2-Think is a reasoning system that achieves state-of-the-art performance with a 32B parameter model, matching or surpassing much larger models like GPT-OSS 120B and DeepSeek v3.1.…