Buchumschlag

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Cao, Jialun, Lu, Yaojie, Li, Meiziniu, Ma, Haoyang, Li, Haokun, He, Mengda, Wen, Cheng, Sun, Le, Zhang, Hongyu, Qin, Shengchao, Cheung, Shing-Chi, Tian, Cong
Format:	Preprint
Veröffentlicht:	2025
Schlagworte:	Artificial Intelligence Computation and Language Programming Languages
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
von: Ravi, Nikil, et al.
Veröffentlicht: (2026)

Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure
von: Hattori, Seiji, et al.
Veröffentlicht: (2025)

A Natural Formalized Proof Language
von: Xie, Lihan, et al.
Veröffentlicht: (2024)

Hilbert: Recursively Building Formal Proofs with Informal Reasoning
von: Varambally, Sumanth, et al.
Veröffentlicht: (2025)

Automated Formalization of Probabilistic Requirements from Structured Natural Language
von: Mavridou, Anastasia, et al.
Veröffentlicht: (2025)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
von: Yang, Chengxi, et al.
Veröffentlicht: (2025)

Isolating Language-Coding from Problem-Solving: Benchmarking LLMs with PseudoEval
von: Wu, Jiarong, et al.
Veröffentlicht: (2025)

Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
von: Wen, Cheng, et al.
Veröffentlicht: (2024)

Formally Verified Linear-Time Invertible Lexing
von: Chassot, Samuel, et al.
Veröffentlicht: (2025)

Enhancing Differential Testing With LLMs For Testing Deep Learning Libraries
von: Li, Meiziniu, et al.
Veröffentlicht: (2024)

NILE: Formalizing Natural-Language Descriptions of Formal Languages
von: Kneisel, Tristan, et al.
Veröffentlicht: (2026)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
von: Monniaux, David
Veröffentlicht: (2024)

Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference
von: Le-Cong, Thanh, et al.
Veröffentlicht: (2025)

APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
von: Xin, Huajian, et al.
Veröffentlicht: (2025)

Formal-LLM: Integrating Formal Language and Natural Language for Controllable LLM-based Agents
von: Li, Zelong, et al.
Veröffentlicht: (2024)

ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair
von: Chen, Zhiyong, et al.
Veröffentlicht: (2026)

CktFormalizer: Autoformalization of Natural Language into Circuit Representations
von: Xiong, Jing, et al.
Veröffentlicht: (2026)

Bounded Exhaustive Random Program Generation for Testing Solidity Compilers
von: Ma, Haoyang, et al.
Veröffentlicht: (2025)

Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability
von: Wang, Ruida, et al.
Veröffentlicht: (2025)

Closure Properties of General Grammars -- Formally Verified
von: Dvorak, Martin, et al.
Veröffentlicht: (2023)

Minuska: Towards a Formally Verified Programming Language Framework
von: Tušil, Jan, et al.
Veröffentlicht: (2024)

Formal Foundations for Translational Separation Logic Verifiers (extended version)
von: Dardinier, Thibault, et al.
Veröffentlicht: (2024)

FMC: Formalization of Natural Language Mathematical Competition Problems
von: Xie, Jiaxuan, et al.
Veröffentlicht: (2025)

Learning from Failures: Correction-Oriented Policy Optimization with Verifiable Rewards
von: Ren, Mengjie, et al.
Veröffentlicht: (2026)

Verified Code Transpilation with LLMs
von: Bhatia, Sahil, et al.
Veröffentlicht: (2024)

A Formally Verified Procedure for Width Inference in FIRRTL
von: Wang, Keyin, et al.
Veröffentlicht: (2026)

Logical Relations for Formally Verified Authenticated Data Structures
von: Gregersen, Simon Oddershede, et al.
Veröffentlicht: (2025)

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes
von: Wang, Shuling, et al.
Veröffentlicht: (2024)

Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts
von: Huyghebaert, Sander, et al.
Veröffentlicht: (2023)

VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning
von: Singh, Vikash, et al.
Veröffentlicht: (2026)

COMET: Coverage-guided Model Generation For Deep Learning Library Testing
von: Li, Meiziniu, et al.
Veröffentlicht: (2022)

Executing Natural Language-Described Algorithms with Large Language Models: An Investigation
von: Zheng, Xin, et al.
Veröffentlicht: (2024)

Are LLMs Stable Formal Logic Translators in Logical Reasoning Across Linguistically Diversified Texts?
von: Li, Qingchuan, et al.
Veröffentlicht: (2025)

Tricking LLMs into Disobedience: Formalizing, Analyzing, and Detecting Jailbreaks
von: Rao, Abhinav, et al.
Veröffentlicht: (2023)

On the Limit of Language Models as Planning Formalizers
von: Huang, Cassie, et al.
Veröffentlicht: (2024)

A Formally Verified Robustness Certifier for Neural Networks (Extended Version)
von: Tobler, James, et al.
Veröffentlicht: (2025)

Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
von: Baumann, Jonathan, et al.
Veröffentlicht: (2026)

Formal Aspects of Language Modeling
von: Cotterell, Ryan, et al.
Veröffentlicht: (2023)

A Reality Check of Language Models as Formalizers on Constraint Satisfaction Problems
von: Amonkar, Rikhil, et al.
Veröffentlicht: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
von: Coglio, Alessandro, et al.
Veröffentlicht: (2025)