3 papers
cs.CR2026
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…
cs.FL2025
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…
cs.AI2025
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…