►
Description
Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more.
https://archive.devcon.org/archive/watch/6/scaling-up-trustless-neural-network-inference-with-zero-knowledge-proofs/index
We present the first ZK-SNARK proof of valid inference for a full resolution ImageNet model. We will describe the arithmetization and quantization optimizations enabling us to SNARK large neural networks as well as a software package enabling transpilation from off-the-shelf models to halo2 circuits. We design protocols using our circuits to verify machine learning model predictions and accuracy and present concrete estimates of overhead costs based on our circuit implementations. This is joint
Speaker(s): Yi Sun
Skill level: Beginner
Track: ZKPs: Privacy, Identity, Infrastructure, & More
Keywords: zk
Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/
Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.
Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/
A
A
So
this
is
a
bit
of
a
book
report
about
what
happened
when
I
tried
to
convince
the
machine
learning
people
that
zero
knowledge
proofs
were
very
relevant
to
them.
So
in
that
line
it's
this
is
Joint
work
with
a
bunch
of
machine
learning,
professors,
okay,
so
the
motivation
we
came
to
this
problem
with
is
that,
right
now
today,
a
lot
of
the
least
trusted
parties
in
society
are
running
machine
learning
models
that
have
broad
societal
impacts.
A
A
So
in
this
Paradigm
you
know
you're,
maybe
making
a
slide,
and
you
want
a
cool
image,
so
you'll
send
hey
openai
I
want
an
image
of
teddy
bears
working
on
AI
research
underwater,
an
opening
I
will
send
you
back
this
beautiful
image.
To
put
in
this
slide
now,
the
core
problem
in
both
of
these
use
cases
is
that
well,
as
the
user,
you
have
no
insight
into
what
the
model
Runner
is
actually
doing.
A
A
A
So
in
this
case
a
number
of
separate
parties
will
perform
the
machine
learning
operation
together
and,
of
course,
because
they're
collaborating
this
requires
that
the
parties
are
online
simultaneously
and
there's
a
one
of
n
trust
model
for
privacy
and
correct
execution.
That
means
that
you
need
to
trust
that
only
one
of
the
end
parties
is
actually
behaving
honestly,
so
it's
possible
for
NPC
to
provide
both
privacy
and
validity,
but
unfortunately
it
requires
pretty
high
interaction
and
high
bandwidth
and
at
least
at
present,
there's
a
really
high
compute
overhead.
If
you
want
to
ensure
validity.
A
So
as
a
result,
we
looked
into
the
literature
and
it
looks
like
MPC-
can
only
handle
relatively
small
models
today.
Another
technique-
that's
pretty
popular,
is
homomorphic
encryption.
The
idea
here
is
you,
take
your
input,
data
encrypt
it
and
send
it
to
some
server
that
runs
a
machine
learning
model
on
the
encrypted
data
without
knowing
about
it.
So
in
this
case,
homomorphic
encryption
is
only
targeted
at
privacy
and
not
at
guaranteeing
validity.
A
The
benefits
are
that
you
don't
need
to
interact
with
the
server
Beyond
sending
your
encrypted
input,
but
the
downside
is
that
there's
a
really
massive
compute
overhead
for
NPC
I
said
there
was
a
big
compute
overhead,
but
trust
me
this
is
really
massive,
and
so,
as
a
consequence,
MPC
today,
as
far
as
I
know,
can
only
handle
quite
tiny
models.
I
mean
recognizing
digits.
A
A
So
in
this
case,
ZK
can
ensure
validity.
That
is
that
the
model
was
correctly
executed
and
it
can
ensure
a
weaker
notion
of
privacy
than
MPC
and
homomorphic
encryption,
that
is
for
ZK.
The
model
runner
needs
to
know
everything
about
the
input,
whereas
that's
not
necessary
in
NPC
and
homomorphic
encryption,
but
once
you
have
the
proof,
the
input
can
be
private
from
the
rest
of
the
world.
A
Another
upside
is
that
there's
no
interaction
required
and
a
downside
is
that
there's
still
a
pretty
massive
computation
overhead
over
the
cost
of
inference.
So
in
this
talk,
I'm
going
to
talk
about
a
method
we
developed
to
scale
this,
the
application
of
ZK
by
reducing
the
compute
overhead
from
pretty
small
models
to
relatively
large
models.
A
Okay,
so
let
me
first
situate
you
in
the
task
and
what
I
mean
by
small
and
big.
So
a
lot
of
Prior
work
in
ZK
for
neural
network
inference
focused
on
these
two
Benchmark
tasks:
mnist
and
c410.
The
task
in
mnist
is
you
get
a
black
and
white
digit
and
you
have
to
recognize
which
of
those
digits
it
is.
The
post
office
uses
something
like
this.
A
In
cfar,
there
are
32
by
32
pixels
of
10
classes
of
things
like
car
automobile
horse
boat,
and
you
have
to
choose
for
each
image
which
of
those
10
glasses
applies.
So
in
our
work
we
scale
things
up
to
approach
the
much
larger
imagenet
data
set.
So
in
this
case
we
have
1000
classes,
image
that
happens
to
contain
many
breeds
of
dog.
So
actually
there
are
200
breeds
of
dog
and
at
1
000
classes.
A
A
Okay,
so
here's
what
we
can
do.
We
chose
a
model
called
mobilenet
V2,
which
was
developed
originally
to
be
run
in
low
resource
environments
such
as
mobile
phones
for
a
range
of
input
resolutions,
we're
able
to
completely
snark
the
execution
of
the
model
and,
as
you
can
see,
the
proving
time
for
a
single
input
is
still
relatively
large.
Okay,
so
even
for
the
smallest
input
resolution
of
96
by
96,
we
take
over
two
minutes,
but
we
are
able
to
scale
to
the
full
image
of
that
resolution
in
about
20
minutes.
A
So
this
is
using
the
Halo
2
back
end
with
the
Original
IPA
proving
system.
As
you
can
see,
the
proof
size
is
relatively
small
and
the
compete
verification.
Time,
thankfully,
is
not
as
large
as
the
proving
time,
although
perhaps
still
quite
large,
okay.
So
let
me
in
the
rest
of
the
talk.
Let
me
talk
a
little
bit
about
how
we
did
this
and
what
we
can
do
with
it.
So
when
you
think
about
snarking
execution
of
a
neural
network,
we
came
at
it
by
dividing
the
problem
into
three
pieces.
A
The
first
piece
is:
it
turns
out
that
the
notion
of
difficulty
of
execution
between
neural
networks
run
on
gpus
and
snarking
things
in
a
zero
case.
Circuit
is
quite
different,
so
we
tried
to
select
the
best
architecture
for
this
task.
The
second
is:
we
had
to
devise
a
pretty
optimal
way
of
arithmeticizing.
This
neural
network
inference
operation
into
a
ZK
circuit,
and
last
we
selected
a
proving
system,
largely
because
we
were
most
familiar
with
Halo
2..
A
The
first
thing
to
note
is
that
it's
very
hard
to
deal
with
floating
Point
numbers
within
a
ZK
circuit,
since
every
variable
in
a
ZK
circuit
is
under
the
hood,
a
large
Prime
field
element
so
that
essentially
forces
us
to
work
with
quantized
models.
That
is,
models
that
were
specifically
designed
to
have
all
of
their
weights,
be
8-bit
integers.
For
now,
the
level
of
quantization
in
machine
learning
generally
gives
you
a
trade-off
between
accuracy
and
how
few
bits
you've
quantized
the
model
into,
and
in
ZK.
This
translates
to
a
trade-off
between
accuracy
and
proving
cost.
A
A
A
Finally,
in
the
arithmetization
back
end,
we
use
the
planckish
arithmetization
for
Halo
2,
and
so
we
actually
only
used
two
types
of
features
of
Halo
2.
We
handle
all
the
linear
layers
via
custom
Gates
and
we
use
the
lookup
tables
to
essentially
build
a
lookup
table
of
all
all
non-linearities
and
finally,
there's
a
small
subtlety
that
we
have
to
readjust
the
fixed
point
in
the
quantization
and
we're
able
to
do
some
optimization
by
shoving
that
into
the
lookup
table.
A
Okay,
let
me
now
finish
by
just
giving
you
a
general
sense
of
one
application
that
we
can
do
with
this.
So
there's
sort
of
four
settings
as
Jason
alluded
to
so
where
the
you
can
make
the
model
either
public
or
private.
You
can
make
the
data
either
public
or
private,
and
you
can
combinatorially
combine
these.
So
we
have
a
couple
ideas
in
each
quadrant.
A
If
your
data
and
model
are
both
public
and
we
think
that
this
could
be
useful
for
on-chain
verification
as
Json
alluded
to.
And
finally,
if
your
data
is
private,
then
in
both
the
private
and
public
model
format,
we
think
that
this
could
be
useful
for
conducting
an
audit
for,
for
example,
in
legal
Discovery.
Without
forcing
revelation
of
the
entire
data
set
that
you
hold.
A
Okay,
so
just
to
give
one
sample
back
of
the
envelope
calculation
of
how
much
it
would
cost
to
use
our
snark
to
do
verified
machine
learning
model
accuracy.
We
made
a
very
basic
protocol
where
a
model
perspective.
Buyer
asked
a
model
seller
to
verify
the
accuracy
of
a
model
on
a
randomly
chosen
test
set.
So
in
this
case,
you
want
to
randomly
sample
from
the
test
set,
find
the
accuracy
on
the
random
sample
and
from
that
you're
going
to
get
some
statistical
estimates
of
your
overall
model
accuracy.
A
So
we
ran
the
numbers
and
it
turns
out
that,
if
you
want
to
have,
you
know
within,
you
have
want
to
know
the
accuracy
within
five
percent
at
a
95
confidence
interval.
You
need
to
sample
600
times
and
that
will
cost
about
ninety
dollars
to
verify.
If
you
want
to
be
within
one
percent,
that's
going
to
cost
you
a
little
over
two
thousand
dollars
with
our
current
implementation
and
just
to
give
you
a
sense
of
whether
that
could
be
reasonable.
A
People
generally
are
willing
to
spend
in
the
high
five
figures-
maybe
low
six
figures
just
to
acquire
data
to
train
their
model.
So
maybe
it's
worthwhile
to
pay
a
couple
thousand
dollars
to
verify
that
what
you're
buying
is
legitimate,
all
right.
So,
just
to
summarize,
we
constructed
the
first
snark.
A
We
think
that
can
scale
to
imagenet
level,
and
for
this
we
had
to
choose
the
correctly
quantized
mile
model
write
a
compiler
from
tensorflow
Lite
to
a
Halo,
2
plonkish
arithmetization,
and
then
we
ran
some
benchmarks
on
whether
this
sort
of
technique
is
reasonable
for
some
concrete
applications
of
verified
inference
so
going
forward.
We're
excited
to
explore
some
more
applications
of
verified
inference
and
also
try
to
scale
this
to
different
types
of
models,
particularly
Transformers
thanks
and
I.
Don't
know
if
there's
any
time
for
questions.
B
A
A
That's
a
very
hard
question,
since,
if
there
is
an
optimization,
we
thought
we
could
do
we
generally
just
did
it
one
thing
I
didn't
mention.
Is
we
tried
to
reduce
the
number
of
lookup
arguments
by
sharing
them
across
layers
in
gen?
This
actually
modifies
the
computation
slightly.
So
there's
a
little
trade-off
between
the
machine
learning
model
accuracy
and
the
proving
speed.