5 papers
Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4
Jianyu Zhang, Fuyuan Zhang, Jiayi Lu +5
Formal methods (FM) are reliable but costly to apply, often requiring years of expert effort in industrial-scale projects such as seL4, especially for theorem proving. Recent advan…
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
Jilin Hu, Jianyu Zhang, Yongwang Zhao +1
Formal methods is pivotal for verifying the reliability of critical systems through rigorous mathematical proofs. However, its adoption is hindered by labor-intensive manual proofs…
Psychometric-Based Evaluation for Theorem Proving with Large Language Models
Jianyu Zhang, Yongwang Zhao, Long Zhang +4
Large language models (LLMs) for formal theorem proving have become a prominent research focus. At present, the proving ability of these LLMs is mainly evaluated through proof pass…
Integrated Modeling, Verification, and Code Generation for Unmanned Aerial Systems
Jianyu Zhang, Long Zhang, Yixuan Wu +2
Unmanned Aerial Systems (UAS) are currently widely used in safety-critical fields such as industrial production, military operations, and disaster relief. Due to the diversity and…
An Agile Formal Specification Language Design Based on K Framework
Jianyu Zhang, Long Zhang, Yixuan Wu +1
Formal Methods (FMs) are currently essential for verifying the safety and reliability of software systems. However, the specification writing in formal methods tends to be complex…