Towards Semantics Lifting for Scientific Computing: A Case Study on FFT
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910786658500608 |
|---|---|
| author | Zhang, Naifeng Rao, Sanil Franusich, Mike Franchetti, Franz |
| author_facet | Zhang, Naifeng Rao, Sanil Franusich, Mike Franchetti, Franz |
| contents | The rise of automated code generation tools, such as large language models (LLMs), has introduced new challenges in ensuring the correctness and efficiency of scientific software, particularly in complex kernels, where numerical stability, domain-specific optimizations, and precise floating-point arithmetic are critical. We propose a stepwise semantics lifting approach using an extended SPIRAL framework with symbolic execution and theorem proving to statically derive high-level code semantics from LLM-generated kernels. This method establishes a structured path for verifying the source code's correctness via a step-by-step lifting procedure to high-level specification. We conducted preliminary tests on the feasibility of this approach by successfully lifting GPT-generated fast Fourier transform code to high-level specifications. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_09201 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Towards Semantics Lifting for Scientific Computing: A Case Study on FFT Zhang, Naifeng Rao, Sanil Franusich, Mike Franchetti, Franz Programming Languages Symbolic Computation The rise of automated code generation tools, such as large language models (LLMs), has introduced new challenges in ensuring the correctness and efficiency of scientific software, particularly in complex kernels, where numerical stability, domain-specific optimizations, and precise floating-point arithmetic are critical. We propose a stepwise semantics lifting approach using an extended SPIRAL framework with symbolic execution and theorem proving to statically derive high-level code semantics from LLM-generated kernels. This method establishes a structured path for verifying the source code's correctness via a step-by-step lifting procedure to high-level specification. We conducted preliminary tests on the feasibility of this approach by successfully lifting GPT-generated fast Fourier transform code to high-level specifications. |
| title | Towards Semantics Lifting for Scientific Computing: A Case Study on FFT |
| topic | Programming Languages Symbolic Computation |
| url | https://arxiv.org/abs/2501.09201 |