Due to the wide employment of automated reasoning in the analysis and construction of correct systems, the results reported by automated reasoning engines must be trustworthy. For Boolean satisfiability (SAT) solvers - and more recently SAT-based maximum satisfiability (MaxSAT) solvers - trustworthiness is obtained by integrating proof logging into solvers, making solvers capable of emitting machine-verifiable proofs to certify correctness of the reasoning steps performed. In this work, we enable for the first time proof logging based on the VeriPB proof format for multi-objective MaxSAT (MO-MaxSAT) optimization techniques. Although VeriPB does not offer direct support for multi-objective problems, we detail how preorders in VeriPB can be used to provide certificates for MO-MaxSAT algorithms computing a representative solution for each element in the non-dominated set of the search space under Pareto-optimality, without extending the VeriPB format or the proof checker. By implementing VeriPB proof logging into a state-of-the-art multi-objective MaxSAT solver, we show empirically that proof logging can be made scalable for MO-MaxSAT with reasonable overhead.

Robustness of reasoning remains a significant challenge for large language models, and addressing it is essential for the practical applicability of AI-driven reasoning systems. We introduce Semantic Self-Verification (SSV), a novel approach that addresses the key challenge in combining language models with the rigor of logical solvers: to accurately formulate the reasoning problem from natural language to the formal language of the solver. SSV uses a consistency-based approach to produce strong abstract formalizations of problems using concrete instantiations that are generated by the model and verified by the solver. In addition to significantly advancing the overall reasoning accuracy over the state-of-the-art, a key novelty that this approach presents is a feature of verification that has near-perfect precision over a significant coverage of cases, as we demonstrate on open reasoning benchmarks. We propose such *near-certain reasoning* as a new approach to reduce the need for manual verification in many cases, taking us closer to more dependable and autonomous AI reasoning systems.

Virtually all verification techniques using formal methods rely on the availability of a formal specification, which describes the design requirements precisely. However, formulating specifications remains a manual task that is notoriously challenging and error-prone. To address this bottleneck in formal verification, recent research has thus focussed on automatically generating specifications for formal verification from examples of (desired and undesired) system behavior. In this survey, we list and compare recent advances in mining specifications in Linear Temporal Logic (LTL), the de facto standard specification language for reactive systems. Several approaches have been designed for learning LTL formulas, which address different aspects and settings of specification design. Moreover, the approaches rely on a diverse range of techniques such as constraint solving, neural network training, enumerative search, etc. We survey the current state-of-the-art techniques and compare them for the convenience of the formal methods practitioners.

Summary and Contributions: This paper frames interactive program synthesis as a reference game played between a demonstrator and a synthesizer. The setting is constructing patterns on a 2D grid, where the demonstration iteratively constructs a pattern by placing symbols, and the synthesizer infers a program to complete the output based on the symbols produced so far. The paper applies recursive pragmatic models from the rational speech acts (RSA) framework, deriving a pragmatic synthesizer that models the demonstrator's intention in choosing symbols. This is done by alternating renormalization over demonstrations and over programs, using full enumeration of the set of possible programs and memoization of probabilities. The paper compares pragmatic and non-pragmatic synthesizers, with humans playing the role of the demonstrators. Pragmatic synthesizers have significantly more efficient interactions: the human needs to place fewer symbols on average in order to correctly get the synthesizer to infer the pattern the person was attempting to demonstrate.

This paper studies the problem of programming by example via the lens of rational communication: how can we synthesize programs assuming humans are providing examples in a rational communcation framework? There are some significant weaknesses in the computational aspects of the paper, where it depends on explicit enumeration that limits its scalability. Having said that, reviewers (and AC) are in agreement that this is an interesting new idea that is worth publishing. I agree with R4's updated assessment that "Upon reflection, I think that encouraging work that take into account the human factor in synthesis could be a positive for the NeurIPS community."

The paper claims that the model "learn[s] entire rule systems from a small set of examples". I'm not convinced that this is the case in this work and neither in the previous work which this one extends (i.e. Both methods heavily rely on the supporting set and the specific neural attention architecture of the encoder and decoder which allow for the replacement of individual tokens. This allows the model to exploit a certain pattern in the support set e.g. "a b c - a c a" by replacing the "a" and "b" on-the-fly and execute the abstract rule given by the supporting set.

Learning compositional rules is an important research direction. The proposed method achieves 100% accuracy on different train/test splits of SCAN. My main concern on this work is it seems to be too specific for SCAN, as pointed out by the reviewers.

"Given a large enough time budget the'no REPL' baseline is competitive with our ablated alternatives." However, the policy rollout baseline is trained with RL using a single machine, making it difficult to explore using entropy based methods or epsilon greedy. However, using multiple actors in an asynchronous setting would be a stronger/fairer baseline (and then doing policy rollouts) to the SMC approach. I expect SMC to do well but this is an important empirical question (other methods cited like Ganin et al. seem to do this in the same context). "The value-guided SMC sampler leads to the highest overall number of correct programs, requiring less time and fewer nodes expanded compared to other inference techniques. " - how well does a SMC sampler work without value guided proposals for both case studies?

This paper provides a method for Deep RL-based program synthesis, which exploits a SMC sampler during inference progressively decode into an executable program. The reviewers were enthusiastic about this method and found the experimental support for the proposal convincing. Without much need for further comment, I find the paper of acceptable standard for the conference. The authors are encouraged to take note of the suggestions made by the reviewers, especially R2 and R3, when improving the paper for eventual publication.

Safety verification for autonomous vehicles (AVs) and ground robots is crucial for ensuring reliable operation given their uncertain environments. Formal language tools provide a robust and sound method to verify safety rules for such complex cyber-physical systems. In this paper, we propose a hybrid approach that combines the strengths of formal verification languages like Linear Temporal Logic (LTL) and Signal Temporal Logic (STL) to generate safe trajectories and optimal control inputs for autonomous vehicle navigation. We implement a symbolic path planning approach using LTL to generate a formally safe reference trajectory. A mixed integer linear programming (MILP) solver is then used on this reference trajectory to solve for the control inputs while satisfying the state, control and safety constraints described by STL. We test our proposed solution on two environments and compare the results with popular path planning algorithms. In contrast to conventional path planning algorithms, our formally safe solution excels in handling complex specification scenarios while ensuring both safety and comparable computation times.