Invariant Relations: A Bridge from Programs to Equations
- URL: http://arxiv.org/abs/2310.04684v1
- Date: Sat, 7 Oct 2023 04:11:23 GMT
- Title: Invariant Relations: A Bridge from Programs to Equations
- Authors: Wided Ghardallou, Hessamaldin Mohammadi, Elijah Brick, Ali Mili
- Abstract summary: We propose a method to derive the function of a C-like program, including programs that have loops nested to an arbitrary level.
To capture the semantics of loops, we use the concept of invariant relation.
- Score: 1.3342735568824553
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Great advances in program analysis would be enabled if it were possible to
derive the function of a program from inputs to outputs (or from initial states
to final states, depending on how we model program semantics). Efforts to do so
have always stalled against the difficulty to derive the function of loops; the
expedient solution to capture the function of loops by unrolling them an
arbitrary number of iterations is clearly inadequate. In this paper, we propose
a relations-based method to derive the function of a C-like program, including
programs that have loops nested to an arbitrary level. To capture the semantics
of loops, we use the concept of invariant relation.
Related papers
- A Formal Comparison Between Chain-of-Thought and Latent Thought [32.84174396586435]
Chain-of-Thought (CoT) elicits reasoning in large language models by explicitly generating intermediate steps in natural language.<n>Latent Thought in looped models operates directly in the continuous latent space, enabling computation beyond discrete linguistic representations.
arXiv Detail & Related papers (2025-09-25T11:27:52Z) - To CoT or To Loop? A Formal Comparison Between Chain-of-Thought and Looped Transformers [32.01426831450348]
Chain-of-Thought (CoT) and Looped Transformers have been shown to empirically improve performance on reasoning tasks.<n>We provide a formal analysis of their respective strengths and limitations.
arXiv Detail & Related papers (2025-05-25T17:49:37Z) - Single-loop Algorithms for Stochastic Non-convex Optimization with Weakly-Convex Constraints [49.76332265680669]
This paper examines a crucial subset of problems where both the objective and constraint functions are weakly convex.
Existing methods often face limitations, including slow convergence rates or reliance on double-loop designs.
We introduce a novel single-loop penalty-based algorithm to overcome these challenges.
arXiv Detail & Related papers (2025-04-21T17:15:48Z) - The nature of loops in programming [37.48416208168878]
In program semantics and verification, reasoning about loops is complicated by the need to produce two separate mathematical arguments.
A single and simple definition is possible, removing this split.
To prove the loop correct there is no need to devise an invariant and a variant.
It suffices to identify the relation, yielding both partial correctness and termination.
arXiv Detail & Related papers (2025-04-10T20:58:55Z) - Origami: (un)folding the abstraction of recursion schemes for program
synthesis [0.0]
Genetic Programming searches for a correct program that satisfies the input specification.
One particular challenge is how to handle loops and recursion avoiding programs that never terminate.
Recursion Schemes generalize the combination of data production and consumption.
arXiv Detail & Related papers (2024-02-21T14:17:45Z) - Finding Inductive Loop Invariants using Large Language Models [14.846222005558666]
Finding inductive loop invariants is an undecidable problem.
Despite a long history of research towards practical solutions, it remains far from a solved problem.
This paper investigates the capabilities of the Large Language Models in offering a new solution.
arXiv Detail & Related papers (2023-11-14T06:58:09Z) - Will Bilevel Optimizers Benefit from Loops [63.22466953441521]
Two current popular bilevelimats AID-BiO and ITD-BiO naturally involve solving one or two sub-problems.
We first establish unified convergence analysis for both AID-BiO and ITD-BiO that are applicable to all implementation choices of loops.
arXiv Detail & Related papers (2022-05-27T20:28:52Z) - Guaranteed Bounds for Posterior Inference in Universal Probabilistic
Programming [4.297070083645049]
We prove that the actual posterior of a given program is sandwiched between the lower and upper bounds (soundness)
We introduce a weight-aware interval type system, which automatically infers interval bounds on not just the return value but also weight of program executions, simultaneously.
Our evaluation on examples from the literature shows that the bounds are useful, and can even be used to recognise wrong outputs from posterior inference procedures.
arXiv Detail & Related papers (2022-04-06T17:28:28Z) - Iterative Genetic Improvement: Scaling Stochastic Program Synthesis [11.195558777385259]
Program synthesis aims to it automatically find programs from an underlying programming language that satisfy a given specification.
Existing program synthesis techniques do not meet this expectation very well, suffering from the scalability issue.
Here we propose a new framework for program synthesis, called iterative genetic improvement to overcome this problem.
arXiv Detail & Related papers (2022-02-26T02:00:35Z) - A Fully Single Loop Algorithm for Bilevel Optimization without Hessian
Inverse [121.54116938140754]
We propose a new Hessian inverse free Fully Single Loop Algorithm for bilevel optimization problems.
We show that our algorithm converges with the rate of $O(epsilon-2)$.
arXiv Detail & Related papers (2021-12-09T02:27:52Z) - Searching for More Efficient Dynamic Programs [61.79535031840558]
We describe a set of program transformations, a simple metric for assessing the efficiency of a transformed program, and a search procedure to improve this metric.
We show that in practice, automated search can find substantial improvements to the initial program.
arXiv Detail & Related papers (2021-09-14T20:52:55Z) - Enforcing Consistency in Weakly Supervised Semantic Parsing [68.2211621631765]
We explore the use of consistency between the output programs for related inputs to reduce the impact of spurious programs.
We find that a more consistent formalism leads to improved model performance even without consistency-based training.
arXiv Detail & Related papers (2021-07-13T03:48:04Z) - Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
We introduce a technique for representing partially written programs in a program synthesis engine.
We learn an approximate execution model implemented as a modular neural network.
We show that these hybrid neuro-symbolic representations enable execution-guided synthesizers to use more powerful language constructs.
arXiv Detail & Related papers (2020-12-23T20:40:18Z) - Latent Programmer: Discrete Latent Codes for Program Synthesis [56.37993487589351]
In many sequence learning tasks, such as program synthesis and document summarization, a key problem is searching over a large space of possible output sequences.
We propose to learn representations of the outputs that are specifically meant for search: rich enough to specify the desired output but compact enough to make search more efficient.
We introduce the emphLatent Programmer, a program synthesis method that first predicts a discrete latent code from input/output examples, and then generates the program in the target language.
arXiv Detail & Related papers (2020-12-01T10:11:35Z) - Translating Recursive Probabilistic Programs to Factor Graph Grammars [20.539191533339427]
A factor graph grammar (FGG) generates a set of factor graphs that do not all need to be enumerated in order to perform inference.
We provide a semantics-preserving translation from first-order probabilistic programs with conditionals and recursion to FGGs.
arXiv Detail & Related papers (2020-10-22T21:17:04Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.