SeminarsView all Seminars | Download ICal for this event
Boolean Functional Synthesis using Gated Continuous Logic Networks
Series: M.Tech (Research) Colloquium- ON-LINE
Speaker: Mr. Ravi Raja, M.Tech (Research) student, Dept. of C.S.A
Date/Time: Apr 28 09:00:00
Location: Microsoft Teams - ON-LINE
Faculty Advisor: Prof. Chiranjib Bhattacharyya and Prof. Deepak DSouza
Boolean Functional Synthesis (BFS) is a well-known challenging problem in the domain of automated program synthesis from logical specifications. This problem aims to synthesize a Boolean function that is correct-by-construction with respect to the declared specification; this specification symbolically relates the inputs and outputs of the function to be synthesized. Since Boolean functions are the basic building blocks of modern digital systems, BFS has applications in a wide range of areas, including QBF-SAT solving, circuit repair and debugging. This has motivated the community to develop practically efficient algorithms for synthesizing compact Boolean functions, which is a non-trivial endeavor. However, to the best of our knowledge, current techniques are unable to specify a bound on the Boolean function size during synthesis. Specifying a bound on the size of the formula offers flexibility in synthesizing minimal-sized Boolean functions.
Learning Boolean functions from logical specifications using neural networks is a difficult problem as it requires the network to represent Boolean functions. Boolean functions are discrete functions and consequently, non-differentiable. Thus, learning a Boolean function directly using traditional neural networks is not possible. Recently Ryan et al proposed the Gated Continuous Logic Network (GCLN) model that builds on Fuzzy Logic to represent Boolean and linear integer operator, in the context of learning invariants for programs. In this work, we investigate the use of the GCLN model to synthesize solutions to the BFS problem. Our model lets us bound the number of clauses used in the synthesized Boolean function.
We implement this approach in our tool BNSynth (for Bounded Neural Synthesis), that also uses sampling and counterexample guided techniques to synthesize Boolean functions. We validate our hypothesis that this system can learn smaller functions as compared to a state-of-the-art tool, over custom benchmarks. We observe a 2.4X average improvement in formula size, for these benchmarks. This empirically proves that our system is capable of synthesizing smaller Boolean functions as compared to the state of the art.
Microsoft teams link: