-
Autoformalization in the Era of Large Language Models: A Survey
Authors:
Ke Weng,
Lun Du,
Sirui Li,
Wangyue Lu,
Haozhe Sun,
Hengyu Liu,
Tiancheng Zhang
Abstract:
Autoformalization, the process of transforming informal mathematical propositions into verifiable formal representations, is a foundational task in automated theorem proving, offering a new perspective on the use of mathematics in both theoretical and applied domains. Driven by the rapid progress in artificial intelligence, particularly large language models (LLMs), this field has witnessed substa…
▽ More
Autoformalization, the process of transforming informal mathematical propositions into verifiable formal representations, is a foundational task in automated theorem proving, offering a new perspective on the use of mathematics in both theoretical and applied domains. Driven by the rapid progress in artificial intelligence, particularly large language models (LLMs), this field has witnessed substantial growth, bringing both new opportunities and unique challenges. In this survey, we provide a comprehensive overview of recent advances in autoformalization from both mathematical and LLM-centric perspectives. We examine how autoformalization is applied across various mathematical domains and levels of difficulty, and analyze the end-to-end workflow from data preprocessing to model design and evaluation. We further explore the emerging role of autoformalization in enhancing the verifiability of LLM-generated outputs, highlighting its potential to improve both the trustworthiness and reasoning capabilities of LLMs. Finally, we summarize key open-source models and datasets supporting current research, and discuss open challenges and promising future directions for the field.
△ Less
Submitted 3 July, 2025; v1 submitted 29 May, 2025;
originally announced May 2025.
-
BiDexHand: Design and Evaluation of an Open-Source 16-DoF Biomimetic Dexterous Hand
Authors:
Zhengyang Kris Weng
Abstract:
Achieving human-level dexterity in robotic hands remains a fundamental challenge for enabling versatile manipulation across diverse applications. This extended abstract presents BiDexHand, a cable-driven biomimetic robotic hand that combines human-like dexterity with accessible and efficient mechanical design. The robotic hand features 16 independently actuated degrees of freedom and 5 mechanicall…
▽ More
Achieving human-level dexterity in robotic hands remains a fundamental challenge for enabling versatile manipulation across diverse applications. This extended abstract presents BiDexHand, a cable-driven biomimetic robotic hand that combines human-like dexterity with accessible and efficient mechanical design. The robotic hand features 16 independently actuated degrees of freedom and 5 mechanically coupled joints through novel phalange designs that replicate natural finger motion. Performance validation demonstrated success across all 33 grasp types in the GRASP Taxonomy, 9 of 11 positions in the Kapandji thumb opposition test, a measured fingertip force of 2.14\,N, and the capability to lift a 10\,lb weight. As an open-source platform supporting multiple control modes including vision-based teleoperation, BiDexHand aims to democratize access to advanced manipulation capabilities for the broader robotics research community.
△ Less
Submitted 20 April, 2025;
originally announced April 2025.
-
EfficientRep:An Efficient Repvgg-style ConvNets with Hardware-aware Neural Network Design
Authors:
Kaiheng Weng,
Xiangxiang Chu,
Xiaoming Xu,
Junshi Huang,
Xiaoming Wei
Abstract:
We present a hardware-efficient architecture of convolutional neural network, which has a repvgg-like architecture. Flops or parameters are traditional metrics to evaluate the efficiency of networks which are not sensitive to hardware including computing ability and memory bandwidth. Thus, how to design a neural network to efficiently use the computing ability and memory bandwidth of hardware is a…
▽ More
We present a hardware-efficient architecture of convolutional neural network, which has a repvgg-like architecture. Flops or parameters are traditional metrics to evaluate the efficiency of networks which are not sensitive to hardware including computing ability and memory bandwidth. Thus, how to design a neural network to efficiently use the computing ability and memory bandwidth of hardware is a critical problem. This paper proposes a method how to design hardware-aware neural network. Based on this method, we designed EfficientRep series convolutional networks, which are high-computation hardware(e.g. GPU) friendly and applied in YOLOv6 object detection framework. YOLOv6 has published YOLOv6N/YOLOv6S/YOLOv6M/YOLOv6L models in v1 and v2 versions.
△ Less
Submitted 1 February, 2023;
originally announced February 2023.
-
Statistical Physics of Deep Neural Networks: Initialization toward Optimal Channels
Authors:
Kangyu Weng,
Aohua Cheng,
Ziyang Zhang,
Pei Sun,
Yang Tian
Abstract:
In deep learning, neural networks serve as noisy channels between input data and its representation. This perspective naturally relates deep learning with the pursuit of constructing channels with optimal performance in information transmission and representation. While considerable efforts are concentrated on realizing optimal channel properties during network optimization, we study a frequently…
▽ More
In deep learning, neural networks serve as noisy channels between input data and its representation. This perspective naturally relates deep learning with the pursuit of constructing channels with optimal performance in information transmission and representation. While considerable efforts are concentrated on realizing optimal channel properties during network optimization, we study a frequently overlooked possibility that neural networks can be initialized toward optimal channels. Our theory, consistent with experimental validation, identifies primary mechanics underlying this unknown possibility and suggests intrinsic connections between statistical physics and deep learning. Unlike the conventional theories that characterize neural networks applying the classic mean-filed approximation, we offer analytic proof that this extensively applied simplification scheme is not valid in studying neural networks as information channels. To fill this gap, we develop a corrected mean-field framework applicable for characterizing the limiting behaviors of information propagation in neural networks without strong assumptions on inputs. Based on it, we propose an analytic theory to prove that mutual information maximization is realized between inputs and propagated signals when neural networks are initialized at dynamic isometry, a case where information transmits via norm-preserving mappings. These theoretical predictions are validated by experiments on real neural networks, suggesting the robustness of our theory against finite-size effects. Finally, we analyze our findings with information bottleneck theory to confirm the precise relations among dynamic isometry, mutual information maximization, and optimal channel properties in deep learning.
△ Less
Submitted 4 December, 2022;
originally announced December 2022.
-
YOLOv6: A Single-Stage Object Detection Framework for Industrial Applications
Authors:
Chuyi Li,
Lulu Li,
Hongliang Jiang,
Kaiheng Weng,
Yifei Geng,
Liang Li,
Zaidan Ke,
Qingyuan Li,
Meng Cheng,
Weiqiang Nie,
Yiduo Li,
Bo Zhang,
Yufei Liang,
Linyuan Zhou,
Xiaoming Xu,
Xiangxiang Chu,
Xiaoming Wei,
Xiaolin Wei
Abstract:
For years, the YOLO series has been the de facto industry-level standard for efficient object detection. The YOLO community has prospered overwhelmingly to enrich its use in a multitude of hardware platforms and abundant scenarios. In this technical report, we strive to push its limits to the next level, stepping forward with an unwavering mindset for industry application.
Considering the divers…
▽ More
For years, the YOLO series has been the de facto industry-level standard for efficient object detection. The YOLO community has prospered overwhelmingly to enrich its use in a multitude of hardware platforms and abundant scenarios. In this technical report, we strive to push its limits to the next level, stepping forward with an unwavering mindset for industry application.
Considering the diverse requirements for speed and accuracy in the real environment, we extensively examine the up-to-date object detection advancements either from industry or academia. Specifically, we heavily assimilate ideas from recent network design, training strategies, testing techniques, quantization, and optimization methods. On top of this, we integrate our thoughts and practice to build a suite of deployment-ready networks at various scales to accommodate diversified use cases. With the generous permission of YOLO authors, we name it YOLOv6. We also express our warm welcome to users and contributors for further enhancement. For a glimpse of performance, our YOLOv6-N hits 35.9% AP on the COCO dataset at a throughput of 1234 FPS on an NVIDIA Tesla T4 GPU. YOLOv6-S strikes 43.5% AP at 495 FPS, outperforming other mainstream detectors at the same scale~(YOLOv5-S, YOLOX-S, and PPYOLOE-S). Our quantized version of YOLOv6-S even brings a new state-of-the-art 43.3% AP at 869 FPS. Furthermore, YOLOv6-M/L also achieves better accuracy performance (i.e., 49.5%/52.3%) than other detectors with a similar inference speed. We carefully conducted experiments to validate the effectiveness of each component. Our code is made available at https://github.com/meituan/YOLOv6.
△ Less
Submitted 7 September, 2022;
originally announced September 2022.
-
A Manifold Learning Approach to Accelerate Phase Field Fracture Simulations in the Representative Volume Element
Authors:
Yangyuanchen Liu,
Kexin Weng,
Yongxing Shen
Abstract:
The multiscale simulation of heterogeneous materials is a popular and important subject in solid mechanics and materials science due to the wide application of composite materials. However, the classical FE2 (finite element2) scheme can be costly, especially when the microproblem is nonlinear. In this paper, we consider the case when the microproblem is the phase field formulation for fracture. We…
▽ More
The multiscale simulation of heterogeneous materials is a popular and important subject in solid mechanics and materials science due to the wide application of composite materials. However, the classical FE2 (finite element2) scheme can be costly, especially when the microproblem is nonlinear. In this paper, we consider the case when the microproblem is the phase field formulation for fracture. We adopt the locally linear embedding (LLE) manifold learning approach, a method for non-linear dimension reduction, to extract the manifold that contains a collection of phase-field-represented initial microcrack patterns in the representative volume element (RVE). Then the output data corresponding to any other microcrack pattern, e.g., the evolved phase field at a fixed load, can be accurately reconstructed using the learned manifold with minimum computation. The method has two features: a minimum number of parameters for the scheme, and an input-specific error bar. The latter feature enables an adaptive strategy for any new input on whether to use the proposed, less expensive reconstruction, or to use an accurate but costly high-fidelity computation instead.
△ Less
Submitted 20 July, 2020;
originally announced July 2020.
-
Convo: What does conversational programming need? An exploration of machine learning interface design
Authors:
Jessica Van Brummelen,
Kevin Weng,
Phoebe Lin,
Catherine Yeo
Abstract:
Vast improvements in natural language understanding and speech recognition have paved the way for conversational interaction with computers. While conversational agents have often been used for short goal-oriented dialog, we know little about agents for developing computer programs. To explore the utility of natural language for programming, we conducted a study ($n$=45) comparing different input…
▽ More
Vast improvements in natural language understanding and speech recognition have paved the way for conversational interaction with computers. While conversational agents have often been used for short goal-oriented dialog, we know little about agents for developing computer programs. To explore the utility of natural language for programming, we conducted a study ($n$=45) comparing different input methods to a conversational programming system we developed. Participants completed novice and advanced tasks using voice-based, text-based, and voice-or-text-based systems. We found that users appreciated aspects of each system (e.g., voice-input efficiency, text-input precision) and that novice users were more optimistic about programming using voice-input than advanced users. Our results show that future conversational programming tools should be tailored to users' programming experience and allow users to choose their preferred input mode. To reduce cognitive load, future interfaces can incorporate visualizations and possess custom natural language understanding and speech recognition models for programming.
△ Less
Submitted 2 March, 2020;
originally announced March 2020.
