3 ms·

I sent you an email, but all I can say is please come to Switzerland so I can work with you guys :-) Everything I've seen so far looks quite awesome. Two quest

I sent you an email, but all I can say is please come to Switzerland so I can work with you guys :-) Everything I've seen so far looks quite awesome. Two questions: 1. Are you implying you are using deep learning heuristics for weighted set packing? Assuming you can't share too much about your IP, did you have a regulatory or business need to deal with worst-case performance guarantees and (how) did you manage this if you did? 2. It sounds like a lot of your stack is OCaml (I'm a fan, 2nd most fanboyed language after Rust and it's a pity it's not more used), is this a deliberate choice or a "grew out of a research project in formal verification where they like ML" consequence?

lpage 5y ago
Thanks! I'll reply to you there as well. 1. There are two places where deep learning and prior-based approaches can come into play for combinatorial auctions. One is pretty analogous to AlphaZero, but substitute placing a piece on a Go board with accepting a bid, hoping that upon reaching a terminal state the set of bids accepted is feasible and close to optimal. The second is perhaps more in line with what you mentioned—using ML for hyperparameter selection in an algorithm portfolio. When we go live and have production data, our meta optimizer will measure how different approaches are doing and allocate computational resources accordingly in an online fashion. We always use a vanilla unit double auction as a baseline to measure relative performance within an auction cycle, and if the baseline is better, we use it instead. 2. There's a fun and serendipitous story here. I wrote an extremely early prototype as a tiny lisp and evaluator to go with it. We needed a very restricted and functionally pure language that we could control the execution context of, symbolically execute, and do basic formal methods on. The approach worked for a POC, but it was a far cry from real-world adoptable. We proceeded to prototype a DSL with an HM inspired type system and a more pythonic syntax, arriving at a poor man's ML. Better, but a DSL, and something limited/bespoke that would ultimately be annoying for developers. Then we met the guys at Imandra [1], who convinced us that we could have our cake and eat it too using vanilla OCaml/ReasonML and an ultra-high level theorem prover to keep code in an acceptable logic fragment. As an aside, rust is our systems PL and where we do most of the heavy lifting. Evaluating Expressive Bids isn't computationally expensive relative to the optimization problem. [1]: https://www.imandra.ai/ https://www.imandra.ai/

lpage 5y ago

Thanks! I'll reply to you there as well. 1. There are two places where deep learning and prior-based approaches can come into play for combinatorial auctions. One is pretty analogous to AlphaZero, but substitute placing a piece on a Go board with accepting a bid, hoping that upon reaching a terminal state the set of bids accepted is feasible and close to optimal. The second is perhaps more in line with what you mentioned—using ML for hyperparameter selection in an algorithm portfolio. When we go live and have production data, our meta optimizer will measure how different approaches are doing and allocate computational resources accordingly in an online fashion. We always use a vanilla unit double auction as a baseline to measure relative performance within an auction cycle, and if the baseline is better, we use it instead. 2. There's a fun and serendipitous story here. I wrote an extremely early prototype as a tiny lisp and evaluator to go with it. We needed a very restricted and functionally pure language that we could control the execution context of, symbolically execute, and do basic formal methods on. The approach worked for a POC, but it was a far cry from real-world adoptable. We proceeded to prototype a DSL with an HM inspired type system and a more pythonic syntax, arriving at a poor man's ML. Better, but a DSL, and something limited/bespoke that would ultimately be annoying for developers. Then we met the guys at Imandra [1], who convinced us that we could have our cake and eat it too using vanilla OCaml/ReasonML and an ultra-high level theorem prover to keep code in an acceptable logic fragment. As an aside, rust is our systems PL and where we do most of the heavy lifting. Evaluating Expressive Bids isn't computationally expensive relative to the optimization problem. [1]: https://www.imandra.ai/ https://www.imandra.ai/