Copertina

Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Yan, Chuanhao, Che, Fengdi, Huang, Xuhan, Xu, Xu, Li, Xin, Li, Yizhi, Qu, Xingwei, Shi, Jingzhe, Lin, Chenghua, Yang, Yaodong, Yuan, Binhang, Zhao, Hang, Qiao, Yu, Zhou, Bowen, Fu, Jie
Natura:	Preprint
Pubblicazione:	2025
Soggetti:	Computation and Language
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
di: Zeng, Lingfei, et al.
Pubblicazione: (2025)

Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification
di: Xu, Xu, et al.
Pubblicazione: (2025)

DafnyBench: A Benchmark for Formal Software Verification
di: Loughridge, Chloe, et al.
Pubblicazione: (2024)

ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization
di: Chen, Guoxin, et al.
Pubblicazione: (2025)

A Tutorial: An Intuitive Explanation of Offline Reinforcement Learning Theory
di: Che, Fengdi
Pubblicazione: (2025)

ReFormer: Generating Radio Fakes for Data Augmentation
di: Kaasaragadda, Yagna, et al.
Pubblicazione: (2024)

DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
di: Banerjee, Debangshu, et al.
Pubblicazione: (2026)

Overview of the NLPCC 2024 Shared Task on Chinese Metaphor Generation
di: Qu, Xingwei, et al.
Pubblicazione: (2024)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
di: Ukhanov, Evgeny
Pubblicazione: (2025)

Dafny as Verification-Aware Intermediate Language for Code Generation
di: Li, Yue Chen, et al.
Pubblicazione: (2025)

Verification of E-Voting Algorithms in Dafny
di: Büttner, Robert, et al.
Pubblicazione: (2025)

dafny-annotator: AI-Assisted Verification of Dafny Programs
di: Poesia, Gabriel, et al.
Pubblicazione: (2024)

From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification
di: Erfan, Md, et al.
Pubblicazione: (2026)

Derivation and Verification of Array Sorting by Merging, and its Certification in Dafny
di: Carbonell, Juan Pablo, et al.
Pubblicazione: (2025)

TinyV: Reducing False Negatives in Verification Improves RL for LLM Reasoning
di: Xu, Zhangchen, et al.
Pubblicazione: (2025)

The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification
di: Tihanyi, Norbert, et al.
Pubblicazione: (2023)

Baking for Dafny: A CakeML Backend for Dafny
di: Nezamabadi, Daniel, et al.
Pubblicazione: (2025)

ReVeal: Self-Evolving Code Agents via Reliable Self-Verification
di: Jin, Yiyang, et al.
Pubblicazione: (2025)

MutDafny: A Mutation-Based Approach to Assess Dafny Specifications
di: Amaral, Isabel, et al.
Pubblicazione: (2025)

Specification-Driven Generation and Evaluation of Discrete-Event World Models via the DEVS Formalism
di: Chen, Zheyu, et al.
Pubblicazione: (2026)

DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
di: Fedchin, Aleksandr, et al.
Pubblicazione: (2025)

Average-DICE: Stationary Distribution Correction by Regression
di: Che, Fengdi, et al.
Pubblicazione: (2025)

Towards a Formal Verification of Secure Vehicle Software Updates
di: Hagen, Martin Slind, et al.
Pubblicazione: (2025)

Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
di: Wojtak, Connor, et al.
Pubblicazione: (2025)

Automated Formal Verification of a Software Fault Isolation System
di: Sotoudeh, Matthew, et al.
Pubblicazione: (2025)

PatchPilot: A Cost-Efficient Software Engineering Agent with Early Attempts on Formal Verification
di: Li, Hongwei, et al.
Pubblicazione: (2025)

Overview of the NLPCC 2025 Shared Task: Gender Bias Mitigation Challenge
di: Li, Yizhi, et al.
Pubblicazione: (2025)

LongEval: A Comprehensive Analysis of Long-Text Generation Through a Plan-based Paradigm
di: Wu, Siwei, et al.
Pubblicazione: (2025)

Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny
di: Carreira, Carolina, et al.
Pubblicazione: (2025)

Distributed Consensus Optimization with Consensus ALADIN
di: Du, Xu, et al.
Pubblicazione: (2025)

CASCADE: A Cascading Architecture for Social Coordination with Controllable Emergence at Low Cost
di: Xu, Yizhi
Pubblicazione: (2026)

Supporting Software Formal Verification with Large Language Models: An Experimental Study
di: Wang, Weiqi, et al.
Pubblicazione: (2025)

The Design of an Interactive Proof Mode for Dafny
di: Ciobâcă, Ştefan, et al.
Pubblicazione: (2025)

Verified VCG and Verified Compiler for Dafny
di: Nezamabadi, Daniel, et al.
Pubblicazione: (2025)

Can Digital Transformation Reduce the Zombification of Enterprises?
di: Xiujuan Lan, et al.
Pubblicazione: (2025)

DocMMIR: A Framework for Document Multi-modal Information Retrieval
di: Li, Zirui, et al.
Pubblicazione: (2025)

Formal Verification of Parameterized Systems based on Induction
di: Xiu, Jiaqi, et al.
Pubblicazione: (2025)

ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
di: Chen, Chen, et al.
Pubblicazione: (2025)

Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds
di: Reinhard, Tobias
Pubblicazione: (2024)

Towards Automated Formal Verification of Backend Systems with LLMs
di: Xu, Kangping, et al.
Pubblicazione: (2025)