0 | {--
 1 | Copyright (C) 2021  Joel Berkeley
 2 |
 3 | This program is free software: you can redistribute it and/or modify
 4 | it under the terms of the GNU Affero General Public License as published
 5 | by the Free Software Foundation, either version 3 of the License, or
 6 | (at your option) any later version.
 7 |
 8 | This program is distributed in the hope that it will be useful,
 9 | but WITHOUT ANY WARRANTY; without even the implied warranty of
10 | MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
11 | GNU Affero General Public License for more details.
12 |
13 | You should have received a copy of the GNU Affero General Public License
14 | along with this program.  If not, see <https://www.gnu.org/licenses/>.
15 | --}
16 | ||| Functionality for Bayesian optimization, the data-efficient optimization of objective functions.
17 | ||| Bayesian optimization recommends new points at which to query your objective by placing a
18 | ||| probabilistic model over historic data then, typically, optimizing an _acquisition function_
19 | ||| which quantifies how useful it would be to evaluate the objective at any given set of points.
20 | module BayesianOptimization
21 |
22 | import Control.Monad.Reader
23 |
24 | import public BayesianOptimization.Acquisition as BayesianOptimization
25 | import Data
26 | import Model
27 | import Tensor
28 |
29 | ||| A `Stream`-like collection where each successive element can extend the set of `Tag`s.
30 | public export
31 | data TagStream : Type -> Type where
32 |   (::) : a -> Inf (Tag (TagStream a)) -> TagStream a
33 |
34 | ||| Take `n` values from a `TagStream`, sequencing the `Tag` effects.
35 | public export
36 | take : (n : Nat) -> TagStream a -> Tag $ Vect n a
37 | take Z _ = pure Nil
38 | take (S k) (x :: xs) = pure (x :: !(take k !xs))
39 |
40 | ||| Create an infinite stream of values from a generator function and a starting value.
41 | export covering
42 | iterate : (a -> Tag a) -> a -> Tag $ TagStream a
43 | iterate f x = do
44 |   x' <- f x
45 |   pure (x' :: iterate f x')
46 |
47 | ||| Construct a single simple Bayesian optimization step.
48 | |||
49 | ||| @objective The objective function to optimize.
50 | ||| @train Used to train the model on new data.
51 | ||| @tactic The tactic, such as an optimized acquisition function, to find a new point from the
52 | |||   data and model
53 | export
54 | step : (objective : forall n . Tensor (n :: features) F64 -> Tag $ Tensor (n :: targets) F64) ->
55 |        (probabilisticModel : ProbabilisticModel features targets marginal model) =>
56 |        (train : Dataset features targets -> model -> Tag $ model) ->
57 |        (tactic : ReaderT (DataModel {probabilisticModel} model) Tag (Tensor (1 :: features) F64)) ->
58 |        DataModel {probabilisticModel} model ->
59 |        Tag $ DataModel {probabilisticModel} model
60 | step objective train tactic env = do
61 |   newPoint <- runReaderT env tactic
62 |   dataset <- tag $ concat env.dataset $ MkDataset newPoint !(objective newPoint)
63 |   pure $ MkDataModel !(train dataset env.model) dataset
64 |