From 7330a0814df2aec8c5d6010802178f80f4525cdd Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 27 May 2024 15:49:23 -0700 Subject: [PATCH] solver-based neural ranking engine This adds a variant of neural ranking that uses a SAT/SMT solver to compute the weights and biases in the neural network. --- examples/Benchmarks/run_solver_nuterm | 158 +++++ .../ebmc/solver-neural-liveness/counter1.desc | 9 + .../ebmc/solver-neural-liveness/counter1.sv | 16 + .../solver-neural-liveness/wrap_around1.desc | 9 + .../solver-neural-liveness/wrap_around1.sv | 18 + src/ebmc/Makefile | 3 +- src/ebmc/ebmc_parse_options.cpp | 11 +- src/ebmc/ebmc_parse_options.h | 3 +- src/ebmc/neural.cpp | 587 ++++++++++++++++++ src/ebmc/neural.h | 27 + src/ebmc/property_checker.cpp | 12 +- src/ebmc/ranking_net.cpp | 106 ++++ src/ebmc/ranking_net.h | 59 ++ ...al_liveness.h => solver_neural_liveness.h} | 10 +- 14 files changed, 1012 insertions(+), 16 deletions(-) create mode 100755 examples/Benchmarks/run_solver_nuterm create mode 100644 regression/ebmc/solver-neural-liveness/counter1.desc create mode 100644 regression/ebmc/solver-neural-liveness/counter1.sv create mode 100644 regression/ebmc/solver-neural-liveness/wrap_around1.desc create mode 100644 regression/ebmc/solver-neural-liveness/wrap_around1.sv create mode 100644 src/ebmc/neural.cpp create mode 100644 src/ebmc/neural.h create mode 100644 src/ebmc/ranking_net.cpp create mode 100644 src/ebmc/ranking_net.h rename src/ebmc/{neural_liveness.h => solver_neural_liveness.h} (52%) diff --git a/examples/Benchmarks/run_solver_nuterm b/examples/Benchmarks/run_solver_nuterm new file mode 100755 index 000000000..e60eccb18 --- /dev/null +++ b/examples/Benchmarks/run_solver_nuterm @@ -0,0 +1,158 @@ +#!/bin/sh + +set -e + +if false ; then +# ok +ebmc PWM_1.sv --solver-neural-liveness +ebmc PWM_2.sv --solver-neural-liveness +ebmc PWM_3.sv --solver-neural-liveness +ebmc PWM_4.sv --solver-neural-liveness +ebmc PWM_5.sv --solver-neural-liveness +ebmc PWM_6.sv --solver-neural-liveness +ebmc PWM_7.sv --solver-neural-liveness +ebmc PWM_8.sv --solver-neural-liveness +ebmc PWM_9.sv --solver-neural-liveness +fi + +if false ; then +# ok +ebmc delay_1.sv --solver-neural-liveness +ebmc delay_2.sv --solver-neural-liveness +ebmc delay_3.sv --solver-neural-liveness +ebmc delay_4.sv --solver-neural-liveness +ebmc delay_5.sv --solver-neural-liveness +ebmc delay_6.sv --solver-neural-liveness +ebmc delay_7.sv --solver-neural-liveness +ebmc delay_8.sv --solver-neural-liveness +ebmc delay_9.sv --solver-neural-liveness +ebmc delay_10.sv --solver-neural-liveness +ebmc delay_11.sv --solver-neural-liveness +ebmc delay_12.sv --solver-neural-liveness +ebmc delay_13.sv --solver-neural-liveness +ebmc delay_14.sv --solver-neural-liveness +ebmc delay_15.sv --solver-neural-liveness +ebmc delay_16.sv --solver-neural-liveness +fi + +if false ; then +# ok +ebmc gray_1.sv --solver-neural-liveness +ebmc gray_2.sv --solver-neural-liveness +ebmc gray_3.sv --solver-neural-liveness +ebmc gray_4.sv --solver-neural-liveness +ebmc gray_5.sv --solver-neural-liveness +ebmc gray_6.sv --solver-neural-liveness +ebmc gray_7.sv --solver-neural-liveness +ebmc gray_8.sv --solver-neural-liveness +ebmc gray_9.sv --solver-neural-liveness +ebmc gray_10.sv --solver-neural-liveness +ebmc gray_11.sv --solver-neural-liveness +fi + +if false ; then +ebmc i2c_1.sv --solver-neural-liveness +ebmc i2c_2.sv --solver-neural-liveness +ebmc i2c_3.sv --solver-neural-liveness +ebmc i2c_4.sv --solver-neural-liveness +ebmc i2c_5.sv --solver-neural-liveness +ebmc i2c_6.sv --solver-neural-liveness +ebmc i2c_7.sv --solver-neural-liveness +ebmc i2c_8.sv --solver-neural-liveness +ebmc i2c_9.sv --solver-neural-liveness +ebmc i2c_10.sv --solver-neural-liveness +ebmc i2c_11.sv --solver-neural-liveness +ebmc i2c_12.sv --solver-neural-liveness +ebmc i2c_13.sv --solver-neural-liveness +ebmc i2c_14.sv --solver-neural-liveness +ebmc i2c_15.sv --solver-neural-liveness +ebmc i2c_16.sv --solver-neural-liveness +ebmc i2c_17.sv --solver-neural-liveness +ebmc i2c_18.sv --solver-neural-liveness +ebmc i2c_19.sv --solver-neural-liveness +ebmc i2c_20.sv --solver-neural-liveness +fi + +if false ; then +ebmc lcd_1.sv --solver-neural-liveness "{3-state,500-cnt}" +ebmc lcd_2.sv --solver-neural-liveness "{3-state,1000-cnt}" +ebmc lcd_3.sv --solver-neural-liveness "{3-state,1500-cnt}" +ebmc lcd_4.sv --solver-neural-liveness "{3-state,2500-cnt}" +ebmc lcd_5.sv --solver-neural-liveness "{3-state,5000-cnt}" +ebmc lcd_6.sv --solver-neural-liveness "{3-state,7500-cnt}" +ebmc lcd_7.sv --solver-neural-liveness "{3-state,10000-cnt}" +ebmc lcd_8.sv --solver-neural-liveness "{3-state,12500-cnt}" +ebmc lcd_9.sv --solver-neural-liveness "{3-state,15000-cnt}" +ebmc lcd_10.sv --solver-neural-liveness "{3-state,17500-cnt}" +ebmc lcd_11.sv --solver-neural-liveness "{3-state,20000-cnt}" +ebmc lcd_12.sv --solver-neural-liveness "{3-state,22500-cnt}" +ebmc lcd_13.sv --solver-neural-liveness "{3-state,90000-cnt}" +ebmc lcd_14.sv --solver-neural-liveness "{3-state,180000-cnt}" +fi + +if false ; then +# ok +ebmc seven_seg_1.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_2.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_3.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_4.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_5.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_6.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_7.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_8.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_9.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_10.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_11.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_12.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_16.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_17.sv --solver-neural-liveness --property SEVEN.property.p1 +ebmc seven_seg_18.sv --solver-neural-liveness --property SEVEN.property.p1 +fi + +if false ; then +ebmc thermocouple_1.sv --solver-neural-liveness "{2-state,2**5-cnt}" +ebmc thermocouple_2.sv --solver-neural-liveness "{2-state,2**9-cnt}" +ebmc thermocouple_3.sv --solver-neural-liveness "{2-state,2**10-cnt}" +ebmc thermocouple_4.sv --solver-neural-liveness "{2-state,2**10-cnt}" +ebmc thermocouple_5.sv --solver-neural-liveness "{2-state,2**11-cnt}" +ebmc thermocouple_6.sv --solver-neural-liveness "{2-state,2**11-cnt}" +ebmc thermocouple_7.sv --solver-neural-liveness "{2-state,2**12-cnt}" +ebmc thermocouple_8.sv --solver-neural-liveness "{2-state,2**12-cnt}" +ebmc thermocouple_9.sv --solver-neural-liveness "{2-state,2**13-cnt}" +ebmc thermocouple_10.sv --solver-neural-liveness "{2-state,2**14-cnt}" +ebmc thermocouple_11.sv --solver-neural-liveness "{2-state,2**14-cnt}" +ebmc thermocouple_12.sv --solver-neural-liveness "{2-state,2**14-cnt}" +ebmc thermocouple_13.sv --solver-neural-liveness "{2-state,2**15-cnt}" +ebmc thermocouple_14.sv --solver-neural-liveness "{2-state,2**16-cnt}" +ebmc thermocouple_15.sv --solver-neural-liveness "{2-state,2**17-cnt}" +ebmc thermocouple_16.sv --solver-neural-liveness "{2-state,2**18-cnt}" +ebmc thermocouple_17.sv --solver-neural-liveness "{2-state,2**19-cnt}" +fi + +if false ; then +# ok +ebmc uart_transmit_1.sv --solver-neural-liveness +ebmc uart_transmit_2.sv --solver-neural-liveness +ebmc uart_transmit_3.sv --solver-neural-liveness +ebmc uart_transmit_4.sv --solver-neural-liveness +ebmc uart_transmit_5.sv --solver-neural-liveness +ebmc uart_transmit_6.sv --solver-neural-liveness +ebmc uart_transmit_7.sv --solver-neural-liveness +ebmc uart_transmit_8.sv --solver-neural-liveness +ebmc uart_transmit_9.sv --solver-neural-liveness +ebmc uart_transmit_10.sv --solver-neural-liveness +ebmc uart_transmit_11.sv --solver-neural-liveness +ebmc uart_transmit_12.sv --solver-neural-liveness +fi + +if false ; then +ebmc vga_1.sv --solver-neural-liveness "{2**5-v_cnt,2**7-h_cnt}" +ebmc vga_2.sv --solver-neural-liveness "{2**6-v_cnt,2**8-h_cnt}" +ebmc vga_3.sv --solver-neural-liveness "{2**6-v_cnt,2**8-h_cnt}" +ebmc vga_4.sv --solver-neural-liveness "{2**7-v_cnt,2**9-h_cnt}" +ebmc vga_5.sv --solver-neural-liveness "{2**8-v_cnt,2**9-h_cnt}" +ebmc vga_6.sv --solver-neural-liveness "{2**8-v_cnt,2**9-h_cnt}" +ebmc vga_7.sv --solver-neural-liveness "{2**8-v_cnt,2**10-h_cnt}" +ebmc vga_8.sv --solver-neural-liveness "{2**9-v_cnt,2**10-h_cnt}" +ebmc vga_9.sv --solver-neural-liveness "{2**9-v_cnt,2**11-h_cnt}" +fi diff --git a/regression/ebmc/solver-neural-liveness/counter1.desc b/regression/ebmc/solver-neural-liveness/counter1.desc new file mode 100644 index 000000000..308bd0129 --- /dev/null +++ b/regression/ebmc/solver-neural-liveness/counter1.desc @@ -0,0 +1,9 @@ +CORE +counter1.sv +--traces 1 --solver-neural-liveness +^weight: nn::fc1\.n0\.w0 = 1$ +^bias: nn::fc1\.n0\.b = .*$ +^\[main\.property\.p0\] always s_eventually main\.counter == 0: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/solver-neural-liveness/counter1.sv b/regression/ebmc/solver-neural-liveness/counter1.sv new file mode 100644 index 000000000..774e492ac --- /dev/null +++ b/regression/ebmc/solver-neural-liveness/counter1.sv @@ -0,0 +1,16 @@ +// count down from 10 to 0 + +module main(input clk); + + reg [7:0] counter; + + initial counter = 10; + + always @(posedge clk) + if(counter != 0) + counter = counter - 1; + + // expected to pass + p0: assert property (s_eventually counter == 0); + +endmodule diff --git a/regression/ebmc/solver-neural-liveness/wrap_around1.desc b/regression/ebmc/solver-neural-liveness/wrap_around1.desc new file mode 100644 index 000000000..63587a300 --- /dev/null +++ b/regression/ebmc/solver-neural-liveness/wrap_around1.desc @@ -0,0 +1,9 @@ +CORE +wrap_around1.sv +--traces 1 --solver-neural-liveness +^weight: nn::fc1\.n0\.w0 = -1$ +^bias: nn::fc1\.n0\.b = .*$ +^\[main\.property\.p0\] always s_eventually main\.counter == 10: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/solver-neural-liveness/wrap_around1.sv b/regression/ebmc/solver-neural-liveness/wrap_around1.sv new file mode 100644 index 000000000..c18f89c68 --- /dev/null +++ b/regression/ebmc/solver-neural-liveness/wrap_around1.sv @@ -0,0 +1,18 @@ +// count up from 0 to 10 + +module main(input clk); + + reg [7:0] counter; + + initial counter = 0; + + always @(posedge clk) + if(counter == 10) + counter = 0; + else + counter = counter + 1; + + // expected to pass + p0: assert property (s_eventually counter == 10); + +endmodule diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile index 6497d7b0a..a0bc3e5dc 100644 --- a/src/ebmc/Makefile +++ b/src/ebmc/Makefile @@ -24,13 +24,14 @@ SRC = \ live_signal.cpp \ main.cpp \ netlist.cpp \ - neural_liveness.cpp \ + neural.cpp \ output_file.cpp \ output_smv_word_level.cpp \ output_verilog.cpp \ property_checker.cpp \ random_traces.cpp \ ranking_function.cpp \ + ranking_net.cpp \ report_results.cpp \ show_formula_solver.cpp \ show_properties.cpp \ diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 3e243e5fc..2139e2226 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -22,7 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "instrument_buechi.h" #include "liveness_to_safety.h" #include "netlist.h" -#include "neural_liveness.h" #include "output_file.h" #include "output_smv_word_level.h" #include "property_checker.h" @@ -142,9 +141,6 @@ int ebmc_parse_optionst::doit() if(cmdline.isset("random-trace") || cmdline.isset("random-waveform")) return random_trace(cmdline, ui_message_handler); - if(cmdline.isset("neural-liveness")) - return do_neural_liveness(cmdline, ui_message_handler); - if(cmdline.isset("ranking-function")) return do_ranking_function(cmdline, ui_message_handler); @@ -224,7 +220,11 @@ int ebmc_parse_optionst::doit() // LTL/SVA to Buechi? if(cmdline.isset("buechi")) + { + if(cmdline.isset("neural")) + throw ebmc_errort() << "The neural engine does not work with --buechi"; instrument_buechi(transition_system, properties, ui_message_handler); + } // possibly apply liveness-to-safety if(cmdline.isset("liveness-to-safety")) @@ -412,9 +412,8 @@ void ebmc_parse_optionst::help() " {y--trace-steps} {unumber} \t set the number of random transitions (default: 10 steps)\n" " {y--ranking-function} {uf} \t prove a liveness property using given ranking funnction (experimental)\n" " {y--property} {uid} \t the liveness property to prove\n" - " {y--neural-liveness} \t check liveness properties using neural " + " {y--neural} \t check properties using neural " "inference (experimental)\n" - " {y--neural-engine} {ucmd} \t the neural engine to use\n" //" --interpolation \t use bit-level interpolants\n" //" --interpolation-word \t use word-level interpolants\n" diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index 6b346444f..ba490ade9 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -34,8 +34,9 @@ class ebmc_parse_optionst:public parse_options_baset "(po)(cegar)(k-induction)(2pi)(bound2):" "(outfile):(xml-ui)(verbosity):(gui)" "(json-modules):(json-properties):(json-result):" - "(neural-liveness)(neural-engine):" + "(neural)" "(reset):(ignore-initial)" + "(solver-neural-liveness)" "(version)(verilog-rtl)(verilog-netlist)" "(compute-interpolant)(interpolation)(interpolation-vmcai)" "(ic3)(property):(constr)(h)(new-mode)(aiger)" diff --git a/src/ebmc/neural.cpp b/src/ebmc/neural.cpp new file mode 100644 index 000000000..9492232c4 --- /dev/null +++ b/src/ebmc/neural.cpp @@ -0,0 +1,587 @@ +/*******************************************************************\ + +Module: Neural Engine + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "neural.h" + +#if 0 +#include +#include +#include +#include +#include + +#include +#include +#include +#include + +#include "live_signal.h" +#include "random_traces.h" +#include "ranking_function.h" +#include "ranking_net.h" +#include "report_results.h" +#include "waveform.h" +#endif + +#include "ebmc_error.h" +#include "ebmc_solver_factory.h" + +#include +#include +#include + +/*******************************************************************\ + + Class: neural_enginet + + Purpose: + +\*******************************************************************/ + +class neural_enginet +{ +public: + neural_enginet( + const cmdlinet &_cmdline, + transition_systemt &_transition_system, + ebmc_propertiest &_properties, + message_handlert &_message_handler) + : cmdline(_cmdline), + transition_system(_transition_system), + properties(_properties), + message_handler(_message_handler), + solver_factory(ebmc_solver_factory(_cmdline)) + { + } + + property_checker_resultt operator()(); + +protected: + const cmdlinet &cmdline; + transition_systemt &transition_system; + ebmc_propertiest &properties; // this is a copy + message_handlert &message_handler; + ebmc_solver_factoryt solver_factory; + + #if 0 + std::vector state_variables; + using state_variable_mapt = std::unordered_map; + state_variable_mapt state_variable_map; + + using propertyt = ebmc_propertiest::propertyt; + + using tracest = std::list; + tracest traces; + + // trace state to state vector + tuple_exprt to_vector(const trans_tracet::statet &, const typet &) const; + + exprt + net_to_expression(const ranking_nett &, const decision_proceduret &) const; + + int show_traces(); + void validate_properties(); + void set_live_signal(const propertyt &, const exprt &); + void sample(); + exprt guess(propertyt &); + void minimize(decision_proceduret &, const exprt &objective); + tvt verify(propertyt &, const exprt &candidate); + #endif +}; + +static ebmc_propertiest::propertyt &find_property(ebmc_propertiest &properties) +{ + // we only do one property + std::vector ptrs; + + for(auto &property : properties.properties) + if(property.is_unknown()) + ptrs.push_back(&property); + + if(ptrs.empty()) + throw ebmc_errort() << "no property"; + + if(ptrs.size() >= 2) + throw ebmc_errort() << "The neural engine expects one property"; + + return *ptrs.front(); +} + +property_checker_resultt neural_enginet::operator()() +{ + auto &property = find_property(properties); + + // This is for LTL and some fragment of SVA only. + if( + !is_LTL(property.normalized_expr) && + !is_Buechi_SVA(property.normalized_expr)) + { + throw ebmc_errort{} << "The neural engine works on omega-regular properties only"; + } + + messaget message{message_handler}; + message.debug() << "Translating " << property.description << " to Buechi" + << messaget::eom; + + // make the automaton for the negation of the property + auto buechi = + ltl_to_buechi(not_exprt{property.normalized_expr}, message_handler); + + + + return property_checker_resultt{std::move(properties)}; +} + +#if 0 +static std::unordered_map +to_map(const std::vector &state_variables) +{ + std::unordered_map result; + for(auto &v : state_variables) + result.emplace(v, result.size()); + return result; +} + +int solver_neural_livenesst::operator()() +{ + if(cmdline.isset("show-traces")) + return show_traces(); + + state_variables = transition_system.state_variables(); + state_variable_map = to_map(state_variables); + + // Save the transition system expression, + // to add the constraint for the 'live' signal. + const auto original_trans_expr = transition_system.main_symbol->value; + + // We do everything per property. + for(auto &property : properties.properties) + { + if(property.is_disabled()) + continue; + + // Set the liveness signal for the property. + set_live_signal(property, original_trans_expr); + + // Now sample some traces. + sample(); + + // Now do a guess-and-verify loop. + while(true) + { + const auto candidate = guess(property); + + if(verify(property, candidate).is_true()) + break; // done, property holds + + const namespacet ns(transition_system.symbol_table); + show_waveform(property.witness_trace.value(), ns); + + // record the counterexample + traces.push_back(property.witness_trace.value()); + } + } +} + +int solver_neural_livenesst::show_traces() +{ + transition_system = + get_transition_system(cmdline, message.get_message_handler()); + + properties = ebmc_propertiest::from_command_line( + cmdline, transition_system, message.get_message_handler()); + + validate_properties(); + + const auto original_trans_expr = transition_system.main_symbol->value; + + for(auto &property : properties.properties) + { + if(property.is_disabled()) + continue; + + set_live_signal(property, original_trans_expr); + + sample(); + + const namespacet ns(transition_system.symbol_table); + + for(const auto &trace : traces) + show_trans_trace_numbered(trace, message, ns, std::cout); + } + + return 0; +} + +void solver_neural_livenesst::validate_properties() +{ + + for(auto &property : properties.properties) + { + if(property.is_disabled()) + { + // ignore + } + else if(property.normalized_expr.id() == ID_AF) + { + // ok + } + else if( + property.normalized_expr.id() == ID_sva_always && + to_sva_always_expr(property.normalized_expr).op().id() == + ID_sva_s_eventually) + { + // ok + } + else + { + throw ebmc_errort() + << "unsupported property - only SVA s_eventually or AF implemented"; + } + } +} + +void solver_neural_livenesst::set_live_signal( + const ebmc_propertiest::propertyt &property, + const exprt &original_trans_expr) +{ + // restore the original transition system + auto main_symbol_writeable = transition_system.symbol_table.get_writeable( + transition_system.main_symbol->name); + main_symbol_writeable->value = original_trans_expr; // copy + ::set_live_signal(transition_system, property.normalized_expr); +} + +void solver_neural_livenesst::sample() +{ + const auto number_of_traces = [this]() -> std::size_t { + if(cmdline.isset("traces")) + { + auto number_of_traces_opt = + string2optional_size_t(cmdline.get_value("traces")); + + if(!number_of_traces_opt.has_value()) + throw ebmc_errort() << "failed to parse number of traces"; + + return number_of_traces_opt.value(); + } + else + return 10; // default + }(); + + const std::size_t number_of_trace_steps = [this]() -> std::size_t { + if(cmdline.isset("trace-steps")) + { + auto trace_steps_opt = + string2optional_size_t(cmdline.get_value("trace-steps")); + + if(!trace_steps_opt.has_value()) + throw ebmc_errort() << "failed to parse number of trace steps"; + + return trace_steps_opt.value(); + } + else + return 10; // default + }(); + + message.status() << "Sampling " << number_of_traces << " traces with " + << number_of_trace_steps << " steps" << messaget::eom; + + auto trace_consumer = [&](trans_tracet trace) { + traces.push_back(std::move(trace)); + }; + + random_traces( + transition_system, + trace_consumer, + number_of_traces, + number_of_trace_steps, + message.get_message_handler()); +} + +static bool is_live(const trans_tracet::statet &state) +{ + for(auto &assignment : state.assignments) + { + auto &lhs = assignment.lhs; + if( + lhs.id() == ID_symbol && + to_symbol_expr(lhs).get_identifier() == "nuterm::live") + return assignment.rhs.is_true(); + } + + throw ebmc_errort() << "liveness signal not found"; +} + +static exprt loss_constraint(tuple_exprt curr, tuple_exprt next) +{ + PRECONDITION(curr.operands().size() == next.operands().size()); + + // The ranking needs to decrease from 'curr' to 'next'. + auto &curr_val = curr.operands()[0]; + auto &next_val = next.operands()[0]; + return less_than_exprt{next_val, curr_val}; +} + +tuple_exprt solver_neural_livenesst::to_vector( + const trans_tracet::statet &state, + const typet &type) const +{ + tuple_exprt::operandst result; + result.resize(state_variable_map.size(), from_integer(0, type)); + + for(auto &assignment : state.assignments) + { + auto s_it = state_variable_map.find(assignment.lhs); + if(s_it != state_variable_map.end()) + if(assignment.rhs.is_constant()) + result[s_it->second] = + typecast_exprt::conditional_cast(assignment.rhs, type); + } + + return tuple_exprt{std::move(result)}; +} + +static exprt objective(const ranking_nett &net) +{ + // return from_integer(0, signedbv_typet{32}); + + exprt::operandst summands; + + for(auto &neuron : net.fc1.neurons) + { + for(auto &weight : neuron.weights) + summands.push_back(abs_exprt{weight}); + + // summands.push_back(abs_exprt{neuron.bias}); + } + + DATA_INVARIANT(!summands.empty(), "must have neuron"); + auto type = summands[0].type(); + + return plus_exprt{std::move(summands), std::move(type)}; +} + +void solver_neural_livenesst::minimize( + decision_proceduret &solver, + const exprt &objective) +{ + exprt objective_value = nil_exprt(); + + std::size_t iteration = 0; + while(true) + { + iteration++; + message.status() << "iteration " << iteration << messaget::eom; + + // we want a better solution + auto constraint = objective_value.is_nil() + ? static_cast(true_exprt()) + : less_than_exprt{objective, objective_value}; + + auto dec_result = solver(constraint); + + switch(dec_result) + { + case decision_proceduret::resultt::D_SATISFIABLE: + objective_value = solver.get(objective); + message.status() << "objective: " << format(objective_value) + << messaget::eom; + break; + + case decision_proceduret::resultt::D_UNSATISFIABLE: + if(objective_value.is_nil()) + { + // no ranking function possible + throw ebmc_errort() + << "architecture does not allow ranking function, giving up"; + } + + message.status() << "found optimal assignment" << messaget::eom; + + // go back to previous, to get satisfying assignment + solver(equal_exprt{objective, objective_value}); + return; + + case decision_proceduret::resultt::D_ERROR: + throw ebmc_errort() << "Error from decision procedure"; + + default: + throw ebmc_errort() << "Unexpected result from decision procedure"; + } + } +} + +static void bits_constraint( + const exprt &expr, + std::size_t bits, + decision_proceduret &solver) +{ + PRECONDITION(bits != 0); + + auto expr_bits = to_bitvector_type(expr.type()).get_width(); + + if(expr_bits <= bits) + return; // nothing to do + + // signed encoding + auto top_bit = extractbit_exprt{expr, expr_bits - 1}; + + for(std::size_t i = bits; i < expr_bits - 1; i++) + solver << equal_exprt{top_bit, extractbit_exprt{expr, i}}; +} + +exprt solver_neural_livenesst::net_to_expression( + const ranking_nett &net, + const decision_proceduret &solver) const +{ + // get the weights + for(std::size_t i = 0; i < state_variables.size(); i++) + { + auto weight_value = solver.get(net.fc1.neurons[0].weights[i]); + std::cout << "weight: " << format(state_variables[i]) << " = " + << format(weight_value) << '\n'; + } + + // get the bias + auto &bias = net.fc1.neurons[0].bias; + std::cout << "bias: " << format(bias) << " = " << format(solver.get(bias)) + << '\n'; + + exprt::operandst summands; + + for(std::size_t i = 0; i < state_variables.size(); i++) + { + auto weight_value = solver.get(net.fc1.neurons[0].weights[i]); + if(!weight_value.is_zero()) + summands.push_back(mult_exprt{ + weight_value, + typecast_exprt::conditional_cast( + state_variables[i], weight_value.type())}); + } + + if(!solver.get(bias).is_zero()) + summands.push_back(solver.get(bias)); + + if(summands.empty()) + throw ebmc_errort() << "no weights"; + + exprt fc1; + + if(summands.size() == 1) + fc1 = summands.front(); + else + { + auto type = summands.front().type(); + fc1 = plus_exprt{std::move(summands), std::move(type)}; + } + + return wrap_around(fc1); +} + +exprt solver_neural_livenesst::guess(propertyt &property) +{ + message.status() << "Fitting a ranking function" << messaget::eom; + + const namespacet ns(transition_system.symbol_table); + satcheckt satcheck{message.get_message_handler()}; + boolbvt solver(ns, satcheck, message.get_message_handler()); + //auto solver_container = solver_factory(ns, message.get_message_handler()); + //auto &solver = solver_container.decision_procedure(); + + // set up net + auto net_type = signedbv_typet{40}; + std::size_t dimension = 2; + auto net = ranking_nett{state_variable_map.size(), dimension, net_type}; + + // form a batch + std::size_t transitions = 0; + + for(const auto &trace : traces) + { + for(std::size_t i = 1; i < trace.states.size(); i++) + { + auto &curr = trace.states[i - 1]; + auto &next = trace.states[i]; + + if(is_live(curr) || is_live(next)) + continue; + + auto prediction_curr = net.forward(to_vector(curr, net_type)); + auto prediction_next = net.forward(to_vector(next, net_type)); + + // loss must be zero + solver << loss_constraint( + std::move(prediction_curr), std::move(prediction_next)); + + transitions++; + } + } + + message.status() << "Batch with " << transitions << " transition(s)" + << messaget::eom; + + // constraints on parameters + for(auto &weight : net.fc1.neurons[0].weights) + bits_constraint(weight, 2, solver); + + // get the bias + bits_constraint(net.fc1.neurons[0].bias, 35, solver); + + // minimize + auto objective = ::objective(net); + message.status() << format(objective) << messaget::eom; + const auto objective_symbol = + symbol_exprt{"nuterm::objective", objective.type()}; + solver << equal_exprt{objective_symbol, std::move(objective)}; + solver.set_frozen(solver.convert_bv(objective_symbol)); + minimize(solver, objective_symbol); + + // read off the candidate + exprt candidate = net_to_expression(net, solver); + + message.status() << "candidate: " << messaget::green << format(candidate) + << messaget::reset << messaget::eom; + + return candidate; +} + +tvt solver_neural_livenesst::verify( + ebmc_propertiest::propertyt &property, + const exprt &candidate) +{ + message.status() << "Checking the candidate ranking function" + << messaget::eom; + + auto result = is_ranking_function( + transition_system, + property.normalized_expr, + candidate, + solver_factory, + message.get_message_handler()); + + property.witness_trace = std::move(result.second); + + if(result.first.is_true()) + property.proved(); + else + property.inconclusive(); + + return result.first; +} +#endif + +property_checker_resultt neural( + const cmdlinet &cmdline, + transition_systemt &transition_system, + ebmc_propertiest &properties, + message_handlert &message_handler) +{ + neural_enginet neural_engine{cmdline, transition_system, properties, message_handler}; + return neural_engine(); +} diff --git a/src/ebmc/neural.h b/src/ebmc/neural.h new file mode 100644 index 000000000..e05b26b34 --- /dev/null +++ b/src/ebmc/neural.h @@ -0,0 +1,27 @@ +/*******************************************************************\ + +Module: Neural Engine + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_EBMC_NEURAL_H +#define CPROVER_EBMC_NEURAL_H + +#include +#include + +#include "ebmc_solver_factory.h" +#include "property_checker.h" + +class transition_systemt; +class ebmc_propertiest; + +[[nodiscard]] property_checker_resultt neural( + const cmdlinet &, + transition_systemt &, + ebmc_propertiest &, + message_handlert &); + +#endif // CPROVER_EBMC_NEURAL_H diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp index d18d72921..b4e36242f 100644 --- a/src/ebmc/property_checker.cpp +++ b/src/ebmc/property_checker.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "ic3_engine.h" #include "k_induction.h" #include "netlist.h" +#include "neural.h" #include "output_file.h" #include "report_results.h" @@ -441,9 +442,10 @@ property_checker_resultt property_checker( ebmc_propertiest &properties, message_handlert &message_handler) { - bool use_heuristic_engine = !cmdline.isset("bdd") && !cmdline.isset("aig") && - !cmdline.isset("k-induction") && - !cmdline.isset("ic3") && !cmdline.isset("bound"); + bool use_heuristic_engine = + !cmdline.isset("bdd") && !cmdline.isset("aig") && + !cmdline.isset("k-induction") && !cmdline.isset("ic3") && + !cmdline.isset("bound") && !cmdline.isset("neural"); auto result = [&]() -> property_checker_resultt { @@ -472,6 +474,10 @@ property_checker_resultt property_checker( cmdline, transition_system, properties, message_handler); #endif } + else if(cmdline.isset("neural")) + { + return neural(cmdline, transition_system, properties, message_handler); + } else if(cmdline.isset("bound")) { // word-level BMC diff --git a/src/ebmc/ranking_net.cpp b/src/ebmc/ranking_net.cpp new file mode 100644 index 000000000..1b58625de --- /dev/null +++ b/src/ebmc/ranking_net.cpp @@ -0,0 +1,106 @@ +/*******************************************************************\ + +Module: Ranking Neural Net + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "ranking_net.h" + +#include +#include +#include + +exprt wrap_around(exprt expr) +{ + // map negative values to positive ones, wrap around: + // -1 --> int_max-1, -2 --> int_max-2, etc. + auto int_max = to_signedbv_type(expr.type()).largest_expr(); + return if_exprt{sign_exprt{expr}, plus_exprt{int_max, expr}, expr}; +} + +tuple_exprt wrap_around_tuple(tuple_exprt expr) +{ + // map negative values to positive ones, wrap around: + // -1 --> int_max-1, -2 --> int_max-2, etc. + for(auto &op : expr.operands()) + op = wrap_around(op); + + return expr; +} + +tuple_exprt ranking_nett::forward(const tuple_exprt &inputs) const +{ + auto fc1_out = fc1.forward(inputs); + auto w_out = wrap_around_tuple(fc1_out); + return w_out; +} + +ranking_nett::lineart::lineart( + const irep_idt &__name, + std::size_t in, + std::size_t out, + const typet &type) + : name(__name) +{ + neurons.reserve(out); + + for(std::size_t i = 0; i < out; i++) + { + irep_idt identifier = id2string(__name) + ".n" + std::to_string(i); + neurons.emplace_back(identifier, in, type); + } +} + +ranking_nett::lineart::neuront::neuront( + const irep_idt &__name, + std::size_t in, + const typet &type) + : name(__name) +{ + { + irep_idt identifier = id2string(__name) + ".b"; + bias = symbol_exprt(identifier, type); + } + + weights.reserve(in); + + for(std::size_t i = 0; i < in; i++) + { + irep_idt identifier = id2string(__name) + ".w" + std::to_string(i); + weights.emplace_back(symbol_exprt{identifier, type}); + } +} + +exprt ranking_nett::lineart::neuront::forward(const tuple_exprt &input) const +{ + exprt::operandst result; + result.reserve(weights.size() + 1); // one more for bias + + result.push_back(bias); + + PRECONDITION(weights.size() == input.operands().size()); + + for(std::size_t i = 0; i < weights.size(); i++) + result.push_back(mult_exprt{weights[i], input.operands()[i]}); + + return plus_exprt{std::move(result), bias.type()}; +} + +exprt relu(exprt expr) +{ + auto zero = from_integer(0, expr.type()); + return if_exprt{greater_than_or_equal_exprt{expr, zero}, expr, zero}; +} + +tuple_exprt ranking_nett::lineart::forward(const tuple_exprt &input) const +{ + tuple_exprt::operandst result; + result.reserve(neurons.size()); + + for(auto &neuron : neurons) + result.push_back(neuron.forward(input)); + + return tuple_exprt{std::move(result)}; +} diff --git a/src/ebmc/ranking_net.h b/src/ebmc/ranking_net.h new file mode 100644 index 000000000..e0945cb7f --- /dev/null +++ b/src/ebmc/ranking_net.h @@ -0,0 +1,59 @@ +/*******************************************************************\ + +Module: Ranking Neural Net + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef EBMC_RANKING_NET_H +#define EBMC_RANKING_NET_H + +#include + +exprt relu(exprt); +exprt wrap_around(exprt); + +class ranking_nett +{ +public: + explicit ranking_nett( + std::size_t number_of_state_variables, + std::size_t fc1_neurons, + const typet &__type) + : fc1("nn::fc1", number_of_state_variables, fc1_neurons, __type) + { + } + + tuple_exprt forward(const tuple_exprt &inputs) const; + + class lineart + { + public: + lineart( + const irep_idt &name, + std::size_t in, + std::size_t out, + const typet &); + + irep_idt name; + + class neuront + { + public: + std::vector weights; + exprt bias; + irep_idt name; + neuront(const irep_idt &name, std::size_t in, const typet &); + exprt forward(const tuple_exprt &) const; + }; + + std::vector neurons; + + tuple_exprt forward(const tuple_exprt &) const; + }; + + lineart fc1; +}; + +#endif // EBMC_RANKING_NET diff --git a/src/ebmc/neural_liveness.h b/src/ebmc/solver_neural_liveness.h similarity index 52% rename from src/ebmc/neural_liveness.h rename to src/ebmc/solver_neural_liveness.h index 159f38208..c639c1d6b 100644 --- a/src/ebmc/neural_liveness.h +++ b/src/ebmc/solver_neural_liveness.h @@ -1,17 +1,17 @@ /*******************************************************************\ -Module: Neural Liveness +Module: Solver Neural Liveness Author: Daniel Kroening, dkr@amazon.com \*******************************************************************/ -#ifndef EBMC_NEURAL_LIVENESS_H -#define EBMC_NEURAL_LIVENESS_H +#ifndef EBMC_SOLVER_NEURAL_LIVENESS_H +#define EBMC_SOLVER_NEURAL_LIVENESS_H #include #include -int do_neural_liveness(const cmdlinet &, ui_message_handlert &); +int do_solver_neural_liveness(const cmdlinet &, ui_message_handlert &); -#endif // EBMC_NEURAL_LIVENESS_H +#endif // EBMC_SOLVER_NEURAL_LIVENESS_H