13 papers
AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language
Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang +4
Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this e…
Training and Benchmarking Code Generation for Physics-Inspired Animations
Yanan Wang, Renxi Wang, Yongxin Wang +5
Large language models (LLMs) have been widely studied in areas such as mathematical reasoning, complex coding, and scientific problem solving. However, their ability to generate ex…
Neural Theorem Proving for Verification Conditions: A Real-World Benchmark
Qiyuan Xu, Xiaokun Luan, Renxi Wang +5
Theorem proving is fundamental to program verification, where the automated proof of Verification Conditions (VCs) remains a primary bottleneck. Real-world program verification fre…
K2-V2: A 360-Open, Reasoning-Enhanced LLM
K2 Team, Zhengzhong Liu, Liping Tang +36
We introduce K2-V2, a 360-open LLM built from scratch as a superior base for reasoning adaptation, in addition to functions such as conversation and knowledge retrieval from genera…
SCALAR: Scientific Citation-based Live Assessment of Long-context Academic Reasoning
Renxi Wang, Honglin Mu, Liqun Ma +5
Long-context understanding has emerged as a critical capability for large language models (LLMs). However, evaluating this ability remains challenging. We present SCALAR, a benchma…
A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
Qiyuan Xu, Renxi Wang, Peixin Wang +2
Neural Theorem Proving (NTP) employs LLMs to automate formal proofs in proof assistants. While LLMs have achieved relatively remarkable success in informal reasoning tasks using na…