Pith. sign in

REVIEW 3 cited by

Towards Semantics Lifting for Scientific Computing: A Case Study on FFT

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2501.09201 v1 pith:6IP4OQM2 submitted 2025-01-15 cs.PL cs.SC

Naifeng Zhang , Sanil Rao , Mike Franusich , Franz Franchetti This is my paper
classification cs.PLcs.SC
keywords codeliftinghigh-levelsemanticsapproachcorrectnesskernelsscientific
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

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.

Discussion (0). Sign in to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Uncovering Business Logic Bugs via Semantics-Driven Unit Test Generation

    cs.SE 2026-04 conditional novelty 7.0 of 10

    SeGa extracts business semantics from requirements to generate unit tests that detect 22-25 more real-world business logic bugs than prior LLM-based methods in industrial Go projects.

  2. Uncovering Business Logic Bugs via Semantics-Driven Unit Test Generation

    cs.SE 2026-04 conditional novelty 6.0 of 10

    SeGa detects 29 of 60 real business-logic bugs by generating tests from requirement-document scenarios, 22-25 more than four LLM-based baselines.

  3. Aligning Requirement for Large Language Model's Code Generation

    cs.SE 2025-09 conditional novelty 5.0 of 10

    An LLM-based specification-alignment method that lifts the model's perceived requirements from generated code and applies ten alignment rules improves Pass@1 by about 30% over existing baselines.

Pith tools