دورية أكاديمية
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming ...
| العنوان: | Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming ... |
|---|---|
| المؤلفون: | Chakraborty, Saikat, Ebner, Gabriel, Bhat, Siddharth, Fakhoury, Sarah, Fatima, Sakina, Lahiri, Shuvendu, Swamy, Nikhil |
| بيانات النشر: | arXiv |
| سنة النشر: | 2024 |
| المجموعة: | DataCite Metadata Store (German National Library of Science and Technology) |
| مصطلحات موضوعية: | Programming Languages cs.PL, Artificial Intelligence cs.AI, Software Engineering cs.SE, FOS Computer and information sciences |
| الوصف: | Proof-oriented programs mix computational content with proofs of program correctness. However, the human effort involved in programming and proving is still substantial, despite the use of Satisfiability Modulo Theories (SMT) solvers to automate proofs in languages such as F*. Seeking to spur research on using AI to automate the construction of proof-oriented programs, we curate a dataset of 600K lines of open-source F* programs and proofs, including software used in production systems ranging from Windows and Linux, to Python and Firefox. Our dataset includes around 32K top-level F* definitions, each representing a type-directed program and proof synthesis problem -- producing a definition given a formal specification expressed as an F* type. We provide a program-fragment checker that queries F* to check the correctness of candidate solutions. We believe this is the largest corpus of SMT-assisted program proofs coupled with a reproducible program-fragment checker. Grounded in this dataset, we investigate ... |
| نوع الوثيقة: | article in journal/newspaper report |
| اللغة: | unknown |
| DOI: | 10.48550/arxiv.2405.01787 |
| الإتاحة: | https://doi.org/10.48550/arxiv.2405.01787Test https://arxiv.org/abs/2405.01787Test |
| حقوق: | Creative Commons Attribution 4.0 International ; https://creativecommons.org/licenses/by/4.0/legalcodeTest ; cc-by-4.0 |
| رقم الانضمام: | edsbas.98B58523 |
| قاعدة البيانات: | BASE |
| DOI: | 10.48550/arxiv.2405.01787 |
|---|